diff --git a/Mathlib.lean b/Mathlib.lean
index 51a2d9e682d0ca..c90036a1249b8b 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean
new file mode 100644
index 00000000000000..6f61edb051e576
--- /dev/null
+++ b/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⟩
diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean
new file mode 100644
index 00000000000000..3095571b4d4d1e
--- /dev/null
+++ b/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]