diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
index e3d7d3b7b1812..f0583990ba7a5 100644
--- a/Mathlib/Algebra/Algebra/Operations.lean
+++ b/Mathlib/Algebra/Algebra/Operations.lean
@@ -596,7 +596,7 @@ def span.ringHom : SetSemiring A →+* Submodule R A where
   map_add' := span_union
   map_mul' s t := by
     dsimp only -- porting note: new, needed due to new-style structures
-    rw [SetSemiring.down_mul, span_mul_span, ← image_mul_prod]
+    rw [SetSemiring.down_mul, span_mul_span]
 #align submodule.span.ring_hom Submodule.span.ringHom
 
 section
diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index e01db35d76d47..ec74a12e6533e 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -2174,7 +2174,7 @@ theorem prod_eq_zero_iff : ∏ x in s, f x = 0 ↔ ∃ a ∈ s, f a = 0 := by
   classical
     induction' s using Finset.induction_on with a s ha ih
     · exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
-    · rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih, ← bex_def]
+    · rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]
 #align finset.prod_eq_zero_iff Finset.prod_eq_zero_iff
 
 theorem prod_ne_zero_iff : ∏ x in s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0 := by
diff --git a/Mathlib/Algebra/DirectSum/Algebra.lean b/Mathlib/Algebra/DirectSum/Algebra.lean
index 35e606e426872..bae2aaab3f22c 100644
--- a/Mathlib/Algebra/DirectSum/Algebra.lean
+++ b/Mathlib/Algebra/DirectSum/Algebra.lean
@@ -68,7 +68,7 @@ instance _root_.GradedMonoid.isScalarTower_right :
     IsScalarTower R (GradedMonoid A) (GradedMonoid A) where
   smul_assoc s x y := by
     dsimp
-    rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]
+    rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc]
 
 instance : Algebra R (⨁ i, A i) where
   toFun := (DirectSum.of A 0).comp GAlgebra.toFun
diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean
index 726e8998e92d1..308e8c6dbb5e2 100644
--- a/Mathlib/Algebra/GCDMonoid/Basic.lean
+++ b/Mathlib/Algebra/GCDMonoid/Basic.lean
@@ -1145,7 +1145,7 @@ noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α)
       dsimp only
       split_ifs with h h_1
       · rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
-      · rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _), mul_zero]
+      · rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]
       rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]
     lcm_zero_left := fun a => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
     lcm_zero_right := fun a => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
diff --git a/Mathlib/Algebra/Quandle.lean b/Mathlib/Algebra/Quandle.lean
index 4514901aa455f..3d8b9425aca0d 100644
--- a/Mathlib/Algebra/Quandle.lean
+++ b/Mathlib/Algebra/Quandle.lean
@@ -163,7 +163,7 @@ lemma act_act_self_eq (x y : S) : (x ◃ y) ◃ x = x ◃ y := by
   rw [h, ← Shelf.self_distrib, act_one]
 #align unital_shelf.act_act_self_eq UnitalShelf.act_act_self_eq
 
-lemma act_idem (x : S) : (x ◃ x) = x := by rw [← act_one x, ← Shelf.self_distrib, act_one, act_one]
+lemma act_idem (x : S) : (x ◃ x) = x := by rw [← act_one x, ← Shelf.self_distrib, act_one]
 #align unital_shelf.act_idem UnitalShelf.act_idem
 
 lemma act_self_act_eq (x y : S) : x ◃ (x ◃ y) = x ◃ y := by
diff --git a/Mathlib/Algebra/Regular/Basic.lean b/Mathlib/Algebra/Regular/Basic.lean
index 82a96e3e01c77..50947cd330356 100644
--- a/Mathlib/Algebra/Regular/Basic.lean
+++ b/Mathlib/Algebra/Regular/Basic.lean
@@ -280,11 +280,11 @@ theorem not_isRegular_zero [Nontrivial R] : ¬IsRegular (0 : R) := fun h => IsRe
 
 @[simp] lemma IsLeftRegular.mul_left_eq_zero_iff (hb : IsLeftRegular b) : b * a = 0 ↔ a = 0 := by
   nth_rw 1 [← mul_zero b]
-  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, mul_zero]⟩
+  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
 
 @[simp] lemma IsRightRegular.mul_right_eq_zero_iff (hb : IsRightRegular b) : a * b = 0 ↔ a = 0 := by
   nth_rw 1 [← zero_mul b]
-  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, zero_mul]⟩
+  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
 
 end MulZeroClass
 
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
index 96f7efa185333..feeb401d91ba1 100644
--- a/Mathlib/AlgebraicGeometry/OpenImmersion.lean
+++ b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -594,8 +594,7 @@ theorem range_pullback_to_base_of_left :
       Set.range f.1.base ∩ Set.range g.1.base := by
   rw [pullback.condition, Scheme.comp_val_base, coe_comp, Set.range_comp,
     range_pullback_snd_of_left, Opens.carrier_eq_coe,
-    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range,
-    Set.inter_comm]
+    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range]
 #align algebraic_geometry.IsOpenImmersion.range_pullback_to_base_of_left AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left
 
 theorem range_pullback_to_base_of_right :
diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean
index 44f616793562a..7e123d7f205d0 100644
--- a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean
+++ b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean
@@ -66,7 +66,7 @@ theorem coe_splitLower : (splitLower I i x : Set (ι → ℝ)) = ↑I ∩ { y |
   ext y
   simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and, ← Pi.le_def,
     le_update_iff, le_min_iff, and_assoc, and_forall_ne (p := fun j => y j ≤ upper I j) i, mem_def]
-  rw [and_comm (a := y i ≤ x), Pi.le_def]
+  rw [and_comm (a := y i ≤ x)]
 #align box_integral.box.coe_split_lower BoxIntegral.Box.coe_splitLower
 
 theorem splitLower_le : I.splitLower i x ≤ I :=
diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
index 2b7e71dc5a8c5..27ae6f8bf09b7 100644
--- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
+++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
@@ -268,8 +268,7 @@ theorem tendsto_integral_exp_smul_cocompact_of_inner_product (μ : Measure V) [
   have : (fun w : V →L[ℝ] ℝ => ∫ v, e[-w v] • f v) = (fun w : V => ∫ v, e[-⟪v, w⟫] • f v) ∘ A := by
     ext1 w
     congr 1 with v : 1
-    rw [← inner_conj_symm, IsROrC.conj_to_real, InnerProductSpace.toDual_symm_apply,
-      Real.fourierChar_apply]
+    rw [← inner_conj_symm, IsROrC.conj_to_real, InnerProductSpace.toDual_symm_apply]
   rw [this]
   exact
     (tendsto_integral_exp_inner_smul_cocompact f).comp
diff --git a/Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean b/Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean
index abe54af7a18f5..a10dc961d3632 100644
--- a/Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean
+++ b/Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean
@@ -260,9 +260,7 @@ def toConstProdContinuousLinearMap : (V →A[𝕜] W) ≃ₗᵢ[𝕜] W × (V 
   left_inv f := by
     ext
     rw [f.decomp]
-    -- Porting note: previously `simp` closed the goal, but now we need to rewrite:
-    simp only [coe_add, ContinuousLinearMap.coe_toContinuousAffineMap, Pi.add_apply]
-    rw [ContinuousAffineMap.coe_const, Function.const_apply]
+    simp only [coe_add, ContinuousLinearMap.coe_toContinuousAffineMap, Pi.add_apply, coe_const]
   right_inv := by rintro ⟨v, f⟩; ext <;> simp
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
index efccafa5dbfe9..fe0ffdfbcee12 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
@@ -91,7 +91,7 @@ theorem log_ofReal_mul {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) :
 #align complex.log_of_real_mul Complex.log_ofReal_mul
 
 theorem log_mul_ofReal (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) :
-    log (x * r) = Real.log r + log x := by rw [mul_comm, log_ofReal_mul hr hx, add_comm]
+    log (x * r) = Real.log r + log x := by rw [mul_comm, log_ofReal_mul hr hx]
 #align complex.log_mul_of_real Complex.log_mul_ofReal
 
 lemma log_mul_eq_add_log_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
diff --git a/Mathlib/CategoryTheory/Localization/Composition.lean b/Mathlib/CategoryTheory/Localization/Composition.lean
index fd7849c6adf5e..ad6cdbd639b37 100644
--- a/Mathlib/CategoryTheory/Localization/Composition.lean
+++ b/Mathlib/CategoryTheory/Localization/Composition.lean
@@ -113,7 +113,7 @@ lemma of_comp (W₃ : MorphismProperty C₁)
     have : (L₁ ⋙ W₂.Q).IsLocalization W₃ :=
       comp L₁ W₂.Q W₁ W₂ W₃ (fun X Y f hf => Localization.inverts W₂.Q W₂ _
         (by simpa only [hW₂₃] using W₃.map_mem_map _ _ hf)) hW₁₃
-        (by rw [hW₂₃, MorphismProperty.subset_iff_le])
+        (by rw [hW₂₃])
     exact IsLocalization.of_equivalence_target W₂.Q W₂ L₂
       (Localization.uniq (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃)
       (liftNatIso L₁ W₁ _ _ _ _
diff --git a/Mathlib/Data/Int/Cast/Basic.lean b/Mathlib/Data/Int/Cast/Basic.lean
index 191a8aa7b66ca..f662d1d520fd3 100644
--- a/Mathlib/Data/Int/Cast/Basic.lean
+++ b/Mathlib/Data/Int/Cast/Basic.lean
@@ -141,15 +141,15 @@ theorem cast_bit1 (n : ℤ) : ((bit1 n : ℤ) : R) = bit1 (n : R) :=
 end deprecated
 
 theorem cast_two : ((2 : ℤ) : R) = 2 :=
-  show (((2 : ℕ) : ℤ) : R) = ((2 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat]
+  show (((2 : ℕ) : ℤ) : R) = ((2 : ℕ) : R) by rw [cast_ofNat]
 #align int.cast_two Int.cast_two
 
 theorem cast_three : ((3 : ℤ) : R) = 3 :=
-  show (((3 : ℕ) : ℤ) : R) = ((3 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat]
+  show (((3 : ℕ) : ℤ) : R) = ((3 : ℕ) : R) by rw [cast_ofNat]
 #align int.cast_three Int.cast_three
 
 theorem cast_four : ((4 : ℤ) : R) = 4 :=
-  show (((4 : ℕ) : ℤ) : R) = ((4 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat]
+  show (((4 : ℕ) : ℤ) : R) = ((4 : ℕ) : R) by rw [cast_ofNat]
 #align int.cast_four Int.cast_four
 
 end Int
diff --git a/Mathlib/Data/List/Rotate.lean b/Mathlib/Data/List/Rotate.lean
index 2a5f5d5271b26..e25c205bc1131 100644
--- a/Mathlib/Data/List/Rotate.lean
+++ b/Mathlib/Data/List/Rotate.lean
@@ -337,7 +337,7 @@ theorem rotate_eq_iff {l l' : List α} {n : ℕ} :
     l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length) := by
   rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
   rcases l'.length.zero_le.eq_or_lt with hl | hl
-  · rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil, rotate_eq_nil_iff]
+  · rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
   · rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
     · simp [← hn]
     · rw [mod_eq_of_lt (tsub_lt_self hl hn), tsub_add_cancel_of_le (α := ℕ), mod_self, rotate_zero]
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 2bdce87de950b..db02ea8e95cbb 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -1492,7 +1492,7 @@ theorem cast_sub [Ring α] (m n) : ((m - n : ZNum) : α) = m - n := by simp [sub
 @[norm_cast] -- @[simp] -- Porting note: simp can prove this
 theorem neg_of_int : ∀ n, ((-n : ℤ) : ZNum) = -n
   | (n + 1 : ℕ) => rfl
-  | 0 => by rw [Int.cast_neg, Int.cast_zero]
+  | 0 => by rw [Int.cast_neg]
   | -[n+1] => (zneg_zneg _).symm
 #align znum.neg_of_int ZNum.neg_of_int
 
diff --git a/Mathlib/Data/PNat/Factors.lean b/Mathlib/Data/PNat/Factors.lean
index 41a602c485b9b..b3c1be95623b1 100644
--- a/Mathlib/Data/PNat/Factors.lean
+++ b/Mathlib/Data/PNat/Factors.lean
@@ -225,7 +225,7 @@ theorem prod_add (u v : PrimeMultiset) : (u + v).prod = u.prod * v.prod := by
 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]
+  | succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ]
 #align prime_multiset.prod_smul PrimeMultiset.prod_smul
 
 end PrimeMultiset
diff --git a/Mathlib/Data/Polynomial/Eval.lean b/Mathlib/Data/Polynomial/Eval.lean
index c08030cde80de..3f07adff3079a 100644
--- a/Mathlib/Data/Polynomial/Eval.lean
+++ b/Mathlib/Data/Polynomial/Eval.lean
@@ -637,7 +637,7 @@ theorem C_mul_comp : (C a * p).comp r = C a * p.comp r := by
 
 @[simp]
 theorem nat_cast_mul_comp {n : ℕ} : ((n : R[X]) * p).comp r = n * p.comp r := by
-  rw [← C_eq_nat_cast, C_mul_comp, C_eq_nat_cast]
+  rw [← C_eq_nat_cast, C_mul_comp]
 #align polynomial.nat_cast_mul_comp Polynomial.nat_cast_mul_comp
 
 theorem mul_X_add_nat_cast_comp {n : ℕ} :
diff --git a/Mathlib/Data/Polynomial/Monic.lean b/Mathlib/Data/Polynomial/Monic.lean
index 9ce115b67ae70..067bc69d00a60 100644
--- a/Mathlib/Data/Polynomial/Monic.lean
+++ b/Mathlib/Data/Polynomial/Monic.lean
@@ -189,7 +189,7 @@ theorem degree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).degree = (q * p).deg
 
 nonrec theorem natDegree_mul' (hp : p.Monic) (hq : q ≠ 0) :
     (p * q).natDegree = p.natDegree + q.natDegree := by
-  rw [natDegree_mul', add_comm]
+  rw [natDegree_mul']
   simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
 #align polynomial.monic.nat_degree_mul' Polynomial.Monic.natDegree_mul'
 
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index f73bd283cd17c..6c3528994c501 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -79,7 +79,7 @@ theorem Finite.encard_eq_coe_toFinset_card (h : s.Finite) : s.encard = h.toFinse
 
 theorem encard_eq_coe_toFinset_card (s : Set α) [Fintype s] : encard s = s.toFinset.card := by
   have h := toFinite s
-  rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset, toFinset_card]
+  rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]
 
 theorem encard_coe_eq_coe_finsetCard (s : Finset α) : encard (s : Set α) = s.card := by
   rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]; simp
diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 60441c7363882..446df0ebf5f0a 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -126,8 +126,8 @@ theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
     simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm]
     refine' Eq.trans _ (congr_arg succ (bodd_add_div2 n))
     cases bodd n <;> simp [cond, not]
-    · rw [Nat.add_comm, Nat.add_succ]
-    · rw [succ_mul, Nat.add_comm 1, Nat.add_succ]
+    · rw [Nat.add_comm]
+    · rw [succ_mul, Nat.add_comm 1]
 #align nat.bodd_add_div2 Nat.bodd_add_div2
 
 theorem div2_val (n) : div2 n = n / 2 := by
diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
index 5b5061e2b527a..7c3fb7f641e45 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
@@ -1508,7 +1508,7 @@ theorem mem_affineSpan_insert_iff {s : AffineSubspace k P} {p1 : P} (hp1 : p1 
   · rintro ⟨r, p3, hp3, rfl⟩
     use r • (p2 -ᵥ p1), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p3 -ᵥ p1,
       vsub_mem_direction hp3 hp1
-    rw [vadd_vsub_assoc, add_comm]
+    rw [vadd_vsub_assoc]
 #align affine_subspace.mem_affine_span_insert_iff AffineSubspace.mem_affineSpan_insert_iff
 
 end AffineSubspace
diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean
index 150c7be3655a3..9517143203dd4 100644
--- a/Mathlib/LinearAlgebra/Basis.lean
+++ b/Mathlib/LinearAlgebra/Basis.lean
@@ -848,7 +848,7 @@ theorem basis_singleton_iff {R M : Type*} [Ring R] [Nontrivial R] [AddCommGroup
         map_smul' := fun c y => ?_ }⟩
     · simp [Finsupp.add_apply, add_smul]
     · simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]
-      rw [← smul_assoc, smul_eq_mul]
+      rw [← smul_assoc]
     · refine' smul_left_injective _ nz _
       simp only [Finsupp.single_eq_same]
       exact (w (f default • x)).choose_spec
diff --git a/Mathlib/LinearAlgebra/Dimension/Constructions.lean b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
index 7546115d6f18c..0afbdba7fa25f 100644
--- a/Mathlib/LinearAlgebra/Dimension/Constructions.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
@@ -304,7 +304,7 @@ theorem rank_fun_eq_lift_mul : Module.rank R (η → M) =
 #align rank_fun_eq_lift_mul rank_fun_eq_lift_mul
 
 theorem rank_fun' : Module.rank R (η → R) = Fintype.card η := by
-  rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one, Cardinal.natCast_inj]
+  rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]
 #align rank_fun' rank_fun'
 
 theorem rank_fin_fun (n : ℕ) : Module.rank R (Fin n → R) = n := by simp [rank_fun']
diff --git a/Mathlib/Logic/Equiv/List.lean b/Mathlib/Logic/Equiv/List.lean
index f55c6bb1faca3..fc96513bb1f0c 100644
--- a/Mathlib/Logic/Equiv/List.lean
+++ b/Mathlib/Logic/Equiv/List.lean
@@ -276,8 +276,7 @@ theorem list_ofNat_succ (v : ℕ) :
     show decodeList (succ v) = _ by
       cases' e : unpair v with v₁ v₂
       simp [decodeList, e]
-      rw [show decodeList v₂ = decode (α := List α) v₂ from rfl, decode_eq_ofNat, Option.seq_some,
-        Option.some.injEq]
+      rw [show decodeList v₂ = decode (α := List α) v₂ from rfl, decode_eq_ofNat, Option.seq_some]
 #align denumerable.list_of_nat_succ Denumerable.list_ofNat_succ
 
 end List
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 32c3853a2f81f..00ed2290e5636 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -681,8 +681,8 @@ theorem update_comm {α} [DecidableEq α] {β : α → Sort*} {a b : α} (h : a
   · rw [dif_pos h₁, dif_pos h₂]
     cases h (h₂.symm.trans h₁)
   · rw [dif_pos h₁, dif_pos h₁, dif_neg h₂]
-  · rw [dif_neg h₁, dif_neg h₁, dif_pos h₂]
-  · rw [dif_neg h₁, dif_neg h₁, dif_neg h₂]
+  · rw [dif_neg h₁, dif_neg h₁]
+  · rw [dif_neg h₁, dif_neg h₁]
 #align function.update_comm Function.update_comm
 
 @[simp]
diff --git a/Mathlib/MeasureTheory/Group/AddCircle.lean b/Mathlib/MeasureTheory/Group/AddCircle.lean
index 339abea6c2111..c06492c1b260f 100644
--- a/Mathlib/MeasureTheory/Group/AddCircle.lean
+++ b/Mathlib/MeasureTheory/Group/AddCircle.lean
@@ -101,7 +101,7 @@ theorem volume_of_add_preimage_eq (s I : Set <| AddCircle T) (u x : AddCircle T)
   have hsG : ∀ g : G, (g +ᵥ s : Set <| AddCircle T) =ᵐ[volume] s := by
     rintro ⟨y, hy⟩; exact (vadd_ae_eq_self_of_mem_zmultiples hs hy : _)
   rw [(isAddFundamentalDomain_of_ae_ball I u x hu hI).measure_eq_card_smul_of_vadd_ae_eq_self s hsG,
-    ← Nat.card_zmultiples u, Nat.card_eq_fintype_card]
+    ← Nat.card_zmultiples u]
 #align add_circle.volume_of_add_preimage_eq AddCircle.volume_of_add_preimage_eq
 
 end AddCircle
diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
index e7fbe81167fa3..6abe019ae1eb4 100644
--- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
@@ -404,7 +404,7 @@ theorem sSup_apply (ms : Set (OuterMeasure α)) (s : Set α) :
 
 @[simp]
 theorem iSup_apply {ι} (f : ι → OuterMeasure α) (s : Set α) : (⨆ i : ι, f i) s = ⨆ i, f i s := by
-  rw [iSup, sSup_apply, iSup_range, iSup]
+  rw [iSup, sSup_apply, iSup_range]
 #align measure_theory.outer_measure.supr_apply MeasureTheory.OuterMeasure.iSup_apply
 
 @[norm_cast]
diff --git a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean
index 8fb8a8a8403fc..6340bf954556f 100644
--- a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean
@@ -500,7 +500,7 @@ theorem toSignedMeasure_sub_apply {μ ν : Measure α} [IsFiniteMeasure μ] [IsF
     {i : Set α} (hi : MeasurableSet i) :
     (μ.toSignedMeasure - ν.toSignedMeasure) i = (μ i).toReal - (ν i).toReal := by
   rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
-    Measure.toSignedMeasure_apply_measurable hi, sub_eq_add_neg]
+    Measure.toSignedMeasure_apply_measurable hi]
 #align measure_theory.measure.to_signed_measure_sub_apply MeasureTheory.Measure.toSignedMeasure_sub_apply
 
 end Measure
diff --git a/Mathlib/NumberTheory/BernoulliPolynomials.lean b/Mathlib/NumberTheory/BernoulliPolynomials.lean
index 1d8e85b7b50d4..31d24af6abc64 100644
--- a/Mathlib/NumberTheory/BernoulliPolynomials.lean
+++ b/Mathlib/NumberTheory/BernoulliPolynomials.lean
@@ -108,7 +108,7 @@ theorem derivative_bernoulli_add_one (k : ℕ) :
   conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
   rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
   congr 3
-  rw [(choose_mul_succ_eq k m).symm, mul_comm]
+  rw [(choose_mul_succ_eq k m).symm]
 #align polynomial.derivative_bernoulli_add_one Polynomial.derivative_bernoulli_add_one
 
 theorem derivative_bernoulli (k : ℕ) :
diff --git a/Mathlib/NumberTheory/DiophantineApproximation.lean b/Mathlib/NumberTheory/DiophantineApproximation.lean
index f368d247ae71d..c1ed3afdf96aa 100644
--- a/Mathlib/NumberTheory/DiophantineApproximation.lean
+++ b/Mathlib/NumberTheory/DiophantineApproximation.lean
@@ -503,7 +503,7 @@ private theorem aux₃ :
   calc
     |(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| :=
       help₁ hξ₀.ne' Hv.ne' Hu.ne'
-    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁, abs_sub_comm]
+    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁]
     _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := ((mul_lt_mul_right H₁).mpr h')
     _ = (u' * (2 * v - 1) * fract ξ)⁻¹ := (help₂ hξ₀.ne' Hv.ne' Hv'.ne' Hu.ne')
     _ ≤ ((u' : ℝ) * (2 * u' - 1))⁻¹ := by
diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean
index 83e0012c672b0..9d763c498c181 100644
--- a/Mathlib/NumberTheory/NumberField/Embeddings.lean
+++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean
@@ -113,7 +113,7 @@ theorem finite_of_norm_le (B : ℝ) : {x : K | IsIntegral ℤ x ∧ ∀ φ : K 
     exact minpoly.natDegree_le x
   rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
   refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
-  rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
+  rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs]
 #align number_field.embeddings.finite_of_norm_le NumberField.Embeddings.finite_of_norm_le
 
 /-- An algebraic integer whose conjugates are all of norm one is a root of unity. -/
diff --git a/Mathlib/NumberTheory/RamificationInertia.lean b/Mathlib/NumberTheory/RamificationInertia.lean
index 25270d5737e24..85143539ed88e 100644
--- a/Mathlib/NumberTheory/RamificationInertia.lean
+++ b/Mathlib/NumberTheory/RamificationInertia.lean
@@ -370,7 +370,7 @@ theorem FinrankQuotientMap.span_eq_top [IsDomain R] [IsDomain S] [Algebra K L] [
     haveI := Ideal.Quotient.nontrivial hp
     calc
       Ideal.Quotient.mk p A.det = Matrix.det ((Ideal.Quotient.mk p).mapMatrix A) := by
-        rw [RingHom.map_det, RingHom.mapMatrix_apply]
+        rw [RingHom.map_det]
       _ = Matrix.det ((Ideal.Quotient.mk p).mapMatrix (Matrix.of A' - 1)) := rfl
       _ = Matrix.det fun i j =>
           (Ideal.Quotient.mk p) (A' i j) - (1 : Matrix (Fin n) (Fin n) (R ⧸ p)) i j := ?_
diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean
index d8b1e12dd8f11..0233e65fad586 100644
--- a/Mathlib/Order/OmegaCompletePartialOrder.lean
+++ b/Mathlib/Order/OmegaCompletePartialOrder.lean
@@ -399,7 +399,7 @@ noncomputable instance omegaCompletePartialOrder :
   le_ωSup c i := by
     intro x hx
     rw [← eq_some_iff] at hx ⊢
-    rw [ωSup_eq_some, ← hx]
+    rw [ωSup_eq_some]
     rw [← hx]
     exact ⟨i, rfl⟩
   ωSup_le := by
diff --git a/Mathlib/Order/SymmDiff.lean b/Mathlib/Order/SymmDiff.lean
index ef8abdd945cee..3a58200bc0e9f 100644
--- a/Mathlib/Order/SymmDiff.lean
+++ b/Mathlib/Order/SymmDiff.lean
@@ -413,7 +413,7 @@ theorem sdiff_symmDiff : c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b := by
 #align sdiff_symm_diff sdiff_symmDiff
 
 theorem sdiff_symmDiff' : c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b) := by
-  rw [sdiff_symmDiff, sdiff_sup, sup_comm]
+  rw [sdiff_symmDiff, sdiff_sup]
 #align sdiff_symm_diff' sdiff_symmDiff'
 
 @[simp]
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean
index 103026f4f819c..fac55ce8be09f 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean
@@ -1532,7 +1532,7 @@ theorem multiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_multipl
   obtain ⟨x, hx⟩ := (normalizedFactorsEquivSpanNormalizedFactors hr).surjective I
   obtain ⟨a, ha⟩ := x
   rw [hx.symm, Equiv.symm_apply_apply, Subtype.coe_mk,
-    multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity hr ha, hx]
+    multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity hr ha]
 #align multiplicity_normalized_factors_equiv_span_normalized_factors_symm_eq_multiplicity multiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_multiplicity
 
 end PID
diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
index 393ea32410ced..a36ced16154e9 100644
--- a/Mathlib/RingTheory/IsTensorProduct.lean
+++ b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -313,8 +313,7 @@ theorem IsBaseChange.ofEquiv (e : M ≃ₗ[R] N) : IsBaseChange R e.toLinearMap
     ext r q
     show (by let _ := I₂; exact r • q) = (by let _ := I₃; exact r • q)
     dsimp
-    rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul,
-      mul_one]
+    rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
   cases this
   refine'
     ⟨g.comp e.symm.toLinearMap, by
diff --git a/Mathlib/RingTheory/Norm.lean b/Mathlib/RingTheory/Norm.lean
index 61bae51d574f1..c7681784bc464 100644
--- a/Mathlib/RingTheory/Norm.lean
+++ b/Mathlib/RingTheory/Norm.lean
@@ -99,7 +99,7 @@ theorem norm_algebraMap_of_basis [Fintype ι] (b : Basis ι R S) (x : R) :
   haveI := Classical.decEq ι
   rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]
   convert @det_diagonal _ _ _ _ _ fun _ : ι => x
-  · ext (i j); rw [toMatrix_lsmul, Matrix.diagonal]
+  · ext (i j); rw [toMatrix_lsmul]
   · rw [Finset.prod_const, Finset.card_univ]
 #align algebra.norm_algebra_map_of_basis Algebra.norm_algebraMap_of_basis
 
diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
index 9f752b3074045..60002ffe5203b 100644
--- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
+++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
@@ -143,7 +143,7 @@ theorem cyclotomic_mul_prime_dvd_eq_pow (R : Type*) {p n : ℕ} [hp : Fact (Nat.
     rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
       this, Polynomial.map_pow]
   rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
-    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic, mul_comm]
+    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]
 #align polynomial.cyclotomic_mul_prime_dvd_eq_pow Polynomial.cyclotomic_mul_prime_dvd_eq_pow
 
 /-- If `R` is of characteristic `p` and `¬p ∣ m`, then
diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
index bf6f5efacc131..659b3a5a4b766 100644
--- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean
+++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
@@ -104,7 +104,7 @@ end
 theorem ascPochhammer_eval_cast (n k : ℕ) :
     (((ascPochhammer ℕ n).eval k : ℕ) : S) = ((ascPochhammer S n).eval k : S) := by
   rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
-      eval₂_at_nat_cast,Nat.cast_id, eq_natCast]
+      eval₂_at_nat_cast,Nat.cast_id]
 #align pochhammer_eval_cast ascPochhammer_eval_cast
 
 theorem ascPochhammer_eval_zero {n : ℕ} : (ascPochhammer S n).eval 0 = if n = 0 then 1 else 0 := by
diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean
index 29f271d1bb5a7..98e97a9cf68c3 100644
--- a/Mathlib/RingTheory/Trace.lean
+++ b/Mathlib/RingTheory/Trace.lean
@@ -502,8 +502,7 @@ theorem traceMatrix_of_matrix_mulVec [Fintype κ] (b : κ → B) (P : Matrix κ
     traceMatrix A (P.map (algebraMap A B) *ᵥ b) = P * traceMatrix A b * Pᵀ := by
   refine' AddEquiv.injective (transposeAddEquiv κ κ A) _
   rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
-    traceMatrix_of_matrix_vecMul, transpose_transpose, transpose_mul, transpose_transpose,
-    transpose_mul]
+    traceMatrix_of_matrix_vecMul, transpose_transpose]
 #align algebra.trace_matrix_of_matrix_mul_vec Algebra.traceMatrix_of_matrix_mulVec
 
 theorem traceMatrix_of_basis [Fintype κ] [DecidableEq κ] (b : Basis κ A B) :
diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean
index 4289267391043..ac22118749761 100644
--- a/Mathlib/SetTheory/Ordinal/Notation.lean
+++ b/Mathlib/SetTheory/Ordinal/Notation.lean
@@ -501,7 +501,7 @@ theorem repr_add : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ + o₂) = rep
         exact lt_of_le_of_lt (le_add_right _ _) this
       · simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos (repr e') omega_pos).2
           (nat_cast_le.2 n'.pos)
-    · rw [ee, ← add_assoc, ← mul_add, ← Nat.cast_add]
+    · rw [ee, ← add_assoc, ← mul_add]
 #align onote.repr_add ONote.repr_add
 
 theorem sub_nfBelow : ∀ {o₁ o₂ b}, NFBelow o₁ b → NF o₂ → NFBelow (o₁ - o₂) b