chore: tidy various files (#9851)

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -974,7 +974,7 @@ def center : NonUnitalSubalgebra R A :=
 theorem coe_center : (center R A : Set A) = Set.center A :=
   rfl
 
-/-- The center of a non-unital algebra is a commutative and associative -/
+/-- The center of a non-unital algebra is commutative and associative -/
 instance center.instNonUnitalCommSemiring : NonUnitalCommSemiring (center R A) :=
   NonUnitalSubsemiring.center.instNonUnitalCommSemiring _
 

Mathlib/Algebra/Group/PNatPowAssoc.lean

@@ -33,7 +33,7 @@ powers are considered.
 ## Todo
 
 * `NatPowAssoc` for `MulOneClass` - more or less the same flow
-* It seems unlikely that anyone will want `NatSMulAssoc` and `PNatSmulAssoc` as additive versions of
+* It seems unlikely that anyone will want `NatSMulAssoc` and `PNatSMulAssoc` as additive versions of
   power-associativity, but we have found that it is not hard to write.
 
 -/
@@ -67,8 +67,8 @@ theorem ppow_mul_comm (m n : ℕ+) (x : M) :
 
 theorem ppow_mul (x : M) (m n : ℕ+) : x ^ (m * n) = (x ^ m) ^ n := by
   refine PNat.recOn n ?_ fun k hk ↦ ?_
-  rw [ppow_one, mul_one]
-  rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
+  · rw [ppow_one, mul_one]
+  · rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
 
 theorem ppow_mul' (x : M) (m n : ℕ+) : x ^ (m * n) = (x ^ n) ^ m := by
   rw [mul_comm]
@@ -78,8 +78,8 @@ end Mul
 
 instance Pi.instPNatPowAssoc {ι : Type*} {α : ι → Type*} [∀ i, Mul <| α i] [∀ i, Pow (α i) ℕ+]
     [∀ i, PNatPowAssoc <| α i] : PNatPowAssoc (∀ i, α i) where
-    ppow_add _ _ _ := by ext; simp [ppow_add]
-    ppow_one _ := by ext; simp
+  ppow_add _ _ _ := by ext; simp [ppow_add]
+  ppow_one _ := by ext; simp
 
 instance Prod.instPNatPowAssoc {N : Type*} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] [Mul N] [Pow N ℕ+]
     [PNatPowAssoc N] : PNatPowAssoc (M × N) where
@@ -89,5 +89,5 @@ instance Prod.instPNatPowAssoc {N : Type*} [Mul M] [Pow M ℕ+] [PNatPowAssoc M]
 theorem ppow_eq_pow [Monoid M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (n : ℕ+) :
     x ^ n = x ^ (n : ℕ) := by
   refine PNat.recOn n ?_ fun k hk ↦ ?_
-  rw [ppow_one, PNat.one_coe, pow_one]
-  rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
+  · rw [ppow_one, PNat.one_coe, pow_one]
+  · rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

Mathlib/Algebra/Order/Module/Defs.lean

@@ -531,9 +531,9 @@ variable [PartialOrder α] [Preorder β]
 lemma PosSMulMono.of_pos (h₀ : ∀ a : α, 0 < a → ∀ b₁ b₂ : β, b₁ ≤ b₂ → a • b₁ ≤ a • b₂) :
     PosSMulMono α β where
   elim a ha b₁ b₂ h := by
-      obtain ha | ha := ha.eq_or_lt
-      · simp [← ha]
-      · exact h₀ _ ha _ _ h
+    obtain ha | ha := ha.eq_or_lt
+    · simp [← ha]
+    · exact h₀ _ ha _ _ h
 
 /-- A constructor for `PosSMulReflectLT` requiring you to prove `a • b₁ < a • b₂ → b₁ < b₂` only
 when `0 < a`-/
@@ -562,7 +562,7 @@ lemma SMulPosMono.of_pos (h₀ : ∀ b : β, 0 < b → ∀ a₁ a₂ : α, a₁
 when `0 < b`-/
 lemma SMulPosReflectLT.of_pos (h₀ : ∀ b : β, 0 < b → ∀ a₁ a₂ : α, a₁ • b < a₂ • b → a₁ < a₂) :
     SMulPosReflectLT α β where
-  elim  b hb a₁ a₂ h := by
+  elim b hb a₁ a₂ h := by
     obtain hb | hb := hb.eq_or_lt
     · simp [← hb] at h
     · exact h₀ _ hb _ _ h

Mathlib/Data/PNat/Factors.lean

@@ -222,12 +222,10 @@ theorem prod_add (u v : PrimeMultiset) : (u + v).prod = u.prod * v.prod := by
   exact Multiset.prod_add _ _
 #align prime_multiset.prod_add PrimeMultiset.prod_add
 
--- Porting note: Need to replace ^ with Pow.pow to get the original mathlib statement
-theorem prod_smul (d : ℕ) (u : PrimeMultiset) : (d • u).prod = Pow.pow u.prod d := by
-  induction' d with n ih
-  · rfl
-  · have : ∀ n' : ℕ, Pow.pow (prod u) n' = Monoid.npow n' (prod u) := fun _ ↦ rfl
-    rw [succ_nsmul, prod_add, ih, this, this, Monoid.npow_succ, mul_comm]
+theorem prod_smul (d : ℕ) (u : PrimeMultiset) : (d • u).prod = u.prod ^ d := by
+  induction d with
+  | zero => simp only [Nat.zero_eq, zero_nsmul, pow_zero, prod_zero]
+  | succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ, mul_comm]
 #align prime_multiset.prod_smul PrimeMultiset.prod_smul
 
 end PrimeMultiset
@@ -303,7 +301,7 @@ theorem factorMultiset_mul (n m : ℕ+) :
 #align pnat.factor_multiset_mul PNat.factorMultiset_mul
 
 theorem factorMultiset_pow (n : ℕ+) (m : ℕ) :
-    factorMultiset (Pow.pow n m) = m • factorMultiset n := by
+    factorMultiset (n ^ m) = m • factorMultiset n := by
   let u := factorMultiset n
   have : n = u.prod := (prod_factorMultiset n).symm
   rw [this, ← PrimeMultiset.prod_smul]
@@ -389,7 +387,7 @@ theorem factorMultiset_lcm (m n : ℕ+) :
 /-- The number of occurrences of p in the factor multiset of m
  is the same as the p-adic valuation of m. -/
 theorem count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ℕ) :
-    Pow.pow (p : ℕ+) k ∣ m ↔ k ≤ m.factorMultiset.count p := by
+    (p : ℕ+) ^ k ∣ m ↔ k ≤ m.factorMultiset.count p := by
   intros
   rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow,
     factorMultiset_ofPrime]

Mathlib/Data/Polynomial/RingDivision.lean

@@ -1072,8 +1072,8 @@ theorem aroots_one [CommRing S] [IsDomain S] [Algebra T S] :
 
 @[simp]
 theorem aroots_neg [CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) :
-    (-p).aroots S = p.aroots S :=
-  by rw [aroots, Polynomial.map_neg, roots_neg]
+    (-p).aroots S = p.aroots S := by
+  rw [aroots, Polynomial.map_neg, roots_neg]
 
 @[simp]
 theorem aroots_C_mul [CommRing S] [IsDomain S] [Algebra T S]

Mathlib/Data/Set/Finite.lean

@@ -1275,8 +1275,8 @@ theorem empty_card : Fintype.card (∅ : Set α) = 0 :=
   rfl
 #align set.empty_card Set.empty_card
 
-theorem empty_card' {h : Fintype.{u} (∅ : Set α)} : @Fintype.card (∅ : Set α) h = 0 :=
-  by simp
+theorem empty_card' {h : Fintype.{u} (∅ : Set α)} : @Fintype.card (∅ : Set α) h = 0 := by
+  simp
 #align set.empty_card' Set.empty_card'
 
 theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) :

Mathlib/Data/Set/Pointwise/Basic.lean

@@ -1301,7 +1301,7 @@ theorem image_mul : m '' (s * t) = m '' s * m '' t :=
 
 @[to_additive]
 lemma mul_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s * t ⊆ range m := by
-  rintro _ ⟨a, ha, b, hb, rfl⟩;
+  rintro _ ⟨a, ha, b, hb, rfl⟩
   obtain ⟨a, rfl⟩ := hs ha
   obtain ⟨b, rfl⟩ := ht hb
   exact ⟨a * b, map_mul _ _ _⟩
@@ -1334,7 +1334,7 @@ theorem image_div : m '' (s / t) = m '' s / m '' t :=
 
 @[to_additive]
 lemma div_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s / t ⊆ range m := by
-  rintro _ ⟨a, ha, b, hb, rfl⟩;
+  rintro _ ⟨a, ha, b, hb, rfl⟩
   obtain ⟨a, rfl⟩ := hs ha
   obtain ⟨b, rfl⟩ := ht hb
   exact ⟨a / b, map_div _ _ _⟩

Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

@@ -86,8 +86,8 @@ lemma eval₂_minpolyDiv_self {T} [CommRing T] [Algebra R T] [IsDomain T] [Decid
 lemma eval_minpolyDiv_of_aeval_eq_zero [IsDomain S] [DecidableEq S]
     {y} (hy : aeval y (minpoly R x) = 0) :
     (minpolyDiv R x).eval y = if x = y then aeval x (derivative <| minpoly R x) else 0 := by
-  rw [eval, eval₂_minpolyDiv_of_eval₂_eq_zero]; rfl
-  exact hy
+  rw [eval, eval₂_minpolyDiv_of_eval₂_eq_zero, RingHom.id_apply, RingHom.id_apply]
+  simpa [aeval_def] using hy
 
 lemma natDegree_minpolyDiv_succ [Nontrivial S] :
     natDegree (minpolyDiv R x) + 1 = natDegree (minpoly R x) := by
@@ -105,7 +105,7 @@ lemma natDegree_minpolyDiv :
 lemma natDegree_minpolyDiv_lt [Nontrivial S] :
     natDegree (minpolyDiv R x) < natDegree (minpoly R x) := by
   rw [← natDegree_minpolyDiv_succ hx]
-  exact Nat.lt.base _
+  exact Nat.lt_succ_self _
 
 lemma coeff_minpolyDiv_mem_adjoin (x : S) (i) :
     coeff (minpolyDiv R x) i ∈ Algebra.adjoin R {x} := by
@@ -123,7 +123,7 @@ lemma coeff_minpolyDiv_mem_adjoin (x : S) (i) :
   · exact zero_mem _
   · refine (Nat.le_add_left _ i).trans_lt ?_
     rw [← add_assoc]
-    exact Nat.lt.base _
+    exact Nat.lt_succ_self _
 
 lemma minpolyDiv_eq_of_isIntegrallyClosed [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
     [Algebra R K] [Algebra K S] [IsScalarTower R K S] [IsFractionRing R K] :
@@ -150,7 +150,8 @@ lemma coeff_minpolyDiv_sub_pow_mem_span {i} (hi : i ≤ natDegree (minpolyDiv R
           (Submodule.mem_span_singleton_self x))
       rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
       apply Submodule.span_mono
-      rintro _ ⟨j, hj : j < i, rfl⟩
+      rintro _ ⟨j, hj, rfl⟩
+      rw [Set.mem_Iio] at hj
       exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ' x j⟩
 
 lemma span_coeff_minpolyDiv :

Mathlib/FieldTheory/Separable.lean

@@ -635,8 +635,10 @@ lemma IsSeparable.of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [Field A₁] [Fie
   letI := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
   haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
     (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
-  let e : B₁ ≃ₐ[A₂] B₂ := { e₂ with commutes' := fun r ↦ by simpa [RingHom.algebraMap_toAlgebra]
-                                                  using DFunLike.congr_fun he.symm (e₁.symm r) }
+  let e : B₁ ≃ₐ[A₂] B₂ :=
+    { e₂ with
+      commutes' := fun r ↦ by
+        simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm r) }
   haveI := isSeparable_tower_top_of_isSeparable A₁ A₂ B₁
   exact IsSeparable.of_algHom _ _ e.symm.toAlgHom
 

Mathlib/Geometry/Manifold/InteriorBoundary.lean

@@ -73,24 +73,21 @@ lemma isBoundaryPoint_iff {x : M} : I.IsBoundaryPoint x ↔ extChartAt I x x ∈
 
 /-- Every point is either an interior or a boundary point. -/
 lemma isInteriorPoint_or_isBoundaryPoint (x : M) : I.IsInteriorPoint x ∨ I.IsBoundaryPoint x := by
-  by_cases h : extChartAt I x x ∈ interior (range I)
-  · exact Or.inl h
-  · right -- Otherwise, we have a boundary point.
-    rw [I.isBoundaryPoint_iff, ← closure_diff_interior, I.closed_range.closure_eq]
-    exact ⟨mem_range_self _, h⟩
+  rw [IsInteriorPoint, or_iff_not_imp_left, I.isBoundaryPoint_iff, ← closure_diff_interior,
+    I.closed_range.closure_eq, mem_diff]
+  exact fun h => ⟨mem_range_self _, h⟩
 
 /-- A manifold decomposes into interior and boundary. -/
 lemma interior_union_boundary_eq_univ : (I.interior M) ∪ (I.boundary M) = (univ : Set M) :=
-  le_antisymm (fun _ _ ↦ trivial) (fun x _ ↦ I.isInteriorPoint_or_isBoundaryPoint x)
+  eq_univ_of_forall fun x => (mem_union _ _ _).mpr (I.isInteriorPoint_or_isBoundaryPoint x)
 
 /-- The interior and boundary of a manifold `M` are disjoint. -/
 lemma disjoint_interior_boundary : Disjoint (I.interior M) (I.boundary M) := by
   by_contra h
   -- Choose some x in the intersection of interior and boundary.
-  choose x hx using not_disjoint_iff.mp h
-  rcases hx with ⟨h1, h2⟩
-  show (extChartAt I x) x ∈ (∅ : Set E)
-  rw [← disjoint_iff_inter_eq_empty.mp (disjoint_interior_frontier (s := range I))]
+  obtain ⟨x, h1, h2⟩ := not_disjoint_iff.mp h
+  rw [← mem_empty_iff_false (extChartAt I x x),
+    ← disjoint_iff_inter_eq_empty.mp (disjoint_interior_frontier (s := range I)), mem_inter_iff]
   exact ⟨h1, h2⟩
 
 /-- The boundary is the complement of the interior. -/
@@ -132,10 +129,9 @@ variable [BoundarylessManifold I M]
 lemma _root_.BoundarylessManifold.isInteriorPoint {x : M} :
     IsInteriorPoint I x := BoundarylessManifold.isInteriorPoint' x
 
-/-- Boundaryless manifolds have full interior. -/
-lemma interior_eq_univ : I.interior M = univ := by
-  ext
-  refine ⟨fun _ ↦ trivial, fun _ ↦ BoundarylessManifold.isInteriorPoint I⟩
+/-- If `I` is boundaryless, `M` has full interior. -/
+lemma interior_eq_univ : I.interior M = univ :=
+  eq_univ_of_forall fun _ => BoundarylessManifold.isInteriorPoint I
 
 /-- Boundaryless manifolds have empty boundary. -/
 lemma Boundaryless.boundary_eq_empty : I.boundary M = ∅ := by

Mathlib/GroupTheory/Subsemigroup/Center.lean

@@ -64,12 +64,12 @@ namespace IsMulCentral
 
 variable {a b c : M} [Mul M]
 
--- c.f. Commute.left_comm
+-- cf. `Commute.left_comm`
 @[to_additive]
 protected theorem left_comm (h : IsMulCentral a) (b c) : a * (b * c) = b * (a * c) := by
   simp only [h.comm, h.right_assoc]
 
--- c.f. Commute.right_comm
+-- cf. `Commute.right_comm`
 @[to_additive]
 protected theorem right_comm (h : IsMulCentral c) (a b) : a * b * c = a * c * b := by
   simp only [h.right_assoc, h.mid_assoc, h.comm]

Mathlib/LinearAlgebra/Basis.lean

@@ -1405,7 +1405,7 @@ lemma Basis.mem_center_iff {A}
           ∧ (b i * z) * b j = b i * (z * b j)
           ∧ (b i * b j) * z = b i * (b j * z) := by
   constructor
-  · intro h;
+  · intro h
     constructor
     · intro i
       apply (h.1 (b i)).symm

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -190,9 +190,9 @@ theorem lt_aleph0_of_finite {ι : Type w}
     [Module.Finite R M] {v : ι → M} (h : LinearIndependent R v) : #ι < ℵ₀ := by
   apply Cardinal.lift_lt.1
   apply lt_of_le_of_lt
-  apply h.cardinal_lift_le_rank
-  rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]
-  apply Cardinal.nat_lt_aleph0
+  · apply h.cardinal_lift_le_rank
+  · rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]
+    apply Cardinal.nat_lt_aleph0
 
 theorem finite [Module.Finite R M] {ι : Type*} {f : ι → M}
     (h : LinearIndependent R f) : Finite ι :=
@@ -364,20 +364,16 @@ variable [StrongRankCondition R] [Module.Finite R M]
 
 /-- A finite rank torsion-free module has positive `finrank` iff it has a nonzero element. -/
 theorem FiniteDimensional.finrank_pos_iff_exists_ne_zero [NoZeroSMulDivisors R M] :
-    0 < finrank R M ↔ ∃ x : M, x ≠ 0 :=
-  Iff.trans
-    (by
-      rw [← finrank_eq_rank]
-      norm_cast)
-    (@rank_pos_iff_exists_ne_zero R M _ _ _ _ _)
+    0 < finrank R M ↔ ∃ x : M, x ≠ 0 := by
+  rw [← @rank_pos_iff_exists_ne_zero R M, ← finrank_eq_rank]
+  norm_cast
 #align finite_dimensional.finrank_pos_iff_exists_ne_zero FiniteDimensional.finrank_pos_iff_exists_ne_zero
 
 /-- An `R`-finite torsion-free module has positive `finrank` iff it is nontrivial. -/
 theorem FiniteDimensional.finrank_pos_iff [NoZeroSMulDivisors R M] :
-    0 < finrank R M ↔ Nontrivial M :=
-  Iff.trans
-    (by rw [← finrank_eq_rank]; norm_cast)
-    (rank_pos_iff_nontrivial (R := R))
+    0 < finrank R M ↔ Nontrivial M := by
+  rw [← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank]
+  norm_cast
 #align finite_dimensional.finrank_pos_iff FiniteDimensional.finrank_pos_iff
 
 /-- A nontrivial finite dimensional space has positive `finrank`. -/
@@ -389,26 +385,23 @@ theorem FiniteDimensional.finrank_pos [NoZeroSMulDivisors R M] [h : Nontrivial M
 /-- See `FiniteDimensional.finrank_zero_iff`
   for the stronger version with `NoZeroSMulDivisors R M`. -/
 theorem FiniteDimensional.finrank_eq_zero_iff [Module.Finite R M] :
-    finrank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0 :=
-  Iff.trans
-    (by rw [← finrank_eq_rank]; norm_cast)
-    (rank_eq_zero_iff (R := R))
+    finrank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0 := by
+  rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank]
+  norm_cast
 
 /-- The `StrongRankCondition` is automatic. See `commRing_strongRankCondition`. -/
 theorem FiniteDimensional.finrank_eq_zero_iff_isTorsion {R} [CommRing R] [StrongRankCondition R]
     [IsDomain R] [Module R M] [Module.Finite R M] :
-    finrank R M = 0 ↔ Module.IsTorsion R M :=
-  Iff.trans
-    (by rw [← finrank_eq_rank]; norm_cast)
-    (rank_eq_zero_iff_isTorsion (R := R))
+    finrank R M = 0 ↔ Module.IsTorsion R M := by
+  rw [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank]
+  norm_cast
 
 /-- A finite dimensional space has zero `finrank` iff it is a subsingleton.
 This is the `finrank` version of `rank_zero_iff`. -/
 theorem FiniteDimensional.finrank_zero_iff [NoZeroSMulDivisors R M] :
-    finrank R M = 0 ↔ Subsingleton M :=
-  Iff.trans
-    (by rw [← finrank_eq_rank]; norm_cast)
-    (rank_zero_iff (R := R))
+    finrank R M = 0 ↔ Subsingleton M := by
+  rw [← rank_zero_iff (R := R), ← finrank_eq_rank]
+  norm_cast
 #align finite_dimensional.finrank_zero_iff FiniteDimensional.finrank_zero_iff
 
 end StrongRankCondition

Mathlib/LinearAlgebra/Dual.lean

@@ -1422,7 +1422,9 @@ theorem range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective (f : M
   have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
   convert this using 1
   -- Porting note: broken dot notation lean4#1910
-  · change range ((range f).subtype.comp f.rangeRestrict).dualMap = _
+  · calc
+      _ = range ((range f).subtype.comp f.rangeRestrict).dualMap := by simp
+      _ = _ := ?_
     rw [← dualMap_comp_dualMap, range_comp_of_range_eq_top]
     rwa [range_eq_top]
   · apply congr_arg

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

@@ -139,7 +139,7 @@ theorem isHermitian_diagonal_of_self_adjoint [DecidableEq n] (v : n → α) (h :
 #align matrix.is_hermitian_diagonal_of_self_adjoint Matrix.isHermitian_diagonal_of_self_adjoint
 
 /-- A diagonal matrix is hermitian if each diagonal entry is self-adjoint -/
-lemma isHermitian_diagonal_iff [DecidableEq n]{d : n → α} :
+lemma isHermitian_diagonal_iff [DecidableEq n] {d : n → α} :
     IsHermitian (diagonal d) ↔ (∀ i : n, IsSelfAdjoint (d i)) := by
   simp [isSelfAdjoint_iff, IsHermitian, conjTranspose, diagonal_transpose, diagonal_map]
 

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -632,7 +632,7 @@ theorem map_prod_of_prime [CommSemiring R] {f : ArithmeticFunction R}
 theorem map_prod_of_subset_primeFactors [CommSemiring R] {f : ArithmeticFunction R}
     (h_mult : ArithmeticFunction.IsMultiplicative f) (l : ℕ)
     (t : Finset ℕ) (ht : t ⊆ l.primeFactors) :
-     f (∏ a in t, a) = ∏ a : ℕ in t, f a :=
+    f (∏ a in t, a) = ∏ a : ℕ in t, f a :=
   map_prod_of_prime h_mult t fun _ a => prime_of_mem_primeFactors (ht a)
 
 theorem nat_cast {f : ArithmeticFunction ℕ} [Semiring R] (h : f.IsMultiplicative) :
@@ -764,7 +764,7 @@ theorem prodPrimeFactors [CommMonoidWithZero R] (f : ℕ → R) :
   rw [iff_ne_zero]
   refine ⟨prodPrimeFactors_apply one_ne_zero, ?_⟩
   intro x y hx hy hxy
-  have hxy₀: x*y ≠ 0 := by exact Nat.mul_ne_zero hx hy
+  have hxy₀ : x * y ≠ 0 := mul_ne_zero hx hy
   rw [prodPrimeFactors_apply hxy₀, prodPrimeFactors_apply hx, prodPrimeFactors_apply hy,
     Nat.primeFactors_mul hx hy, ← Finset.prod_union hxy.disjoint_primeFactors]
 
@@ -778,7 +778,8 @@ theorem prodPrimeFactors_add_of_squarefree [CommSemiring R] {f g : ArithmeticFun
     factors_eq]
   apply Finset.sum_congr rfl
   intro t ht
-  erw [t.prod_val, ← prod_primeFactors_sdiff_of_squarefree hn (Finset.mem_powerset.mp ht),
+  rw [t.prod_val, Function.id_def,
+    ← prod_primeFactors_sdiff_of_squarefree hn (Finset.mem_powerset.mp ht),
     hf.map_prod_of_subset_primeFactors n t (Finset.mem_powerset.mp ht),
     ← hg.map_prod_of_subset_primeFactors n (_ \ t) (Finset.sdiff_subset _ t)]