chore: tidy various files (#21475)

Author: Ruben-VandeVelde

Mathlib/Algebra/BigOperators/Fin.lean

@@ -392,10 +392,10 @@ def finSigmaFinEquiv {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) 
 @[simp]
 theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) :
     (finSigmaFinEquiv k : ℕ) = ∑ i : Fin k.1, n (Fin.castLE k.1.2.le i) + k.2 := by
-  induction m
-  · exact k.fst.elim0
-  rename_i m ih
-  rcases k with ⟨⟨iv,hi⟩,j⟩
+  induction m with
+  | zero => exact k.fst.elim0
+  | succ m ih =>
+  rcases k with ⟨⟨iv, hi⟩, j⟩
   rw [finSigmaFinEquiv]
   unfold finSumFinEquiv
   simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.instTrans_trans,

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -434,9 +434,9 @@ isomorphic"]
 def freeMonoidCongr (e : α ≃ β) :  FreeMonoid α ≃* FreeMonoid β where
   toFun := FreeMonoid.map ⇑e
   invFun := FreeMonoid.map ⇑e.symm
-  left_inv := fun _ => map_symm_apply_map_eq e
-  right_inv := fun _ => map_apply_map_symm_eq e
-  map_mul' := (by simp [map_mul])
+  left_inv _ := map_symm_apply_map_eq e
+  right_inv _ := map_apply_map_symm_eq e
+  map_mul' := by simp [map_mul]
 
 @[to_additive (attr := simp)]
 theorem freeMonoidCongr_of (e : α ≃ β) (a : α) : freeMonoidCongr e (of a) = of (e a) := rfl

Mathlib/Algebra/Homology/Embedding/Basic.lean

@@ -219,9 +219,7 @@ lemma not_mem_range_embeddingUpIntLE_iff (n : ℤ) :
   constructor
   · intro h
     by_contra!
-    simp only [Int.not_lt] at this
-    obtain ⟨k, rfl⟩ := Int.le.dest this
-    exact (h k) (by simp)
+    exact h (p - n).natAbs (by simp; omega)
   · intros
     dsimp
     omega
@@ -231,9 +229,7 @@ lemma not_mem_range_embeddingUpIntGE_iff (n : ℤ) :
   constructor
   · intro h
     by_contra!
-    simp only [Int.not_lt] at this
-    obtain ⟨k, rfl⟩ := Int.le.dest this
-    exact (h k) (by simp)
+    exact h (n - p).natAbs (by simp; omega)
   · intros
     dsimp
     omega

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -294,7 +294,7 @@ def quasiIso [CategoryWithHomology C] :
 variable {C c} [CategoryWithHomology C]
 
 @[simp]
-lemma mem_quasiIso_iff  (f : K ⟶ L) : quasiIso C c f ↔ QuasiIso f := by rfl
+lemma mem_quasiIso_iff (f : K ⟶ L) : quasiIso C c f ↔ QuasiIso f := by rfl
 
 instance : (quasiIso C c).IsMultiplicative where
   id_mem _ := by

Mathlib/Algebra/MonoidAlgebra/Division.lean

@@ -69,14 +69,14 @@ theorem zero_divOf (g : G) : (0 : k[G]) /ᵒᶠ g = 0 :=
 
 @[simp]
 theorem divOf_zero (x : k[G]) : x /ᵒᶠ 0 = x := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` doesn't work
+  ext
   simp only [AddMonoidAlgebra.divOf_apply, zero_add]
 
 theorem add_divOf (x y : k[G]) (g : G) : (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g :=
   map_add (Finsupp.comapDomain.addMonoidHom _) _ _
 
 theorem divOf_add (x : k[G]) (a b : G) : x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` doesn't work
+  ext
   simp only [AddMonoidAlgebra.divOf_apply, add_assoc]
 
 /-- A bundled version of `AddMonoidAlgebra.divOf`. -/
@@ -93,13 +93,13 @@ noncomputable def divOfHom : Multiplicative G →* AddMonoid.End k[G] where
         (divOf_add _ _ _)
 
 theorem of'_mul_divOf (a : G) (x : k[G]) : of' k G a * x /ᵒᶠ a = x := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` doesn't work
+  ext
   rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
   intro c hc
   exact add_right_inj _
 
 theorem mul_of'_divOf (x : k[G]) (a : G) : x * of' k G a /ᵒᶠ a = x := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` doesn't work
+  ext
   rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]
   intro c hc
   rw [add_comm]
@@ -133,14 +133,14 @@ theorem modOf_apply_self_add (x : k[G]) (g : G) (d : G) : (x %ᵒᶠ g) (g + d)
   modOf_apply_of_exists_add _ _ _ ⟨_, rfl⟩
 
 theorem of'_mul_modOf (g : G) (x : k[G]) : of' k G g * x %ᵒᶠ g = 0 := by
-  refine Finsupp.ext fun g' => ?_  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext g'` doesn't work
+  ext g'
   rw [Finsupp.zero_apply]
   obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
   · rw [modOf_apply_self_add]
   · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
 
 theorem mul_of'_modOf (x : k[G]) (g : G) : x * of' k G g %ᵒᶠ g = 0 := by
-  refine Finsupp.ext fun g' => ?_  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext g'` doesn't work
+  ext g'
   rw [Finsupp.zero_apply]
   obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
   · rw [modOf_apply_self_add]
@@ -152,7 +152,7 @@ theorem of'_modOf (g : G) : of' k G g %ᵒᶠ g = 0 := by
 
 theorem divOf_add_modOf (x : k[G]) (g : G) :
     of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x := by
-  refine Finsupp.ext fun g' => ?_  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` doesn't work
+  ext g'
   rw [Finsupp.add_apply] -- Porting note: changed from `simp_rw` which can't see through the type
   obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
   swap

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -321,7 +321,7 @@ lemma isoSpec_hom : hU.isoSpec.hom = U.toSpecΓ := rfl
 lemma toSpecΓ_isoSpec_inv : U.toSpecΓ ≫ hU.isoSpec.inv = 𝟙 _ := hU.isoSpec.hom_inv_id
 
 @[reassoc (attr := simp)]
-lemma isoSpec_inv_toSpecΓ :  hU.isoSpec.inv ≫ U.toSpecΓ = 𝟙 _ := hU.isoSpec.inv_hom_id
+lemma isoSpec_inv_toSpecΓ : hU.isoSpec.inv ≫ U.toSpecΓ = 𝟙 _ := hU.isoSpec.inv_hom_id
 
 open IsLocalRing in
 lemma isoSpec_hom_base_apply (x : U) :

Mathlib/Analysis/Analytic/Basic.lean

@@ -335,11 +335,10 @@ theorem radius_le_smul {p : FormalMultilinearSeries 𝕜 E F} {c : 𝕜} : p.rad
   gcongr
   exact h n
 
-theorem radius_smul_eq (p : FormalMultilinearSeries 𝕜 E F) {c : 𝕜}
-    (hc : c ≠ 0) : (c • p).radius = p.radius := by
+theorem radius_smul_eq (p : FormalMultilinearSeries 𝕜 E F) {c : 𝕜} (hc : c ≠ 0) :
+    (c • p).radius = p.radius := by
   apply eq_of_le_of_le _ radius_le_smul
-  conv => rhs; rw [show p = c⁻¹ • (c • p) by simp [smul_smul, inv_mul_cancel₀ hc]]
-  apply radius_le_smul
+  exact radius_le_smul.trans_eq (congr_arg _ <| inv_smul_smul₀ hc p)
 
 @[simp]
 theorem radius_shift (p : FormalMultilinearSeries 𝕜 E F) : p.shift.radius = p.radius := by

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

@@ -392,11 +392,7 @@ lemma CStarAlgebra.spectralOrderedRing : @StarOrderedRing A _ (CStarAlgebra.spec
         refine ⟨s * s, ?_, by rwa [eq_sub_iff_add_eq', eq_comm] at hs₂⟩
         exact AddSubmonoid.subset_closure ⟨s, by simp [hs₁.star_eq, sq]⟩
       · rintro ⟨p, hp, rfl⟩
-        show IsSelfAdjoint (x + p - x) ∧
-          QuasispectrumRestricts (x + p - x) ContinuousMap.realToNNReal
-        simp only [add_sub_cancel_left]
-        --suffices IsSelfAdjoint p ∧ SpectrumRestricts p ContinuousMap.realToNNReal from
-          --⟨by simpa using this.1, by simpa using this.2⟩
+        simp only [spectralOrder, add_sub_cancel_left]
         induction hp using AddSubmonoid.closure_induction with
         | mem x hx =>
           obtain ⟨s, rfl⟩ := hx

Mathlib/Data/Finset/Filter.lean

@@ -212,10 +212,8 @@ lemma _root_.Set.pairwiseDisjoint_filter [DecidableEq β] (f : α → β) (s : S
 theorem disjoint_filter_and_not_filter :
     Disjoint (s.filter (fun x ↦ p x ∧ ¬q x)) (s.filter (fun x ↦ q x ∧ ¬p x)) := by
   intro _ htp htq
-  simp [bot_eq_empty, le_eq_subset, subset_empty]
-  by_contra hn
-  rw [← not_nonempty_iff_eq_empty, not_not] at hn
-  obtain ⟨_, hx⟩ := hn
+  simp only [bot_eq_empty, le_eq_subset, subset_empty, ← not_nonempty_iff_eq_empty]
+  rintro ⟨_, hx⟩
   exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1
 
 variable {p q}

Mathlib/Data/Finset/Lattice/Fold.lean

@@ -650,9 +650,9 @@ theorem sup_mem_of_nonempty (hs : s.Nonempty) : s.sup f ∈ f '' s := by
   | empty => exfalso; simp only [Finset.not_nonempty_empty] at hs
   | @insert a s _ h =>
     rw [Finset.sup_insert (b := a) (s := s) (f := f)]
-    by_cases hs : s = ∅
-    · simp [hs]
-    · rw [← ne_eq, ← Finset.nonempty_iff_ne_empty] at hs
+    cases s.eq_empty_or_nonempty with
+    | inl hs => simp [hs]
+    | inr hs =>
       simp only [Finset.coe_insert]
       rcases le_total (f a) (s.sup f) with (ha | ha)
       · rw [sup_eq_right.mpr ha]