From 38fe3eda02d0c624db72b0ca6275e0dd9a2c64a8 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Wed, 22 Apr 2026 09:33:33 +0200 Subject: [PATCH 01/16] added finiteness conditions to option type --- Mathlib/Data/Finite/Option.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 Mathlib/Data/Finite/Option.lean diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean new file mode 100644 index 00000000000000..52f7ef27bfcfb0 --- /dev/null +++ b/Mathlib/Data/Finite/Option.lean @@ -0,0 +1,16 @@ +module + +public import Mathlib.Data.Fintype.Option +public import Mathlib.Logic.Equiv.Fin.Basic + +@[expose] public section + +@[simp] +theorem Option.finite_iff {α : Type*} : Finite (Option α) ↔ Finite α where + mpr _ := instFiniteOption + mp + | @Finite.intro _ 0 e => (e none).elim0 + | @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩ + + +#min_imports From 53ac572c8328a28f4d7dcd9376a1a2d7d85be5d8 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 10:56:06 +0200 Subject: [PATCH 02/16] feat(Mathlib/Data/Finite/Option): option type is finite iff type is finite --- Mathlib/Data/Finite/Option.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean index 52f7ef27bfcfb0..2354e1ad0938fb 100644 --- a/Mathlib/Data/Finite/Option.lean +++ b/Mathlib/Data/Finite/Option.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2026 Alex Brodbelt. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex Brodbelt and Eric Wieser +-/ module public import Mathlib.Data.Fintype.Option From 50129d7bef8adbbe07430d626336a9874dcd006e Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:05:09 +0200 Subject: [PATCH 03/16] feat(Mathlib/Data/Finite/Subtype): Subtype of elements not equal to a term is finite iff type is finite --- Mathlib/Data/Finite/Subtype.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 Mathlib/Data/Finite/Subtype.lean diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean new file mode 100644 index 00000000000000..29527be166ae74 --- /dev/null +++ b/Mathlib/Data/Finite/Subtype.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Alex Brodbelt. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex Brodbelt and Eric Wieser +-/ +module + +public import Mathlib.Data.Finite.Option + +@[expose] public section + +@[simp] +theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by + classical + rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff] + +#min_imports From 9a375372eed4d678a817f1474c58af8101505461 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:13:36 +0200 Subject: [PATCH 04/16] remove min imports command --- Mathlib/Data/Finite/Subtype.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean index 29527be166ae74..9b90419fe6a054 100644 --- a/Mathlib/Data/Finite/Subtype.lean +++ b/Mathlib/Data/Finite/Subtype.lean @@ -13,5 +13,3 @@ public import Mathlib.Data.Finite.Option theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by classical rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff] - -#min_imports From 3ca377b5008a0bddbe87f3bcd884505d625e8375 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:14:57 +0200 Subject: [PATCH 05/16] remove min import command --- Mathlib/Data/Finite/Option.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean index 2354e1ad0938fb..d0dfa49f8e0628 100644 --- a/Mathlib/Data/Finite/Option.lean +++ b/Mathlib/Data/Finite/Option.lean @@ -16,6 +16,3 @@ theorem Option.finite_iff {α : Type*} : Finite (Option α) ↔ Finite α where mp | @Finite.intro _ 0 e => (e none).elim0 | @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩ - - -#min_imports From 99baf79d68edb8c9bbd13708f58800535f7ec235 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:44:57 +0200 Subject: [PATCH 06/16] add new file to Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 51a2d9e682d0ca..76ae6b4dedc9ff 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3820,6 +3820,7 @@ public import Mathlib.Data.FinEnum public import Mathlib.Data.FinEnum.Option public import Mathlib.Data.Finite.Card public import Mathlib.Data.Finite.Defs +public import Mathlib.Data.Finite.Option public import Mathlib.Data.Finite.Perm public import Mathlib.Data.Finite.Prod public import Mathlib.Data.Finite.Set From a88c8cce5bc40ce6c40484b1e86a86a5621ee4e9 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 12:04:18 +0200 Subject: [PATCH 07/16] added docstrings and comments to files --- Mathlib/Data/Finite/Option.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean index d0dfa49f8e0628..5fedbe9aa34088 100644 --- a/Mathlib/Data/Finite/Option.lean +++ b/Mathlib/Data/Finite/Option.lean @@ -1,15 +1,19 @@ /- Copyright (c) 2026 Alex Brodbelt. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex Brodbelt and Eric Wieser +Authors: Alex Brodbelt, Eric Wieser -/ module public import Mathlib.Data.Fintype.Option public import Mathlib.Logic.Equiv.Fin.Basic -@[expose] public section +/-! +# Finiteness conditions for `Option` types +-/ +@[expose] public section +/-- The `Option` type on a type is finite if and only if the underlying type is finite -/ @[simp] theorem Option.finite_iff {α : Type*} : Finite (Option α) ↔ Finite α where mpr _ := instFiniteOption From 33329466da56eb8eb5cb547afbcab381640f46a1 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:05:09 +0200 Subject: [PATCH 08/16] feat(Mathlib/Data/Finite/Subtype): Subtype of elements not equal to a term is finite iff type is finite --- Mathlib/Data/Finite/Subtype.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 Mathlib/Data/Finite/Subtype.lean diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean new file mode 100644 index 00000000000000..29527be166ae74 --- /dev/null +++ b/Mathlib/Data/Finite/Subtype.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Alex Brodbelt. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex Brodbelt and Eric Wieser +-/ +module + +public import Mathlib.Data.Finite.Option + +@[expose] public section + +@[simp] +theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by + classical + rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff] + +#min_imports From 0f8f3853a9af7d4761d724963b4df97c72aa9bd5 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:13:36 +0200 Subject: [PATCH 09/16] remove min imports command --- Mathlib/Data/Finite/Subtype.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean index 29527be166ae74..9b90419fe6a054 100644 --- a/Mathlib/Data/Finite/Subtype.lean +++ b/Mathlib/Data/Finite/Subtype.lean @@ -13,5 +13,3 @@ public import Mathlib.Data.Finite.Option theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by classical rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff] - -#min_imports From 0fcbb1c32361da6dd2b2cce945129df50b5eb11f Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 12:01:20 +0200 Subject: [PATCH 10/16] add file to Mathlib.lean and add docstrings --- Mathlib.lean | 1 + Mathlib/Data/Finite/Subtype.lean | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib.lean b/Mathlib.lean index 76ae6b4dedc9ff..c90036a1249b8b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3825,6 +3825,7 @@ public import Mathlib.Data.Finite.Perm public import Mathlib.Data.Finite.Prod public import Mathlib.Data.Finite.Set public import Mathlib.Data.Finite.Sigma +public import Mathlib.Data.Finite.Subtype public import Mathlib.Data.Finite.Sum public import Mathlib.Data.Finite.Vector public import Mathlib.Data.Finmap diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean index 9b90419fe6a054..c64ba014405be4 100644 --- a/Mathlib/Data/Finite/Subtype.lean +++ b/Mathlib/Data/Finite/Subtype.lean @@ -1,14 +1,19 @@ /- Copyright (c) 2026 Alex Brodbelt. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex Brodbelt and Eric Wieser +Authors: Alex Brodbelt, Eric Wieser -/ module public import Mathlib.Data.Finite.Option +/-! +# Finitiness conditions on subtypes +-/ + @[expose] public section +/-- The subtype of terms not equal to a given term is finite if and only if the type is finite -/ @[simp] theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by classical From 7531e4e3b2ad857487278d9439272384c3d9a462 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 12:36:42 +0200 Subject: [PATCH 11/16] follow modifications from review --- Mathlib/Data/Finite/Option.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean index 5fedbe9aa34088..6f61edb051e576 100644 --- a/Mathlib/Data/Finite/Option.lean +++ b/Mathlib/Data/Finite/Option.lean @@ -6,17 +6,18 @@ Authors: Alex Brodbelt, Eric Wieser module public import Mathlib.Data.Fintype.Option -public import Mathlib.Logic.Equiv.Fin.Basic +import Mathlib.Logic.Equiv.Fin.Basic /-! # Finiteness conditions for `Option` types -/ -@[expose] public section -/-- The `Option` type on a type is finite if and only if the underlying type is finite -/ +public section + +/-- The `Option` type on a type is finite if and only if the underlying type is finite. -/ @[simp] theorem Option.finite_iff {α : Type*} : Finite (Option α) ↔ Finite α where - mpr _ := instFiniteOption + mpr _ := inferInstance mp | @Finite.intro _ 0 e => (e none).elim0 | @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩ From 81b6c468a201107d81fdc00bdeb8f5ff65edbff5 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:05:09 +0200 Subject: [PATCH 12/16] feat(Mathlib/Data/Finite/Subtype): Subtype of elements not equal to a term is finite iff type is finite --- Mathlib/Data/Finite/Subtype.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 Mathlib/Data/Finite/Subtype.lean diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean new file mode 100644 index 00000000000000..29527be166ae74 --- /dev/null +++ b/Mathlib/Data/Finite/Subtype.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Alex Brodbelt. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex Brodbelt and Eric Wieser +-/ +module + +public import Mathlib.Data.Finite.Option + +@[expose] public section + +@[simp] +theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by + classical + rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff] + +#min_imports From bba11000f075663f021d011c00fb3b337eb2f0f6 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 11:13:36 +0200 Subject: [PATCH 13/16] remove min imports command --- Mathlib/Data/Finite/Subtype.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean index 29527be166ae74..9b90419fe6a054 100644 --- a/Mathlib/Data/Finite/Subtype.lean +++ b/Mathlib/Data/Finite/Subtype.lean @@ -13,5 +13,3 @@ public import Mathlib.Data.Finite.Option theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by classical rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff] - -#min_imports From f4297c9604bc38268fbb82e45517fc15f509290e Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 12:01:20 +0200 Subject: [PATCH 14/16] add file to Mathlib.lean and add docstrings --- Mathlib.lean | 1 + Mathlib/Data/Finite/Subtype.lean | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib.lean b/Mathlib.lean index 76ae6b4dedc9ff..c90036a1249b8b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3825,6 +3825,7 @@ public import Mathlib.Data.Finite.Perm public import Mathlib.Data.Finite.Prod public import Mathlib.Data.Finite.Set public import Mathlib.Data.Finite.Sigma +public import Mathlib.Data.Finite.Subtype public import Mathlib.Data.Finite.Sum public import Mathlib.Data.Finite.Vector public import Mathlib.Data.Finmap diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean index 9b90419fe6a054..c64ba014405be4 100644 --- a/Mathlib/Data/Finite/Subtype.lean +++ b/Mathlib/Data/Finite/Subtype.lean @@ -1,14 +1,19 @@ /- Copyright (c) 2026 Alex Brodbelt. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex Brodbelt and Eric Wieser +Authors: Alex Brodbelt, Eric Wieser -/ module public import Mathlib.Data.Finite.Option +/-! +# Finitiness conditions on subtypes +-/ + @[expose] public section +/-- The subtype of terms not equal to a given term is finite if and only if the type is finite -/ @[simp] theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by classical From bb97a2a2e6af1ae5d1f488faa19fe0710b224306 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 12:42:49 +0200 Subject: [PATCH 15/16] fix typos and styling --- Mathlib/Data/Finite/Subtype.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean index c64ba014405be4..20abfc7f965434 100644 --- a/Mathlib/Data/Finite/Subtype.lean +++ b/Mathlib/Data/Finite/Subtype.lean @@ -8,12 +8,12 @@ module public import Mathlib.Data.Finite.Option /-! -# Finitiness conditions on subtypes +# `Finite`ness conditions on subtypes -/ @[expose] public section -/-- The subtype of terms not equal to a given term is finite if and only if the type is finite -/ +/-- The subtype of terms not equal to a given term is finite if and only if the type is finite. -/ @[simp] theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by classical From b74f87e54e6638a6fd6499588b46413148c3bd54 Mon Sep 17 00:00:00 2001 From: AlexBrodbelt Date: Tue, 19 May 2026 12:44:41 +0200 Subject: [PATCH 16/16] fix typose and styling --- Mathlib/Data/Finite/Subtype.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean index 20abfc7f965434..3095571b4d4d1e 100644 --- a/Mathlib/Data/Finite/Subtype.lean +++ b/Mathlib/Data/Finite/Subtype.lean @@ -11,7 +11,7 @@ public import Mathlib.Data.Finite.Option # `Finite`ness conditions on subtypes -/ -@[expose] public section +public section /-- The subtype of terms not equal to a given term is finite if and only if the type is finite. -/ @[simp]