chore: tidy various files (#22894)

Ruben-VandeVelde · Ruben-VandeVelde · commit 3afb02999e85 · 2025-03-14T12:06:17.000Z
diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean
@@ -398,7 +398,7 @@ variable {ι : Type*} {α : ι → Type*} {β : ι → Type*} [∀ i, AddCommMon
 variable [∀ i, AddCommMonoid (β i)] (f : ∀ (i : ι), α i →+ β i)
 
 /-- create a homomorphism from `⨁ i, α i` to `⨁ i, β i` by giving the component-wise map `f`. -/
-def map : (⨁ i, α i) →+ ⨁ i, β i :=  DFinsupp.mapRange.addMonoidHom f
+def map : (⨁ i, α i) →+ ⨁ i, β i := DFinsupp.mapRange.addMonoidHom f
 
 @[simp] lemma map_of [DecidableEq ι] (i : ι) (x : α i) : map f (of α i x) = of β i (f i x) :=
   DFinsupp.mapRange_single (hf := fun _ => map_zero _)
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -908,7 +908,7 @@ lemma ContinuousWithinAt.enorm {s : Set X} {a : X} (h : ContinuousWithinAt f s a
 
 @[fun_prop]
 lemma ContinuousOn.enorm (h : ContinuousOn f s) : ContinuousOn (‖f ·‖ₑ) s :=
-  (ContinuousENorm.continuous_enorm.continuousOn).comp (t := Set.univ) h fun _ _ ↦ trivial
+  (ContinuousENorm.continuous_enorm.continuousOn).comp (t := Set.univ) h <| Set.mapsTo_univ _ _
 
 end ContinuousENorm
 
@@ -920,16 +920,16 @@ variable {E : Type*} [TopologicalSpace E] [ENormedMonoid E]
 lemma enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := ENormedMonoid.enorm_mul_le a b
 
 @[to_additive (attr := simp) enorm_eq_zero]
-lemma enorm_eq_zero' {a : E} :
-  ‖a‖ₑ = 0 ↔ a = 1 := by simp [enorm, ENormedMonoid.enorm_eq_zero]
+lemma enorm_eq_zero' {a : E} : ‖a‖ₑ = 0 ↔ a = 1 := by
+  simp [enorm, ENormedMonoid.enorm_eq_zero]
 
 @[to_additive enorm_ne_zero]
-lemma enorm_ne_zero' {a : E} :
-    ‖a‖ₑ ≠ 0 ↔ a ≠ 1 := enorm_eq_zero'.ne
+lemma enorm_ne_zero' {a : E} : ‖a‖ₑ ≠ 0 ↔ a ≠ 1 :=
+  enorm_eq_zero'.ne
 
 @[to_additive (attr := simp) enorm_pos]
-lemma enorm_pos' {a : E} :
-    0 < ‖a‖ₑ ↔ a ≠ 1 := pos_iff_ne_zero.trans enorm_ne_zero'
+lemma enorm_pos' {a : E} : 0 < ‖a‖ₑ ↔ a ≠ 1 :=
+  pos_iff_ne_zero.trans enorm_ne_zero'
 
 end ENormedMonoid
 
diff --git a/Mathlib/Analysis/Normed/Group/Continuity.lean b/Mathlib/Analysis/Normed/Group/Continuity.lean
@@ -98,7 +98,7 @@ instance SeminormedGroup.toContinuousENorm [SeminormedGroup E] : ContinuousENorm
 @[to_additive]
 instance NormedGroup.toENormedMonoid {F : Type*} [NormedGroup F] : ENormedMonoid F where
   enorm_eq_zero := by simp [enorm_eq_nnnorm]
-  enorm_mul_le :=  by simp [enorm_eq_nnnorm, ← coe_add, nnnorm_mul_le']
+  enorm_mul_le := by simp [enorm_eq_nnnorm, ← coe_add, nnnorm_mul_le']
 
 @[to_additive]
 instance NormedCommGroup.toENormedCommMonoid [NormedCommGroup E] : ENormedCommMonoid E where
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals.lean b/Mathlib/Analysis/SpecialFunctions/Integrals.lean
@@ -382,17 +382,15 @@ theorem integral_rpow {r : ℝ} (h : -1 < r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a,
     (∫ x in a..b, (x : ℂ) ^ (r : ℂ)) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) :=
     integral_cpow h'
   apply_fun Complex.re at this; convert this
-  · simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul]
-    have : Complex.re = RCLike.re := rfl
-    rw [this, ← integral_re]
-    · rfl
+  · simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul, rpow_def,
+      ← RCLike.re_eq_complex_re, smul_eq_mul]
+    rw [integral_re]
     refine intervalIntegrable_iff.mp ?_
     rcases h' with h' | h'
     · exact intervalIntegrable_cpow' h'
     · exact intervalIntegrable_cpow (Or.inr h'.2)
   · rw [(by push_cast; rfl : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))]
-    simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re]
-    rfl
+    simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re, rpow_def]
 
 theorem integral_zpow {n : ℤ} (h : 0 ≤ n ∨ n ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
     ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) := by
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
@@ -112,8 +112,8 @@ lemma preservesBinaryProducts_of_isIso_prodComparison
     PreservesLimitsOfShape (Discrete WalkingPair) G where
   preservesLimit := by
     intro K
-    have : PreservesLimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G := by
-        apply PreservesLimitPair.of_iso_prod_comparison
+    have : PreservesLimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
+      PreservesLimitPair.of_iso_prod_comparison ..
     apply preservesLimit_of_iso_diagram G (diagramIsoPair K).symm
 
 end
@@ -193,8 +193,8 @@ lemma preservesBinaryCoproducts_of_isIso_coprodComparison
     PreservesColimitsOfShape (Discrete WalkingPair) G where
   preservesColimit := by
     intro K
-    have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G := by
-        apply PreservesColimitPair.of_iso_coprod_comparison
+    have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
+      PreservesColimitPair.of_iso_coprod_comparison ..
     apply preservesColimit_of_iso_diagram G (diagramIsoPair K).symm
 
 end
diff --git a/Mathlib/CategoryTheory/Monoidal/Yoneda.lean b/Mathlib/CategoryTheory/Monoidal/Yoneda.lean
@@ -210,9 +210,10 @@ lemma IsCommMon.ofRepresentableBy (F : Cᵒᵖ ⥤ CommMonCat)
     IsCommMon X := by
   letI : Mon_Class X := Mon_Class.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
   have : μ = α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X)) := rfl
-  exact ⟨by simp_rw [this, ←α.homEquiv.apply_eq_iff_eq, α.homEquiv_comp, Functor.comp_map,
+  constructor
+  simp_rw [this, ← α.homEquiv.apply_eq_iff_eq, α.homEquiv_comp, Functor.comp_map,
     ConcreteCategory.forget_map_eq_coe, Equiv.apply_symm_apply, map_mul,
-    ←ConcreteCategory.forget_map_eq_coe, ←Functor.comp_map, ← α.homEquiv_comp, op_tensorObj,
-    Functor.comp_obj, braiding_hom_fst, braiding_hom_snd, _root_.mul_comm]⟩
+    ← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp, op_tensorObj,
+    Functor.comp_obj, braiding_hom_fst, braiding_hom_snd, _root_.mul_comm]
 
 end CommMon_
diff --git a/Mathlib/CategoryTheory/WithTerminal.lean b/Mathlib/CategoryTheory/WithTerminal.lean
@@ -280,7 +280,7 @@ instance : Limits.HasTerminal (WithTerminal C) := Limits.hasTerminal_of_unique s
 /-- The isomorphism between star and an abstract terminal object of `WithTerminal C` -/
 @[simps!]
 noncomputable def starIsoTerminal : star ≅ ⊤_ (WithTerminal C) :=
-    starTerminal.uniqueUpToIso (Limits.terminalIsTerminal)
+  starTerminal.uniqueUpToIso (Limits.terminalIsTerminal)
 
 /-- Lift a functor `F : C ⥤ D` to `WithTerminal C ⥤ D`. -/
 @[simps]
@@ -663,7 +663,7 @@ instance : Limits.HasInitial (WithInitial C) := Limits.hasInitial_of_unique star
 /-- The isomorphism between star and an abstract initial object of `WithInitial C` -/
 @[simps!]
 noncomputable def starIsoInitial : star ≅ ⊥_ (WithInitial C) :=
-    starInitial.uniqueUpToIso (Limits.initialIsInitial)
+  starInitial.uniqueUpToIso (Limits.initialIsInitial)
 
 /-- Lift a functor `F : C ⥤ D` to `WithInitial C ⥤ D`. -/
 @[simps]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean b/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean
@@ -144,8 +144,7 @@ theorem isBipartiteWith_neighborFinset (h : G.IsBipartiteWith s t) (hv : v ∈ s
 "above" `v` according to the adjacency relation of `G`. -/
 theorem isBipartiteWith_bipartiteAbove (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
     G.neighborFinset v = bipartiteAbove G.Adj t v := by
-  rw [isBipartiteWith_neighborFinset h hv]
-  rfl
+  rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]
 
 /-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is a subset of `s`. -/
 theorem isBipartiteWith_neighborFinset_subset (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
@@ -177,8 +176,7 @@ theorem isBipartiteWith_neighborFinset' (h : G.IsBipartiteWith s t) (hw : w ∈
 "below" `w` according to the adjacency relation of `G`. -/
 theorem isBipartiteWith_bipartiteBelow (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
     G.neighborFinset w = bipartiteBelow G.Adj s w := by
-  rw [isBipartiteWith_neighborFinset' h hw]
-  rfl
+  rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]
 
 /-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is a subset of `s`. -/
 theorem isBipartiteWith_neighborFinset_subset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean
@@ -203,8 +203,9 @@ theorem chain'_iff_forall_rel_of_append_cons_cons {l : List α} :
     match tail with
     | nil => exact fun _ ↦ chain'_singleton head
     | cons head' tail =>
-      refine fun h ↦ chain'_cons.mpr ⟨h (nil_append _).symm, ih @(fun a b l₁ l₂ eq => ?_)⟩
-      simpa [eq] using @h (l₁ := head :: l₁) (l₂ := l₂)
+      refine fun h ↦ chain'_cons.mpr ⟨h (nil_append _).symm, ih fun ⦃a b l₁ l₂⦄ eq => ?_⟩
+      apply h
+      rw [eq, cons_append]
 
 theorem chain'_map (f : β → α) {l : List β} :
     Chain' R (map f l) ↔ Chain' (fun a b : β => R (f a) (f b)) l := by
diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
@@ -1007,7 +1007,7 @@ theorem liftRel_congr {R : α → β → Prop} {ca ca' : Computation α} {cb cb'
 theorem liftRel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
     {s2 : Computation β} {f1 : α → γ} {f2 : β → δ} (h1 : LiftRel R s1 s2)
     (h2 : ∀ {a b}, R a b → S (f1 a) (f2 b)) : LiftRel S (map f1 s1) (map f2 s2) := by
-  rw [← bind_pure, ← bind_pure]; apply liftRel_bind _ _ h1; simp; exact @h2
+  rw [← bind_pure, ← bind_pure]; apply liftRel_bind _ _ h1; simpa
 
 theorem map_congr {s1 s2 : Computation α} {f : α → β}
     (h1 : s1 ~ s2) : map f s1 ~ map f s2 := by
diff --git a/Mathlib/Data/Set/FunctorToTypes.lean b/Mathlib/Data/Set/FunctorToTypes.lean
@@ -10,7 +10,7 @@ import Mathlib.Data.Set.Basic
 /-!
 # The functor from `Set X` to types
 
-Given `X : Type u`, we define the functor `Set.toTypes : Set X ⥤ Type u`
+Given `X : Type u`, we define the functor `Set.functorToTypes : Set X ⥤ Type u`
 which sends `A : Set X` to its underlying type.
 
 -/
diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean
@@ -339,7 +339,7 @@ lemma det_mulRight (a : R) : (mulRight R a).det = a := by simp
 theorem det_prodMap [Module.Free R M] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M']
     (f : Module.End R M) (f' : Module.End R M') :
     (prodMap f f').det = f.det * f'.det := by
-  let b  := Module.Free.chooseBasis R M
+  let b := Module.Free.chooseBasis R M
   let b' := Module.Free.chooseBasis R M'
   rw [← det_toMatrix (b.prod b'), ← det_toMatrix b, ← det_toMatrix b', toMatrix_prodMap,
     det_fromBlocks_zero₂₁, det_toMatrix]
diff --git a/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean b/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
@@ -356,7 +356,7 @@ theorem Fintype.bilinearCombination_apply :
 
 theorem Fintype.bilinearCombination_apply_single [DecidableEq α] (i : α) (r : R) :
     Fintype.bilinearCombination R S v (Pi.single i r) = r • v i := by
-  simp [Fintype.bilinearCombination]-- Fintype.linearCombination_apply_single]
+  simp [Fintype.bilinearCombination]
 
 section SpanRange
 
diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean
@@ -68,8 +68,7 @@ theorem det_eq_sum_column_mul_submatrix_succAbove_succAbove_det {n : ℕ}
     (hv : ∀ j ≠ j₀, ∑ i, M i j = 0) :
     M.det = (-1) ^ (i₀ + j₀ : ℕ) *
       (∑ i, M i j₀) * (M.submatrix (Fin.succAbove i₀) (Fin.succAbove j₀)).det := by
-  rw [show M.det = (1 : R) • Matrix.det _ by rw [one_smul],
-    ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]
+  rw [← one_smul R M.det, ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]
   simp only [updateRow_apply, if_true, one_smul, submatrix_updateRow_succAbove, Finset.sum_apply]
   rw [Fintype.sum_eq_add_sum_subtype_ne _ j₀]
   conv_lhs =>
@@ -85,8 +84,8 @@ theorem det_eq_sum_row_mul_submatrix_succAbove_succAbove_det {n : ℕ}
     (hv : ∀ i ≠ i₀, ∑ j, M i j = 0) :
     M.det = (-1) ^ (i₀ + j₀ : ℕ) *
       (∑ j, M i₀ j) * (M.submatrix (Fin.succAbove i₀) (Fin.succAbove j₀)).det := by
-    rw [← det_transpose, det_eq_sum_column_mul_submatrix_succAbove_succAbove_det _ j₀ i₀
-      (by simpa using hv), ← det_transpose, transpose_submatrix, transpose_transpose, add_comm]
-    simp_rw [transpose_apply]
+  rw [← det_transpose, det_eq_sum_column_mul_submatrix_succAbove_succAbove_det _ j₀ i₀
+    (by simpa using hv), ← det_transpose, transpose_submatrix, transpose_transpose, add_comm]
+  simp_rw [transpose_apply]
 
 end Matrix
diff --git a/Mathlib/MeasureTheory/Function/FactorsThrough.lean b/Mathlib/MeasureTheory/Function/FactorsThrough.lean
@@ -31,8 +31,7 @@ theorem _root_.Measurable.factorsThrough [MeasurableSpace Z] [MeasurableSingleto
     (hg : Measurable[mY.comap f] g) : g.FactorsThrough f := by
   refine fun x₁ x₂ h ↦ eq_of_mem_singleton ?_
   obtain ⟨s, -, hs⟩ := hg (measurableSet_singleton (g x₂))
-  rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs]
-  rfl
+  rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
 
 /-- If a function `g` is strongly measurable with respect to the pullback along some function `f`,
 then to prove `g x = g y` it is enough to prove `f x = f y`.
diff --git a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean
@@ -165,7 +165,7 @@ theorem analyticOnNhd_circleMap (c : ℂ) (R : ℝ) :
   intro z hz
   apply analyticAt_const.add
   apply analyticAt_const.mul
-  rw [(by rfl : (fun θ ↦ exp (θ * I) : ℝ → ℂ) = cexp ∘ (fun θ : ℝ ↦ (θ * I)))]
+  rw [← Function.comp_def]
   apply analyticAt_cexp.restrictScalars.comp ((ofRealCLM.analyticAt z).mul (by fun_prop))
 
 /-- The circleMap is continuously differentiable. -/
@@ -268,8 +268,9 @@ theorem CircleIntegrable.congr_codiscreteWithin {c : ℂ} {R : ℝ} {f₁ f₂ :
   · simp [hR]
   apply (intervalIntegrable_congr_codiscreteWithin _).1 hf₁
   rw [eventuallyEq_iff_exists_mem]
-  use (circleMap c R)⁻¹' {z | f₁ z = f₂ z}, codiscreteWithin.mono
-    (by simp only [Set.subset_univ]) (circleMap_preimage_codiscrete hR hf), (by tauto)
+  exact ⟨(circleMap c R)⁻¹' {z | f₁ z = f₂ z},
+    codiscreteWithin.mono (by simp only [Set.subset_univ]) (circleMap_preimage_codiscrete hR hf),
+    by tauto⟩
 
 /-- Circle integrability is invariant when functions change along discrete sets. -/
 theorem circleIntegrable_congr_codiscreteWithin {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℂ}
diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -22,7 +22,7 @@ to form the Dirichlet ring.
 ## Main Definitions
 
  * `ArithmeticFunction R` consists of functions `f : ℕ → R` such that `f 0 = 0`.
- * An arithmetic function `f` `IsMultiplicative` when `x.coprime y → f (x * y) = f x * f y`.
+ * An arithmetic function `f` `IsMultiplicative` when `x.Coprime y → f (x * y) = f x * f y`.
  * The pointwise operations `pmul` and `ppow` differ from the multiplication
   and power instances on `ArithmeticFunction R`, which use Dirichlet multiplication.
  * `ζ` is the arithmetic function such that `ζ x = 1` for `0 < x`.
@@ -297,16 +297,7 @@ theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b
   rw [← sum_subset h]
   · simp
   intro y ymem ynmem
-  have y1ne : y.fst ≠ 1 := by
-    intro con
-    simp only [mem_divisorsAntidiagonal, one_mul, Ne] at ymem
-    simp only [mem_singleton, Prod.ext_iff] at ynmem
-    -- Porting note: `tauto` worked from here.
-    cases y
-    subst con
-    simp only [true_and, one_mul, x0, not_false_eq_true, and_true] at ynmem ymem
-    tauto
-
+  have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff]
   simp [y1ne]
 
 end Module
@@ -426,11 +417,11 @@ theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
     rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one]
   · rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk]
 
-theorem zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i :=
-  coe_zeta_mul_apply
+theorem zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := by
+  rw [← natCoe_nat ζ, coe_zeta_mul_apply]
 
-theorem mul_zeta_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (f * ζ) x = ∑ i ∈ divisors x, f i :=
-  coe_mul_zeta_apply
+theorem mul_zeta_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (f * ζ) x = ∑ i ∈ divisors x, f i := by
+  rw [← natCoe_nat ζ, coe_mul_zeta_apply]
 
 end Zeta
 
@@ -482,8 +473,7 @@ theorem ppow_zero {f : ArithmeticFunction R} : f.ppow 0 = ζ := by rw [ppow, dif
 
 @[simp]
 theorem ppow_apply {f : ArithmeticFunction R} {k x : ℕ} (kpos : 0 < k) : f.ppow k x = f x ^ k := by
-  rw [ppow, dif_neg (Nat.ne_of_gt kpos)]
-  rfl
+  rw [ppow, dif_neg (Nat.ne_of_gt kpos), coe_mk]
 
 theorem ppow_succ' {f : ArithmeticFunction R} {k : ℕ} : f.ppow (k + 1) = f.pmul (f.ppow k) := by
   ext x
@@ -671,7 +661,7 @@ theorem pmul [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicat
 @[arith_mult]
 theorem pdiv [CommGroupWithZero R] {f g : ArithmeticFunction R} (hf : IsMultiplicative f)
     (hg : IsMultiplicative g) : IsMultiplicative (pdiv f g) :=
-  ⟨ by simp [hf, hg], fun {m n} cop => by
+  ⟨by simp [hf, hg], fun {m n} cop => by
     simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop,
       div_eq_mul_inv, mul_inv]
     apply mul_mul_mul_comm ⟩
@@ -748,7 +738,7 @@ theorem lcm_apply_mul_gcd_apply [CommMonoidWithZero R] {f : ArithmeticFunction R
     intro i; rw [Nat.pow_zero, hf.1]
   iterate 4 rw [hf.multiplicative_factorization f (by assumption),
     Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
-      (s := (x.primeFactors ⊔ y.primeFactors))]
+      (s := (x.primeFactors ∪ y.primeFactors))]
   · rw [← Finset.prod_mul_distrib, ← Finset.prod_mul_distrib]
     apply Finset.prod_congr rfl
     intro p _
@@ -758,19 +748,19 @@ theorem lcm_apply_mul_gcd_apply [CommMonoidWithZero R] {f : ArithmeticFunction R
         inf_of_le_left, mul_comm]
   · apply Finset.subset_union_right
   · apply Finset.subset_union_left
-  · rw [factorization_gcd hx hy, Finsupp.support_inf, Finset.sup_eq_union]
+  · rw [factorization_gcd hx hy, Finsupp.support_inf]
     apply Finset.inter_subset_union
   · simp [factorization_lcm hx hy]
 
 theorem map_gcd [CommGroupWithZero R] {f : ArithmeticFunction R}
     (hf : f.IsMultiplicative) {x y : ℕ} (hf_lcm : f (x.lcm y) ≠ 0) :
     f (x.gcd y) = f x * f y / f (x.lcm y) := by
-  rw [←hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]
+  rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]
 
 theorem map_lcm [CommGroupWithZero R] {f : ArithmeticFunction R}
     (hf : f.IsMultiplicative) {x y : ℕ} (hf_gcd : f (x.gcd y) ≠ 0) :
     f (x.lcm y) = f x * f y / f (x.gcd y) := by
-  rw [←hf.lcm_apply_mul_gcd_apply, mul_div_cancel_right₀ _ hf_gcd]
+  rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_right₀ _ hf_gcd]
 
 theorem eq_zero_of_squarefree_of_dvd_eq_zero [CommMonoidWithZero R] {f : ArithmeticFunction R}
     (hf : IsMultiplicative f) {m n : ℕ} (hn : Squarefree n) (hmn : m ∣ n)
@@ -945,8 +935,7 @@ theorem cardDistinctFactors_eq_cardFactors_iff_squarefree {n : ℕ} (h0 : n ≠
   constructor <;> intro h
   · rw [← n.primeFactorsList.dedup_sublist.eq_of_length h]
     apply List.nodup_dedup
-  · rw [h.dedup]
-    rfl
+  · simp [h.dedup, cardFactors]
 
 @[simp]
 theorem cardDistinctFactors_apply_prime_pow {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) :
@@ -1009,7 +998,7 @@ theorem moebius_sq {n : ℕ} :
   split_ifs with h
   · exact moebius_sq_eq_one_of_squarefree h
   · simp only [pow_eq_zero_iff, moebius_eq_zero_of_not_squarefree h,
-    zero_pow (show 2 ≠ 0 by norm_num)]
+      zero_pow (show 2 ≠ 0 by norm_num)]
 
 theorem abs_moebius {n : ℕ} :
     |μ n| = if Squarefree n then 1 else 0 := by
@@ -1208,7 +1197,7 @@ theorem sum_eq_iff_sum_smul_moebius_eq_on [AddCommGroup R] {f g : ℕ → R}
   · intro h
     let G := fun (n : ℕ) => (∑ i ∈ n.divisors, f i)
     intro n hn hnP
-    suffices ∑ d ∈ n.divisors, μ (n/d) • G d = f n from by
+    suffices ∑ d ∈ n.divisors, μ (n/d) • G d = f n by
       rw [Nat.sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
       intro d hd
       rw [← h d (Nat.pos_of_mem_divisors hd) <| hs d n (Nat.dvd_of_mem_divisors hd) hnP]
@@ -1218,7 +1207,7 @@ theorem sum_eq_iff_sum_smul_moebius_eq_on [AddCommGroup R] {f g : ℕ → R}
   · intro h
     let F := fun (n : ℕ) => ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd
     intro n hn hnP
-    suffices ∑ d ∈ n.divisors, F d = g n from by
+    suffices ∑ d ∈ n.divisors, F d = g n by
       rw [← this, sum_congr rfl]
       intro d hd
       rw [← h d (Nat.pos_of_mem_divisors hd) <| hs d n (Nat.dvd_of_mem_divisors hd) hnP]
diff --git a/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean b/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean
diff --git a/Mathlib/RingTheory/MatrixPolynomialAlgebra.lean b/Mathlib/RingTheory/MatrixPolynomialAlgebra.lean
diff --git a/Mathlib/RingTheory/Polynomial/SmallDegreeVieta.lean b/Mathlib/RingTheory/Polynomial/SmallDegreeVieta.lean
diff --git a/Mathlib/SetTheory/Cardinal/Regular.lean b/Mathlib/SetTheory/Cardinal/Regular.lean
diff --git a/Mathlib/Topology/DiscreteSubset.lean b/Mathlib/Topology/DiscreteSubset.lean
diff --git a/Mathlib/Topology/MetricSpace/Closeds.lean b/Mathlib/Topology/MetricSpace/Closeds.lean
