chore: review induction principles for Set.Finite (#20444)

Rename `Set.Finite.dinduction_on` to `Set.Finite.induction_on` as this is the more useful induction principle (it works with `induction`). Rename `Set.Finite.induction_on'` to `Set.Finite.induction_on_subset` and make it dependent. Give the assumptions meaningful names.

Author: YaelDillies

Mathlib/Data/Set/Card.lean

@@ -112,7 +112,7 @@ theorem encard_insert_of_not_mem {a : α} (has : a ∉ s) : (insert a s).encard
   rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]
 
 theorem Finite.encard_lt_top (h : s.Finite) : s.encard < ⊤ := by
-  refine h.induction_on (by simp) ?_
+  refine h.induction_on _ (by simp) ?_
   rintro a t hat _ ht'
   rw [encard_insert_of_not_mem hat]
   exact lt_tsub_iff_right.1 ht'

Mathlib/Data/Set/Finite/Basic.lean

@@ -668,31 +668,40 @@ theorem finite_option {s : Set (Option α)} : s.Finite ↔ { x : α | some x ∈
     ((h.image some).insert none).subset fun x =>
       x.casesOn (fun _ => Or.inl rfl) fun _ hx => Or.inr <| mem_image_of_mem _ hx⟩
 
+/-- Induction principle for finite sets: To prove a property `motive` of a finite set `s`, it's
+enough to prove for the empty set and to prove that `motive t → motive ({a} ∪ t)` for all `t`.
+
+See also `Set.Finite.induction_on` for the version requiring to check `motive t → motive ({a} ∪ t)`
+only for `t ⊆ s`. -/
 @[elab_as_elim]
-theorem Finite.induction_on {C : Set α → Prop} {s : Set α} (h : s.Finite) (H0 : C ∅)
-    (H1 : ∀ {a s}, a ∉ s → Set.Finite s → C s → C (insert a s)) : C s := by
-  lift s to Finset α using h
-  induction' s using Finset.cons_induction_on with a s ha hs
-  · rwa [Finset.coe_empty]
-  · rw [Finset.coe_cons]
-    exact @H1 a s ha (Set.toFinite _) hs
-
-/-- Analogous to `Finset.induction_on'`. -/
+theorem Finite.induction_on {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α) (hs : s.Finite)
+    (empty : motive ∅ finite_empty)
+    (insert : ∀ {a s}, a ∉ s →
+      ∀ hs : Set.Finite s, motive s hs → motive (insert a s) (hs.insert a)) :
+    motive s hs := by
+  lift s to Finset α using id hs
+  induction' s using Finset.cons_induction_on with a s ha ih
+  · simpa
+  · simpa using @insert a s ha (Set.toFinite _) (ih _)
+
+/-- Induction principle for finite sets: To prove a property `C` of a finite set `s`, it's enough
+to prove for the empty set and to prove that `C t → C ({a} ∪ t)` for all `t ⊆ s`.
+
+This is analogous to `Finset.induction_on'`. See also `Set.Finite.induction_on` for the version
+requiring `C t → C ({a} ∪ t)` for all `t`. -/
 @[elab_as_elim]
-theorem Finite.induction_on' {C : Set α → Prop} {S : Set α} (h : S.Finite) (H0 : C ∅)
-    (H1 : ∀ {a s}, a ∈ S → s ⊆ S → a ∉ s → C s → C (insert a s)) : C S := by
-  refine @Set.Finite.induction_on α (fun s => s ⊆ S → C s) S h (fun _ => H0) ?_ Subset.rfl
+theorem Finite.induction_on_subset {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α)
+    (hs : s.Finite) (empty : motive ∅ finite_empty)
+    (insert : ∀ {a t}, a ∈ s → ∀ hts : t ⊆ s, a ∉ t → motive t (hs.subset hts) →
+      motive (insert a t) ((hs.subset hts).insert a)) : motive s hs := by
+  refine Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs
+    (fun _ => empty) ?_ .rfl
   intro a s has _ hCs haS
   rw [insert_subset_iff] at haS
-  exact H1 haS.1 haS.2 has (hCs haS.2)
+  exact insert haS.1 haS.2 has (hCs haS.2)
 
-@[elab_as_elim]
-theorem Finite.dinduction_on {C : ∀ s : Set α, s.Finite → Prop} (s : Set α) (h : s.Finite)
-    (H0 : C ∅ finite_empty)
-    (H1 : ∀ {a s}, a ∉ s → ∀ h : Set.Finite s, C s h → C (insert a s) (h.insert a)) : C s h :=
-  have : ∀ h : s.Finite, C s h :=
-    Finite.induction_on h (fun _ => H0) fun has hs ih _ => H1 has hs (ih _)
-  this h
+@[deprecated (since := "2025-01-03")] alias Finite.induction_on' := Finite.induction_on_subset
+@[deprecated (since := "2025-01-03")] alias Finite.dinduction_on := Finite.induction_on
 
 section
 
@@ -908,9 +917,9 @@ theorem finite_range_findGreatest {P : α → ℕ → Prop} [∀ x, DecidablePre
 
 theorem Finite.exists_maximal_wrt [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite)
     (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a' := by
-  induction s, h using Set.Finite.dinduction_on with
-  | H0 => exact absurd hs not_nonempty_empty
-  | @H1 a s his _ ih =>
+  induction s, h using Set.Finite.induction_on with
+  | empty => exact absurd hs not_nonempty_empty
+  | @insert a s his _ ih =>
     rcases s.eq_empty_or_nonempty with h | h
     · use a
       simp [h]

Mathlib/Data/Set/Finite/Lattice.lean

@@ -276,9 +276,9 @@ lemma map_finite_iInf {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [
 theorem Finite.iSup_biInf_of_monotone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι']
     [IsDirected ι' (· ≤ ·)] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α}
     (hf : ∀ i ∈ s, Monotone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j := by
-  induction s, hs using Set.Finite.dinduction_on with
-  | H0 => simp [iSup_const]
-  | H1 _ _ ihs =>
+  induction s, hs using Set.Finite.induction_on with
+  | empty => simp [iSup_const]
+  | insert _ _ ihs =>
     rw [forall_mem_insert] at hf
     simp only [iInf_insert, ← ihs hf.2]
     exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj
@@ -361,12 +361,12 @@ variable [Preorder α] [IsDirected α (· ≤ ·)] [Nonempty α] {s : Set α}
 
 /-- A finite set is bounded above. -/
 protected theorem Finite.bddAbove (hs : s.Finite) : BddAbove s :=
-  Finite.induction_on hs bddAbove_empty fun _ _ h => h.insert _
+  Finite.induction_on _ hs bddAbove_empty fun _ _ h => h.insert _
 
 /-- A finite union of sets which are all bounded above is still bounded above. -/
 theorem Finite.bddAbove_biUnion {I : Set β} {S : β → Set α} (H : I.Finite) :
     BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i) :=
-  Finite.induction_on H (by simp only [biUnion_empty, bddAbove_empty, forall_mem_empty])
+  Finite.induction_on _ H (by simp only [biUnion_empty, bddAbove_empty, forall_mem_empty])
     fun _ _ hs => by simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]
 
 theorem infinite_of_not_bddAbove : ¬BddAbove s → s.Infinite :=

Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

@@ -110,11 +110,10 @@ theorem toSubalgebra_iSup_of_directed (dir : Directed (· ≤ ·) t) :
 instance finiteDimensional_iSup_of_finite [h : Finite ι] [∀ i, FiniteDimensional K (t i)] :
     FiniteDimensional K (⨆ i, t i : IntermediateField K L) := by
   rw [← iSup_univ]
-  let P : Set ι → Prop := fun s => FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L)
-  change P Set.univ
-  apply Set.Finite.induction_on
-  all_goals dsimp only [P]
-  · exact Set.finite_univ
+  refine Set.Finite.induction_on
+    (motive := fun s _ => FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L))
+    _ Set.finite_univ ?_ ?_
+  all_goals dsimp
   · rw [iSup_emptyset]
     exact (botEquiv K L).symm.toLinearEquiv.finiteDimensional
   · intro _ s _ _ hs

Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean

@@ -100,7 +100,7 @@ theorem exists_finite_submodule_of_finite (s : Set (M ⊗[R] N)) (hs : s.Finite)
     ∃ (M' : Submodule R M) (N' : Submodule R N), Module.Finite R M' ∧ Module.Finite R N' ∧
       s ⊆ LinearMap.range (mapIncl M' N') := by
   simp_rw [Module.Finite.iff_fg]
-  refine hs.induction_on ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩ ?_
+  refine hs.induction_on _ ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩ ?_
   rintro a s - - ⟨M', N', hM', hN', h⟩
   refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
   · exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -171,10 +171,8 @@ theorem integrableOn_singleton_iff {x : α} [MeasurableSingletonClass α] :
 
 @[simp]
 theorem integrableOn_finite_biUnion {s : Set β} (hs : s.Finite) {t : β → Set α} :
-    IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ := by
-  refine hs.induction_on ?_ ?_
-  · simp
-  · intro a s _ _ hf; simp [hf, or_imp, forall_and]
+    IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ :=
+  hs.induction_on _ (by simp) <| by intro a s _ _ hf; simp [hf, or_imp, forall_and]
 
 @[simp]
 theorem integrableOn_finset_iUnion {s : Finset β} {t : β → Set α} :

Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

@@ -264,7 +264,7 @@ theorem Set.Subsingleton.measurableSet {s : Set α} (hs : s.Subsingleton) : Meas
   hs.induction_on .empty .singleton
 
 theorem Set.Finite.measurableSet {s : Set α} (hs : s.Finite) : MeasurableSet s :=
-  Finite.induction_on hs MeasurableSet.empty fun _ _ hsm => hsm.insert _
+  Finite.induction_on _ hs .empty fun _ _ hsm => hsm.insert _
 
 @[measurability]
 protected theorem Finset.measurableSet (s : Finset α) : MeasurableSet (↑s : Set α) :=

Mathlib/NumberTheory/Cyclotomic/Basic.lean

@@ -301,7 +301,7 @@ protected theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExte
     Module.Finite A B := by
   cases' nonempty_fintype S with h
   revert h₂ A B
-  refine Set.Finite.induction_on h₁ (fun A B => ?_) @fun n S _ _ H A B => ?_
+  refine Set.Finite.induction_on _ h₁ (fun A B => ?_) @fun n S _ _ H A B => ?_
   · intro _ _ _ _ _
     refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩
     simp [← top_toSubmodule, ← empty, toSubmodule_bot, Submodule.one_eq_span]

Mathlib/Order/Filter/Finite.lean

@@ -25,7 +25,7 @@ variable {α : Type u} {f g : Filter α} {s t : Set α}
 @[simp]
 theorem biInter_mem {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Finite) :
     (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f :=
-  Finite.induction_on hf (by simp) fun _ _ hs => by simp [hs]
+  Finite.induction_on _ hf (by simp) fun _ _ hs => by simp [hs]
 
 @[simp]
 theorem biInter_finset_mem {β : Type v} {s : β → Set α} (is : Finset β) :

Mathlib/Order/Filter/Ultrafilter.lean

@@ -161,7 +161,7 @@ theorem eventually_imp : (∀ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) 
   simp only [imp_iff_not_or, eventually_or, eventually_not]
 
 theorem finite_sUnion_mem_iff {s : Set (Set α)} (hs : s.Finite) : ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f :=
-  Finite.induction_on hs (by simp) fun _ _ his => by
+  Finite.induction_on _ hs (by simp) fun _ _ his => by
     simp [union_mem_iff, his, or_and_right, exists_or]
 
 theorem finite_biUnion_mem_iff {is : Set β} {s : β → Set α} (his : is.Finite) :