chore: tidy various files (#10311)

Mathlib/Algebra/Associated.lean

@@ -621,7 +621,7 @@ lemma prime_pow_iff [CancelCommMonoidWithZero α] {p : α} {n : ℕ} :
     Prime (p ^ n) ↔ Prime p ∧ n = 1 := by
   refine ⟨fun hp ↦ ?_, fun ⟨hp, hn⟩ ↦ by simpa [hn]⟩
   suffices n = 1 by aesop
-  cases' n with n n
+  cases' n with n
   · simp at hp
   · rw [Nat.succ.injEq]
     rw [pow_succ, prime_mul_iff] at hp

Mathlib/Algebra/GroupPower/Basic.lean

@@ -425,7 +425,7 @@ theorem inv_pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^
 @[to_additive add_one_zsmul]
 lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
   | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_ofNat, pow_succ']
-  | -[0+1] => by erw [zpow_zero, zpow_negSucc, pow_one, mul_left_inv]
+  | -[0+1] => by simp [negSucc_eq', Int.add_left_neg]
   | -[n + 1+1] => by
     rw [zpow_negSucc, pow_succ, mul_inv_rev, inv_mul_cancel_right]
     rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -35,10 +35,10 @@ These actions are available in the `Pointwise` locale.
 
 For an `R`-module `M`, The action of a subset of `R` acting on a submodule of `M` introduced in
 section `set_acting_on_submodules` does not have a counterpart in
-`GroupTheory/Submonoid/Pointwise.lean`.
+`Mathlib/GroupTheory/Submonoid/Pointwise.lean`.
 
 Other than section `set_acting_on_submodules`, most of the lemmas in this file are direct copies of
-lemmas from `GroupTheory/Submonoid/Pointwise.lean`.
+lemmas from `Mathlib/GroupTheory/Submonoid/Pointwise.lean`.
 -/
 
 
@@ -447,7 +447,7 @@ lemma set_smul_eq_map [SMulCommClass R R N] :
         exact fun p hp ↦ hp hr hn
       · aesop
 
-lemma mem_set_smul(x : M) [SMulCommClass R R N] :
+lemma mem_set_smul (x : M) [SMulCommClass R R N] :
     x ∈ sR • N ↔ ∃ (c : R →₀ N), (c.support : Set R) ⊆ sR ∧ x = c.sum fun r m ↦ r • m := by
   fconstructor
   · intros h

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -589,8 +589,7 @@ instance {n : ℕ} {i : Fin (n + 1)} : Epi (σ i) := by
     -- This was not needed before leanprover/lean4#2644
     dsimp
     rw [Fin.predAbove_of_le_castSucc i b (by simpa only [Fin.coe_eq_castSucc] using h)]
-    simp only [len_mk, Fin.coe_eq_castSucc]
-    rfl
+    simp only [len_mk, Fin.coe_eq_castSucc, Fin.castPred_castSucc]
   · use b.succ
     -- This was not needed before leanprover/lean4#2644
     dsimp
@@ -672,9 +671,8 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
     rw [Fin.predAbove_of_le_castSucc i x h']
     dsimp [δ]
     erw [Fin.succAbove_of_castSucc_lt _ _ _]
-    swap
+    · rw [Fin.castSucc_castPred]
     · exact (Fin.castSucc_lt_succ_iff.mpr h')
-    rfl
   · simp only [not_le] at h'
     let y := x.pred <| by rintro (rfl : x = 0); simp at h'
     have hy : x = y.succ := (Fin.succ_pred x _).symm
@@ -741,18 +739,17 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
       -- This was not needed before leanprover/lean4#2644
       dsimp
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-      erw [Fin.predAbove_of_le_castSucc _ _ (by exact h')]
+      erw [Fin.predAbove_of_le_castSucc _ _ (by rwa [Fin.castSucc_castPred])]
       dsimp [δ]
       erw [Fin.succAbove_of_castSucc_lt i]
-      swap
+      · rw [Fin.castSucc_castPred]
       · rw [(hi x).le_iff_lt] at h'
         exact h'
-      rfl
     · simp only [not_le] at h'
       -- The next three tactics used to be a simp only call before leanprover/lean4#2644
       rw [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk, OrderHom.coe_mk]
       erw [OrderHom.coe_mk]
-      erw [Fin.predAbove_of_castSucc_lt _ _ (by exact h')]
+      erw [Fin.predAbove_of_castSucc_lt _ _ (by rwa [Fin.castSucc_castPred])]
       dsimp [δ]
       rw [Fin.succAbove_of_le_castSucc i _]
       -- This was not needed before leanprover/lean4#2644
@@ -765,9 +762,8 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
     ext x : 3
     dsimp [δ, σ]
     simp_rw [Fin.succAbove_last, Fin.predAbove_last_apply]
-    split_ifs with h
-    · exact ((hi x) h).elim
-    · rfl
+    erw [dif_neg (hi x)]
+    rw [Fin.castSucc_castPred]
 #align simplex_category.eq_comp_δ_of_not_surjective' SimplexCategory.eq_comp_δ_of_not_surjective'
 
 theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

@@ -378,8 +378,8 @@ theorem derivSeries_apply_diag (n : ℕ) (x : E) :
     coe_sum', Finset.sum_apply, continuousMultilinearCurryFin1_apply, Matrix.zero_empty]
   convert Finset.sum_const _
   · rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
-  · erw [← card, card_subtype, ← Finset.powersetCard_eq_filter, Finset.card_powersetCard, ← card,
-      card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
+  · rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
+      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
 
 end FormalMultilinearSeries
 
@@ -415,7 +415,7 @@ theorem factorial_smul (n : ℕ) :
     n ! • p n (fun _ ↦ y) = iteratedFDeriv 𝕜 n f x (fun _ ↦ y) := by
   cases n
   · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-  · erw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag, ← smul_apply,
+  · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag, ← smul_apply,
       factorial_smul'.{_,u,v} _ h.fderiv, iteratedFDeriv_succ_apply_right]
     rfl
 

Mathlib/Analysis/Complex/TaylorSeries.lean

@@ -78,11 +78,9 @@ variable ⦃z : ℂ⦄ (hz : z ∈ EMetric.ball c r)
 is given by evaluating its Taylor series at `c` on this open ball. -/
 lemma hasSum_taylorSeries_on_emetric_ball :
     HasSum (fun n : ℕ ↦ (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z) := by
-  obtain ⟨r', hr', hzr'⟩ : ∃ r' < r, z ∈ EMetric.ball c r'
-  · obtain ⟨r', h₁, h₂⟩ := exists_between (EMetric.mem_ball'.mp hz)
-    exact ⟨r', h₂, EMetric.mem_ball'.mpr h₁⟩
+  obtain ⟨r', hzr', hr'⟩ := exists_between (EMetric.mem_ball'.mp hz)
   lift r' to NNReal using ne_top_of_lt hr'
-  rw [Metric.emetric_ball_nnreal] at hzr'
+  rw [← EMetric.mem_ball', Metric.emetric_ball_nnreal] at hzr'
   refine hasSum_taylorSeries_on_ball ?_ hzr'
   rw [← Metric.emetric_ball_nnreal]
   exact hf.mono <| EMetric.ball_subset_ball hr'.le

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -62,8 +62,8 @@ lemma hasFDerivAt_fourier_transform_integrand_right (v : V) (w : W) :
 /-- Norm of the `w`-derivative of the Fourier transform integrand. -/
 lemma norm_fderiv_fourier_transform_integrand_right
     (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W) :
-    ‖fourierChar [-L v w] • mul_L L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ :=
-  by rw [norm_smul, norm_eq_abs (fourierChar _ : ℂ), abs_coe_circle, one_mul, mul_L, norm_smul,
+    ‖fourierChar [-L v w] • mul_L L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := by
+  rw [norm_smul, norm_eq_abs (fourierChar _ : ℂ), abs_coe_circle, one_mul, mul_L, norm_smul,
     norm_neg, norm_mul, norm_mul, norm_eq_abs I, abs_I, mul_one, norm_eq_abs ((_ : ℝ) : ℂ),
     Complex.abs_of_nonneg pi_pos.le, norm_eq_abs (2 : ℂ), Complex.abs_two,
     ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
@@ -95,7 +95,7 @@ theorem hasFDerivAt_fourier [CompleteSpace E] [MeasurableSpace V] [BorelSpace V]
     eventually_of_forall (fun w' ↦ (h0 w').aestronglyMeasurable)
   have h2 : Integrable (F w) μ := h0 w
   have h3 : AEStronglyMeasurable (F' w) μ
-  · change AEStronglyMeasurable (fun v ↦ fourierChar [-L v w] • mul_L L f v) μ
+  · simp only [F']
     refine AEStronglyMeasurable.smul ?_ ?_
     · refine (continuous_subtype_val.comp (continuous_fourierChar.comp ?_)).aestronglyMeasurable
       exact continuous_ofAdd.comp (L.continuous₂.comp (Continuous.Prod.mk_left w)).neg

Mathlib/Analysis/Normed/Group/Completeness.lean

@@ -15,13 +15,14 @@ series.
 
 ## Main results
 
-* `NormedAddCommGroup.completeSpace_of_summable_implies_tendsto`: A normed additive group is
+* `NormedAddCommGroup.completeSpace_of_summable_imp_tendsto`: A normed additive group is
 complete if any absolutely convergent series converges in the space.
 
 ## References
 
-* [bergh_lofstrom_1976] `completeSpace_of_summable_implies_tendsto` and
-  `summable_implies_tendsto_of_complete` correspond to the two directions of Lemma 2.2.1.
+* [bergh_lofstrom_1976] `NormedAddCommGroup.completeSpace_of_summable_imp_tendsto` and
+  `NormedAddCommGroup.summable_imp_tendsto_of_complete` correspond to the two directions of
+  Lemma 2.2.1.
 
 ## Tags
 
@@ -67,8 +68,8 @@ lemma NormedAddCommGroup.completeSpace_of_summable_imp_tendsto
   refine ⟨a + u (f 0), ?_⟩
   refine tendsto_nhds_of_cauchySeq_of_subseq hu hf₁.tendsto_atTop ?_
   rw [hv_sum] at ha
-  have h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0))) := by
-    refine Tendsto.add_const _ ha
+  have h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0))) :=
+    Tendsto.add_const _ ha
   simpa only [sub_add_cancel] using h₁
 
 /-- In a complete normed additive group, every absolutely convergent series converges in the

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -799,7 +799,7 @@ lemma log_le_rpow_div {x ε : ℝ} (hx : 0 ≤ x) (hε : 0 < ε) : log x ≤ x ^
   exact (log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans
     (sub_one_lt _).le
 
-/-- The (real) logarithm of a natural number `n`is bounded by a multiple of every power of `n`
+/-- The (real) logarithm of a natural number `n` is bounded by a multiple of every power of `n`
 with positive exponent. -/
 lemma log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : log n ≤ n ^ ε / ε :=
   log_le_rpow_div n.cast_nonneg hε

Mathlib/Computability/TuringMachine.lean

@@ -1015,10 +1015,10 @@ set_option linter.uppercaseLean3 false
 
 section
 
--- type of "labels" or TM states
+-- type of tape symbols
 variable (Γ : Type*) [Inhabited Γ]
 
--- type of tape symbols
+-- type of "labels" or TM states
 variable (Λ : Type*) [Inhabited Λ]
 
 /-- A Turing machine "statement" is just a command to either move

Mathlib/Data/Fin/Basic.lean

@@ -961,11 +961,11 @@ def castSuccEmb : Fin n ↪o Fin (n + 1) :=
 @[simp]
 theorem castSucc_le_castSucc_iff : castSucc a ≤ castSucc b ↔ a ≤ b := Iff.rfl
 @[simp]
-theorem succ_le_castSucc_iff : succ a ≤ castSucc b ↔ a < b :=
-  by rw [le_castSucc_iff, succ_lt_succ_iff]
+theorem succ_le_castSucc_iff : succ a ≤ castSucc b ↔ a < b := by
+  rw [le_castSucc_iff, succ_lt_succ_iff]
 @[simp]
-theorem castSucc_lt_succ_iff : castSucc a < succ b ↔ a ≤ b :=
-  by rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]
+theorem castSucc_lt_succ_iff : castSucc a < succ b ↔ a ≤ b := by
+  rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]
 
 theorem le_of_castSucc_lt_of_succ_lt {a b : Fin (n + 1)} {i : Fin n}
     (hl : castSucc i < a) (hu : b < succ i) : b < a := (castSucc_lt_iff_succ_le.mp hl).trans_lt' hu
@@ -1168,10 +1168,9 @@ theorem monotone_pred_comp [Preorder α] {f : α → Fin (n + 1)} (hf : ∀ a, f
 
 #align fin.nat_add_sub_nat_cast Fin.natAdd_subNat_castₓ
 
-theorem pred_one' [NeZero n] (h := (zero_ne_one' (n := n)).symm):
-    Fin.pred (1 : Fin (n + 1)) h = 0 :=
-    by simp_rw [Fin.ext_iff, coe_pred, val_one', val_zero',
-      tsub_eq_zero_iff_le, Nat.mod_le]
+theorem pred_one' [NeZero n] (h := (zero_ne_one' (n := n)).symm) :
+    Fin.pred (1 : Fin (n + 1)) h = 0 := by
+  simp_rw [Fin.ext_iff, coe_pred, val_one', val_zero', tsub_eq_zero_iff_le, Nat.mod_le]
 
 theorem pred_last (h := last_pos'.ne') :
     pred (last (n + 1)) h = last n := by simp_rw [← succ_last, pred_succ]

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -868,7 +868,8 @@ theorem insertNth_zero_right [∀ j, Zero (α j)] (i : Fin (n + 1)) (x : α i) :
 
 lemma insertNth_rev {α : Type*} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)) :
     insertNth (α := fun _ ↦ α) i a f (rev j) = insertNth (α := fun _ ↦ α) i.rev a (f ∘ rev) j := by
-  induction j using Fin.succAboveCases; exact rev i
+  induction j using Fin.succAboveCases
+  · exact rev i
   · simp
   · simp [rev_succAbove]
 

Mathlib/Data/Finset/Pointwise.lean

@@ -2215,7 +2215,7 @@ variable [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {s : Finset 
 
 /-!
 Note that we have neither `SMulWithZero α (Finset β)` nor `SMulWithZero (Finset α) (Finset β)`
-because `0 * ∅ ≠ 0`.
+because `0 • ∅ ≠ 0`.
 -/
 
 lemma zero_smul_subset (t : Finset β) : (0 : Finset α) • t ⊆ 0 := by simp [subset_iff, mem_smul]

Mathlib/Data/Nat/Cast/Basic.lean

@@ -63,13 +63,15 @@ def castRingHom : ℕ →+* α :=
 #align nat.coe_cast_ring_hom Nat.coe_castRingHom
 
 lemma _root_.nsmul_eq_mul' (a : α) (n : ℕ) : n • a = a * n := by
-  induction' n with n ih <;> [rw [zero_nsmul, Nat.cast_zero, mul_zero];
-    rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]]
+  induction n with
+  | zero => rw [zero_nsmul, Nat.cast_zero, mul_zero]
+  | succ n ih => rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]
 #align nsmul_eq_mul' nsmul_eq_mul'
 
 @[simp] lemma _root_.nsmul_eq_mul (n : ℕ) (a : α) : n • a = n * a := by
-  induction' n with n ih <;> [rw [zero_nsmul, Nat.cast_zero, zero_mul];
-    rw [succ_nsmul', ih, Nat.cast_succ, add_mul, one_mul]]
+  induction n with
+  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
+  | succ n ih => rw [succ_nsmul', ih, Nat.cast_succ, add_mul, one_mul]
 #align nsmul_eq_mul nsmul_eq_mul
 
 end NonAssocSemiring

Mathlib/Data/Polynomial/Derivative.lean

@@ -484,11 +484,11 @@ theorem pow_sub_one_dvd_derivative_of_pow_dvd {p q : R[X]} {n : ℕ}
 
 theorem pow_sub_dvd_iterate_derivative_of_pow_dvd {p q : R[X]} {n : ℕ} (m : ℕ)
     (dvd : q ^ n ∣ p) : q ^ (n - m) ∣ derivative^[m] p := by
-  revert p
-  induction' m with m ih <;> intro p h
-  · exact h
-  · rw [Nat.sub_succ, Function.iterate_succ']
-    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih h)
+  induction m generalizing p with
+  | zero => simpa
+  | succ m ih =>
+    rw [Nat.sub_succ, Function.iterate_succ']
+    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)
 
 theorem pow_sub_dvd_iterate_derivative_pow (p : R[X]) (n m : ℕ) :
     p ^ (n - m) ∣ derivative^[m] (p ^ n) := pow_sub_dvd_iterate_derivative_of_pow_dvd m dvd_rfl

Mathlib/FieldTheory/SeparableDegree.lean

@@ -334,8 +334,7 @@ theorem natSepDegree_eq_of_splits (h : f.Splits (algebraMap F E)) :
     f.natSepDegree = (f.aroots E).toFinset.card := by
   rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
     roots_map _ ((splits_id_iff_splits _).mpr <| SplittingField.splits f),
-    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _)]
-  rfl
+    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
 
 variable (E) in
 /-- The separable degree of a polynomial is equal to
@@ -522,8 +521,9 @@ theorem finSepDegree_adjoin_simple_eq_natSepDegree {α : E} (halg : IsAlgebraic
     finSepDegree F F⟮α⟯ = (minpoly F α).natSepDegree := by
   have : finSepDegree F F⟮α⟯ = _ := Nat.card_congr
     (algHomAdjoinIntegralEquiv F (K := AlgebraicClosure F⟮α⟯) halg.isIntegral)
-  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯)]
-  exact Eq.trans (by simp only [Multiset.mem_toFinset]) (Fintype.card_coe _)
+  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
+    ← Fintype.card_coe]
+  simp_rw [Multiset.mem_toFinset]
 
 -- The separable degree of `F⟮α⟯ / F` divides the degree of `F⟮α⟯ / F`.
 -- Marked as `private` because it is a special case of `finSepDegree_dvd_finrank`.

Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

@@ -31,7 +31,7 @@ groups here are not necessarily finite dimensional.
   is smooth
 * `ContMDiff.inv₀` and variants: if `SmoothInv₀ N`, point-wise inversion of smooth maps `f : M → N`
   is smooth at all points at which `f` doesn't vanish.
-  ``ContMDiff.div₀` and variants: if also `SmoothMul N` (i.e., `N` is a Lie group except possibly
+* `ContMDiff.div₀` and variants: if also `SmoothMul N` (i.e., `N` is a Lie group except possibly
   for smoothness of inversion at `0`), similar results hold for point-wise division.
 * `normedSpaceLieAddGroup` : a normed vector space over a nontrivially normed field
   is an additive Lie group.

Mathlib/Geometry/Manifold/IntegralCurve.lean

@@ -438,7 +438,7 @@ theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff (ht₀ : t₀ ∈ Ioo a b)
     (h : γ t₀ = γ' t₀) : EqOn γ γ' (Ioo a b) := by
   set s := {t | γ t = γ' t} ∩ Ioo a b with hs
   -- since `Ioo a b` is connected, we get `s = Ioo a b` by showing that `s` is clopen in `Ioo a b`
-  -- in the subtype toplogy (`s` is also non-empty by assumption)
+  -- in the subtype topology (`s` is also non-empty by assumption)
   -- here we use a slightly weaker alternative theorem
   suffices hsub : Ioo a b ⊆ s from fun t ht ↦ mem_setOf.mp ((subset_def ▸ hsub) t ht).1
   apply isPreconnected_Ioo.subset_of_closure_inter_subset (s := Ioo a b) (u := s) _

Mathlib/LinearAlgebra/Basis.lean

@@ -1528,9 +1528,8 @@ lemma basis_finite_of_finite_spans (w : Set M) (hw : w.Finite) (s : span R w = 
     rw [← b.total_repr x, Finsupp.span_image_eq_map_total, Submodule.mem_map]
     use b.repr x
     simp only [and_true_iff, eq_self_iff_true, Finsupp.mem_supported]
-    change (b.repr x).support ≤ S
-    convert Finset.le_sup (α := Finset ι) (by simp : (⟨x, m⟩ : w) ∈ Finset.univ)
-    rfl
+    rw [Finset.coe_subset, ← Finset.le_iff_subset]
+    exact Finset.le_sup (f := fun x : w ↦ (b.repr ↑x).support) (Finset.mem_univ (⟨x, m⟩ : w))
   -- Thus this finite subset of the basis elements spans the entire module.
   have k : span R bS = ⊤ := eq_top_iff.2 (le_trans s.ge (span_le.2 h))
   -- Now there is some `x : ι` not in `S`, since `ι` is infinite.
@@ -1563,15 +1562,15 @@ theorem union_support_maximal_linearIndependent_eq_range_basis {ι : Type w} (b
   have r : range v ⊆ range v' := by
     rintro - ⟨k, rfl⟩
     use some k
-    rfl
+    simp only [Option.elim_some]
   have r' : b b' ∉ range v := by
     rintro ⟨k, p⟩
     simpa [w] using congr_arg (fun m => (b.repr m) b') p
   have r'' : range v ≠ range v' := by
     intro e
     have p : b b' ∈ range v' := by
       use none
-      rfl
+      simp only [Option.elim_none]
     rw [← e] at p
     exact r' p
   -- The key step in the proof is checking that this strictly larger family is linearly independent.

Mathlib/MeasureTheory/Covering/VitaliFamily.lean

@@ -232,7 +232,7 @@ theorem filterAt_basis_closedBall (x : α) :
 
 theorem mem_filterAt_iff {x : α} {s : Set (Set α)} :
     s ∈ v.filterAt x ↔ ∃ ε > (0 : ℝ), ∀ a ∈ v.setsAt x, a ⊆ closedBall x ε → a ∈ s := by
-  simp only [(v.filterAt_basis_closedBall x).mem_iff, ← and_imp]; rfl
+  simp only [(v.filterAt_basis_closedBall x).mem_iff, ← and_imp, subset_def, mem_setOf]
 #align vitali_family.mem_filter_at_iff VitaliFamily.mem_filterAt_iff
 
 instance filterAt_neBot (x : α) : (v.filterAt x).NeBot :=
@@ -266,7 +266,7 @@ theorem eventually_filterAt_measurableSet (x : α) : ∀ᶠ a in v.filterAt x, M
 
 theorem frequently_filterAt_iff {x : α} {P : Set α → Prop} :
     (∃ᶠ a in v.filterAt x, P a) ↔ ∀ ε > (0 : ℝ), ∃ a ∈ v.setsAt x, a ⊆ closedBall x ε ∧ P a := by
-  simp only [(v.filterAt_basis_closedBall x).frequently_iff, ← and_assoc]; rfl
+  simp only [(v.filterAt_basis_closedBall x).frequently_iff, ← and_assoc, subset_def, mem_setOf]
 #align vitali_family.frequently_filter_at_iff VitaliFamily.frequently_filterAt_iff
 
 theorem eventually_filterAt_subset_of_nhds {x : α} {o : Set α} (hx : o ∈ 𝓝 x) :

Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

@@ -260,10 +260,10 @@ the source has a zero and another element. -/
 @[coe, simps]
 def toMonoidWithZeroHom {R : Type*} [CommMonoidWithZero R] [Nontrivial R] (χ : MulChar R R') :
     R →*₀ R' where
-      toFun := χ.toFun
-      map_zero' := χ.map_zero
-      map_one' := χ.map_one'
-      map_mul' := χ.map_mul'
+  toFun := χ.toFun
+  map_zero' := χ.map_zero
+  map_one' := χ.map_one'
+  map_mul' := χ.map_mul'
 
 /-- If the domain is a ring `R`, then `χ (ringChar R) = 0`. -/
 theorem map_ringChar {R : Type u} [CommRing R] [Nontrivial R] (χ : MulChar R R') :