chore: deprime induction for localizations and quotients

Mathlib/Algebra/Module/LocalizedModule/Basic.lean

@@ -150,9 +150,7 @@ theorem mk_add_mk {m1 m2 : M} {s1 s2 : S} :
   mk_eq.mpr <| ⟨1, rfl⟩
 
 private theorem add_assoc' (x y z : LocalizedModule S M) : x + y + z = x + (y + z) := by
-  induction' x with mx sx
-  induction' y with my sy
-  induction' z with mz sz
+  cases x; cases y; cases z; rename_i mx sx my sy mz sz
   simp only [mk_add_mk, smul_add]
   refine mk_eq.mpr ⟨1, ?_⟩
   rw [one_smul, one_smul]
@@ -329,20 +327,19 @@ theorem mk_smul_mk (r : R) (m : M) (s t : S) :
 variable {T}
 
 private theorem one_smul_aux (p : LocalizedModule S M) : (1 : T) • p = p := by
-  induction' p with m s
+  cases p
   rw [show (1 : T) = IsLocalization.mk' T (1 : R) (1 : S) by rw [IsLocalization.mk'_one, map_one]]
   rw [mk'_smul_mk, one_smul, one_mul]
 
 private theorem mul_smul_aux (x y : T) (p : LocalizedModule S M) :
     (x * y) • p = x • y • p := by
-  induction' p with m s
+  cases p
   rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y]
   simp_rw [← IsLocalization.mk'_mul, mk'_smul_mk, ← mul_smul, mul_assoc]
 
 private theorem smul_add_aux (x : T) (p q : LocalizedModule S M) :
     x • (p + q) = x • p + x • q := by
-  induction' p with m s
-  induction' q with n t
+  cases p; cases q
   rw [smul_def, smul_def, mk_add_mk, mk_add_mk]
   rw [show x • _ =  IsLocalization.mk' T _ _ • _ by rw [IsLocalization.mk'_sec (M := S) T]]
   rw [← IsLocalization.mk'_cancel _ _ (IsLocalization.sec S x).2, mk'_smul_mk]
@@ -355,7 +352,7 @@ private theorem smul_zero_aux (x : T) : x • (0 : LocalizedModule S M) = 0 := b
 
 private theorem add_smul_aux (x y : T) (p : LocalizedModule S M) :
     (x + y) • p = x • p + y • p := by
-  induction' p with m s
+  cases p with | _ m s => ?_
   rw [smul_def T x, smul_def T y, mk_add_mk, show (x + y) • _ =  IsLocalization.mk' T _ _ • _ by
     rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
       ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s], mk'_smul_mk, ← smul_assoc,
@@ -365,7 +362,7 @@ private theorem add_smul_aux (x y : T) (p : LocalizedModule S M) :
   · rw [mul_mul_mul_comm, mul_assoc] -- ring does not work here
 
 private theorem zero_smul_aux (p : LocalizedModule S M) : (0 : T) • p = 0 := by
-  induction' p with m s
+  cases p
   rw [show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],
     mk'_smul_mk, zero_smul, zero_mk]
 
@@ -449,7 +446,7 @@ theorem algebraMap_mk {A : Type*} [Semiring A] [Algebra R A] (a : R) (s : S) :
 
 instance : IsScalarTower R T (LocalizedModule S M) where
   smul_assoc r x p := by
-    induction' p with m s
+    cases p
     rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
       smul'_mk, mul_smul]
 
@@ -689,7 +686,7 @@ If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S
 theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
     (l : LocalizedModule S M →ₗ[R] M'') (hl : l.comp (LocalizedModule.mkLinearMap S M) = g) :
     LocalizedModule.lift S g h = l := by
-  ext x; induction' x with m s
+  ext x; cases x
   rw [LocalizedModule.lift_mk]
   rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp,
     Function.comp_apply, LocalizedModule.mkLinearMap_apply, ← l.map_smul, LocalizedModule.smul'_mk]
@@ -807,8 +804,7 @@ theorem fromLocalizedModule_mk (m : M) (s : S) :
   rfl
 
 theorem fromLocalizedModule.inj : Function.Injective <| fromLocalizedModule S f := fun x y eq1 => by
-  induction' x with a b
-  induction' y with a' b'
+  cases x; cases y
   simp only [fromLocalizedModule_mk] at eq1
   rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← LinearMap.map_smul,
     Module.End_algebraMap_isUnit_inv_apply_eq_iff'] at eq1

Mathlib/Algebra/Pointwise/Stabilizer.lean

@@ -250,7 +250,7 @@ local notation " q " => ((↑) : G → Q)
 @[to_additive]
 lemma stabilizer_image_coe_quotient : stabilizer Q (q '' s) = ⊥ := by
   ext a
-  induction' a using QuotientGroup.induction_on with a
+  induction a using QuotientGroup.induction_on with | _ a => ?_
   simp only [mem_stabilizer_iff, Subgroup.mem_bot, QuotientGroup.eq_one_iff]
   have : q a • q '' s = q '' (a • s) :=
     (image_smul_distrib (QuotientGroup.mk' <| stabilizer G s) _ _).symm

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -181,7 +181,7 @@ noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ Circle :=
 
 theorem homeomorphCircle_apply (hT : T ≠ 0) (x : AddCircle T) :
     homeomorphCircle hT x = toCircle x := by
-  induction' x using QuotientAddGroup.induction_on with x
+  induction x using QuotientAddGroup.induction_on
   rw [homeomorphCircle, Homeomorph.trans_apply,
     homeomorphAddCircle_apply_mk, homeomorphCircle'_apply_mk, toCircle_apply_mk]
   ring_nf

Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

@@ -231,7 +231,7 @@ theorem _root_.Real.list_prod_map_rpow' {ι} (l : List ι) (f : ι → ℝ)
 theorem _root_.Real.multiset_prod_map_rpow {ι} (s : Multiset ι) (f : ι → ℝ)
     (hs : ∀ i ∈ s, (0 : ℝ) ≤ f i) (r : ℝ) :
     (s.map (f · ^ r)).prod = (s.map f).prod ^ r := by
-  induction' s using Quotient.inductionOn with l
+  obtain ⟨l⟩ := s
   simpa using Real.list_prod_map_rpow' l f hs r
 
 /-- `rpow` version of `Finset.prod_pow`. -/

Mathlib/CategoryTheory/Action/Concrete.lean

@@ -109,7 +109,7 @@ def toEndHom [N.Normal] : G →* End (G ⧸ₐ N) where
       simpa [mul_assoc] using Subgroup.Normal.conj_mem ‹_› _ (QuotientGroup.leftRel_apply.mp h) _
     comm := fun (g : G) ↦ by
       ext (x : G ⧸ N)
-      induction' x using Quotient.inductionOn with x
+      obtain ⟨x⟩ := x
       simp only [FintypeCat.comp_apply, Action.FintypeCat.ofMulAction_apply, Quotient.lift_mk]
       show Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) _ (⟦g • x⟧) = _
       simp only [smul_eq_mul, Quotient.lift_mk, mul_assoc]
@@ -118,12 +118,12 @@ def toEndHom [N.Normal] : G →* End (G ⧸ₐ N) where
   map_one' := by
     apply Action.hom_ext
     ext (x : G ⧸ N)
-    induction' x using Quotient.inductionOn with x
+    induction x using Quotient.inductionOn
     simp
   map_mul' σ τ := by
     apply Action.hom_ext
     ext (x : G ⧸ N)
-    induction' x using Quotient.inductionOn with x
+    obtain ⟨x⟩ := x
     show ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
     rw [mul_inv_rev, mul_assoc]
 
@@ -134,7 +134,7 @@ variable {N} in
 lemma toEndHom_trivial_of_mem [N.Normal] {n : G} (hn : n ∈ N) : toEndHom N n = 𝟙 (G ⧸ₐ N) := by
   apply Action.hom_ext
   ext (x : G ⧸ N)
-  induction' x using Quotient.inductionOn with μ
+  obtain ⟨μ⟩ := x
   exact Quotient.sound ((QuotientGroup.leftRel_apply).mpr <| by simpa)
 
 /-- If `H` and `N` are subgroups of a group `G` with `N` normal, there is a canonical
@@ -155,7 +155,7 @@ def quotientToQuotientOfLE [Fintype (G ⧸ H)] (h : N ≤ H) : (G ⧸ₐ N) ⟶
     (QuotientGroup.leftRel_apply).mpr (h <| (QuotientGroup.leftRel_apply).mp hab)
   comm g := by
     ext (x : G ⧸ N)
-    induction' x using Quotient.inductionOn with μ
+    obtain ⟨μ⟩ := x
     rfl
 
 @[simp]

Mathlib/CategoryTheory/Galois/EssSurj.lean

@@ -152,7 +152,7 @@ private def coconeQuotientDiag :
     rw [← cancel_epi (u.inv), Iso.inv_hom_id_assoc]
     apply Action.hom_ext
     ext (x : Aut F ⧸ U.toSubgroup)
-    induction' m, x using Quotient.inductionOn₂ with σ μ
+    induction m, x using Quotient.inductionOn₂ with | _ σ μ => ?_
     suffices h : ⟦μ * σ⁻¹⟧ = ⟦μ⟧ by
       simp only [quotientToQuotientOfLE_hom_mk, quotientDiag_map,
         functorToAction_map_quotientToEndObjectHom V _ u]
@@ -179,7 +179,7 @@ private def coconeQuotientDiagDesc
     simp only [← h2, const_obj_obj, Action.comp_hom, FintypeCat.comp_apply]
   comm g := by
     ext (x : Aut F ⧸ V.toSubgroup)
-    induction' x using Quotient.inductionOn with σ
+    obtain ⟨σ⟩ := x
     simp only [const_obj_obj]
     show (((Aut F ⧸ₐ U.toSubgroup).ρ g ≫ u.inv.hom) ≫ (s.ι.app (SingleObj.star _)).hom) ⟦σ⟧ =
       ((s.ι.app (SingleObj.star _)).hom ≫ s.pt.ρ g) (u.inv.hom ⟦σ⟧)
@@ -197,13 +197,13 @@ private def coconeQuotientDiagIsColimit :
     apply (cancel_epi u.inv).mp
     apply Action.hom_ext
     ext (x : Aut F ⧸ U.toSubgroup)
-    induction' x using Quotient.inductionOn with σ
+    obtain ⟨σ⟩ := x
     simp
     rfl
   uniq s f hf := by
     apply Action.hom_ext
     ext (x : Aut F ⧸ V.toSubgroup)
-    induction' x using Quotient.inductionOn with σ
+    induction x using Quotient.inductionOn
     simp [← hf (SingleObj.star _)]
 
 end
@@ -224,7 +224,7 @@ lemma exists_lift_of_quotient_openSubgroup (V : OpenSubgroup (Aut F)) :
   have h1 (σ : Aut F) (σinU : σ ∈ U) : σ.hom.app A = 𝟙 (F.obj A) := by
     have hi : (Aut F ⧸ₐ MulAction.stabilizer (Aut F) a).ρ σ = 𝟙 _ := by
       refine FintypeCat.hom_ext _ _ (fun x ↦ ?_)
-      induction' x using Quotient.inductionOn with τ
+      obtain ⟨τ⟩ := x
       show ⟦σ * τ⟧ = ⟦τ⟧
       apply Quotient.sound
       apply (QuotientGroup.leftRel_apply).mpr

Mathlib/CategoryTheory/Limits/Types/Colimits.lean

@@ -227,7 +227,7 @@ def colimitCoconeIsColimit (F : J ⥤ Type max v u) : IsColimit (colimitCocone F
       exact (congr_fun (Cocone.w s f) x).symm
   uniq s m hm := by
     funext x
-    induction' x using Quot.ind with x
+    obtain ⟨x⟩ := x
     exact congr_fun (hm x.1) x.2
 
 end TypeMax

Mathlib/CategoryTheory/Subobject/Basic.lean

@@ -533,12 +533,12 @@ def pullback (f : X ⟶ Y) : Subobject Y ⥤ Subobject X :=
   lower (MonoOver.pullback f)
 
 theorem pullback_id (x : Subobject X) : (pullback (𝟙 X)).obj x = x := by
-  induction' x using Quotient.inductionOn' with f
+  obtain ⟨f⟩ := x
   exact Quotient.sound ⟨MonoOver.pullbackId.app f⟩
 
 theorem pullback_comp (f : X ⟶ Y) (g : Y ⟶ Z) (x : Subobject Z) :
     (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x) := by
-  induction' x using Quotient.inductionOn' with t
+  obtain ⟨t⟩ := x
   exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩
 
 theorem pullback_obj_mk {A B X Y : C} {f : Y ⟶ X} {i : A ⟶ X} [Mono i]
@@ -572,19 +572,19 @@ lemma map_mk {A X Y : C} (i : A ⟶ X) [Mono i] (f : X ⟶ Y) [Mono f] :
   rfl
 
 theorem map_id (x : Subobject X) : (map (𝟙 X)).obj x = x := by
-  induction' x using Quotient.inductionOn' with f
+  obtain ⟨f⟩ := x
   exact Quotient.sound ⟨(MonoOver.mapId _).app f⟩
 
 theorem map_comp (f : X ⟶ Y) (g : Y ⟶ Z) [Mono f] [Mono g] (x : Subobject X) :
     (map (f ≫ g)).obj x = (map g).obj ((map f).obj x) := by
-  induction' x using Quotient.inductionOn' with t
+  obtain ⟨t⟩ := x
   exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩
 
 lemma map_obj_injective {X Y : C} (f : X ⟶ Y) [Mono f] :
     Function.Injective (Subobject.map f).obj := by
   intro X₁ X₂ h
-  induction' X₁ using Subobject.ind with X₁ i₁ _
-  induction' X₂ using Subobject.ind with X₂ i₂ _
+  induction X₁ using Subobject.ind
+  induction X₂ using Subobject.ind
   simp only [map_mk] at h
   exact mk_eq_mk_of_comm _ _ (isoOfMkEqMk _ _ h) (by simp [← cancel_mono f])
 

Mathlib/CategoryTheory/Subobject/FactorThru.lean

@@ -84,7 +84,7 @@ theorem factors_comp_arrow {X Y : C} {P : Subobject Y} (f : X ⟶ P) : P.Factors
 
 theorem factors_of_factors_right {X Y Z : C} {P : Subobject Z} (f : X ⟶ Y) {g : Y ⟶ Z}
     (h : P.Factors g) : P.Factors (f ≫ g) := by
-  induction' P using Quotient.ind' with P
+  obtain ⟨P⟩ := P
   obtain ⟨g, rfl⟩ := h
   exact ⟨f ≫ g, by simp⟩
 

Mathlib/CategoryTheory/Subobject/Lattice.lean

@@ -410,7 +410,7 @@ theorem finset_inf_arrow_factors {I : Type*} {B : C} (s : Finset I) (P : I → S
 theorem inf_eq_map_pullback' {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) :
     (Subobject.inf.obj (Quotient.mk'' f₁)).obj f₂ =
       (Subobject.map f₁.arrow).obj ((Subobject.pullback f₁.arrow).obj f₂) := by
-  induction' f₂ using Quotient.inductionOn' with f₂
+  obtain ⟨f₂⟩ := f₂
   rfl
 
 theorem inf_eq_map_pullback {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) :

Mathlib/Data/Finset/NoncommProd.lean

@@ -129,7 +129,7 @@ theorem noncommProd_cons (s : Multiset α) (a : α) (comm) :
 @[to_additive]
 theorem noncommProd_cons' (s : Multiset α) (a : α) (comm) :
     noncommProd (a ::ₘ s) comm = noncommProd s (comm.mono fun _ => mem_cons_of_mem) * a := by
-  induction' s using Quotient.inductionOn with s
+  induction s using Quotient.inductionOn with | _ s => ?_
   simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
   induction' s with hd tl IH
   · simp
@@ -155,7 +155,7 @@ theorem noncommProd_add (s t : Multiset α) (comm) :
 lemma noncommProd_induction (s : Multiset α) (comm)
     (p : α → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p x) :
     p (s.noncommProd comm) := by
-  induction' s using Quotient.inductionOn with l
+  induction s using Quotient.inductionOn with | _ l => ?_
   simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢
   exact l.prod_induction p hom unit base
 
@@ -197,7 +197,7 @@ theorem noncommProd_commute (s : Multiset α) (comm) (y : α) (h : ∀ x ∈ s,
 theorem mul_noncommProd_erase [DecidableEq α] (s : Multiset α) {a : α} (h : a ∈ s) (comm)
     (comm' := fun _ hx _ hy hxy ↦ comm (s.mem_of_mem_erase hx) (s.mem_of_mem_erase hy) hxy) :
     a * (s.erase a).noncommProd comm' = s.noncommProd comm := by
-  induction' s using Quotient.inductionOn with l
+  induction s using Quotient.inductionOn with | _ l => ?_
   simp only [quot_mk_to_coe, mem_coe, coe_erase, noncommProd_coe] at comm h ⊢
   suffices ∀ x ∈ l, ∀ y ∈ l, x * y = y * x by rw [List.prod_erase_of_comm h this]
   intro x hx y hy

Mathlib/Data/Finsupp/BigOperators.lean

@@ -92,7 +92,7 @@ theorem List.support_sum_eq [AddZeroClass M] (l : List (ι →₀ M))
 theorem Multiset.support_sum_eq [AddCommMonoid M] (s : Multiset (ι →₀ M))
     (hs : s.Pairwise (_root_.Disjoint on Finsupp.support)) :
     s.sum.support = (s.map Finsupp.support).sup := by
-  induction' s using Quot.inductionOn with a
+  obtain ⟨a⟩ := s
   obtain ⟨l, hl, hd⟩ := hs
   suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
     convert List.support_sum_eq a this

Mathlib/Data/Fintype/Quotient.lean

@@ -58,7 +58,7 @@ lemma list_ind {l : List ι} {C : (∀ i ∈ l, Quotient (S i)) → Prop}
   |     [] => cast (congr_arg _ (funext₂ nofun)) (f nofun)
   | i :: l => by
     rw [← List.Pi.cons_eta q]
-    induction' List.Pi.head q using Quotient.ind with a
+    obtain ⟨a⟩ := List.Pi.head q
     refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)
     intro as
     rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]

Mathlib/Data/List/Cycle.lean

@@ -529,7 +529,7 @@ theorem subsingleton_reverse_iff {s : Cycle α} : s.reverse.Subsingleton ↔ s.S
 
 theorem Subsingleton.congr {s : Cycle α} (h : Subsingleton s) :
     ∀ ⦃x⦄ (_hx : x ∈ s) ⦃y⦄ (_hy : y ∈ s), x = y := by
-  induction' s using Quot.inductionOn with l
+  obtain ⟨l⟩ := s
   simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff,
     length_eq_zero_iff, length_eq_one_iff, Nat.not_lt_zero, false_or] at h
   rcases h with (rfl | ⟨z, rfl⟩) <;> simp
@@ -557,7 +557,7 @@ theorem nontrivial_reverse_iff {s : Cycle α} : s.reverse.Nontrivial ↔ s.Nontr
 
 theorem length_nontrivial {s : Cycle α} (h : Nontrivial s) : 2 ≤ length s := by
   obtain ⟨x, y, hxy, hx, hy⟩ := h
-  induction' s using Quot.inductionOn with l
+  obtain ⟨l⟩ := s
   rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
   · simp at hx
   · simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
@@ -581,7 +581,7 @@ theorem nodup_reverse_iff {s : Cycle α} : s.reverse.Nodup ↔ s.Nodup :=
   Quot.inductionOn s fun _ => nodup_reverse
 
 theorem Subsingleton.nodup {s : Cycle α} (h : Subsingleton s) : Nodup s := by
-  induction' s using Quot.inductionOn with l
+  obtain ⟨l⟩ := s
   obtain - | ⟨hd, tl⟩ := l
   · simp
   · have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h
@@ -677,9 +677,7 @@ instance {s : Cycle α} : Decidable (Nodup s) :=
 
 instance fintypeNodupCycle [Fintype α] : Fintype { s : Cycle α // s.Nodup } :=
   Fintype.ofSurjective (fun l : { l : List α // l.Nodup } => ⟨l.val, by simpa using l.prop⟩)
-    fun ⟨s, hs⟩ => by
-    induction' s using Quotient.inductionOn' with s hs
-    exact ⟨⟨s, hs⟩, by simp⟩
+    fun ⟨s, hs⟩ => by obtain ⟨hs⟩ := s; exact ⟨⟨_, hs⟩, by simp⟩
 
 instance fintypeNodupNontrivialCycle [Fintype α] :
     Fintype { s : Cycle α // s.Nodup ∧ s.Nontrivial } :=

Mathlib/Data/Nat/ChineseRemainder.lean

@@ -146,7 +146,7 @@ def chineseRemainderOfMultiset {m : Multiset ι} :
 theorem chineseRemainderOfMultiset_lt_prod {m : Multiset ι}
     (nod : m.Nodup) (hs : ∀ i ∈ m, s i ≠ 0) (pp : Set.Pairwise {x | x ∈ m} (Coprime on s)) :
     chineseRemainderOfMultiset a s nod hs pp < (m.map s).prod := by
-  induction' m using Quot.ind with l
+  obtain ⟨l⟩ := m
   unfold chineseRemainderOfMultiset
   simpa using chineseRemainderOfList_lt_prod a s l
     (List.Nodup.pairwise_of_forall_ne nod pp) (by simpa using hs)

Mathlib/Data/Setoid/Partition.lean

@@ -164,9 +164,7 @@ noncomputable def quotientEquivClasses (r : Setoid α) : Quotient r ≃ Setoid.c
         (Setoid.mem_classes r b) (Setoid.refl b)
   apply Equiv.ofBijective (Quot.lift f f_respects_relation)
   constructor
-  · intro (q_a : Quotient r) (q_b : Quotient r) h_eq
-    induction' q_a using Quotient.ind with a
-    induction' q_b using Quotient.ind with b
+  · rintro ⟨a⟩ ⟨b⟩ h_eq
     simp only [f, Quotient.lift_mk, Subtype.ext_iff] at h_eq
     apply Quotient.sound
     show a ∈ { x | r x b }