feat(Mathlib/Data/Finite/Subtype): Subtype of elements not equal to a term is finite iff type is finite

Mathlib.lean

@@ -3820,10 +3820,12 @@ 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
 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

Mathlib/Data/Finite/Option.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Alex Brodbelt. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Brodbelt, Eric Wieser
+-/
+module
+
+public import Mathlib.Data.Fintype.Option
+import Mathlib.Logic.Equiv.Fin.Basic
+
+/-!
+# Finiteness conditions for `Option` types
+-/
+
+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 _ := inferInstance
+  mp
+  | @Finite.intro _ 0 e => (e none).elim0
+  | @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩

Mathlib/Data/Finite/Subtype.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 Alex Brodbelt. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Brodbelt, Eric Wieser
+-/
+module
+
+public import Mathlib.Data.Finite.Option
+
+/-!
+# `Finite`ness conditions on subtypes
+-/
+
+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
+  rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff]