[Merged by Bors] - chore: Remove unnecessary "rw"s

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

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

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

Mathlib/Algebra/DirectSum/Decomposition.lean

@@ -135,7 +135,7 @@ theorem decompose_of_mem {x : M} {i : ι} (hx : x ∈ ℳ i) :
 #align direct_sum.decompose_of_mem DirectSum.decompose_of_mem
 
 theorem decompose_of_mem_same {x : M} {i : ι} (hx : x ∈ ℳ i) : (decompose ℳ x i : M) = x := by
-  rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
+  rw [decompose_of_mem _ hx, DirectSum.of_eq_same]
 #align direct_sum.decompose_of_mem_same DirectSum.decompose_of_mem_same
 
 theorem decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j) :

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 _ _)

Mathlib/Algebra/Module/Zlattice.lean

@@ -162,7 +162,7 @@ theorem fract_zspan_add (m : E) {v : E} (h : v ∈ span ℤ (Set.range b)) :
   simp_rw [repr_fract_apply, Int.fract_eq_fract]
   use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
   rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
-    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
+    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply]
 #align zspan.fract_zspan_add Zspan.fract_zspan_add
 
 @[simp]

Mathlib/Algebra/MonoidAlgebra/Grading.lean

@@ -183,7 +183,7 @@ instance gradeBy.gradedAlgebra : GradedAlgebra (gradeBy R f) :=
       ext : 2
       simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, AlgHom.coe_comp, Function.comp_apply,
         of_apply, AlgHom.coe_id, id_eq]
-      rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])
+      rw [decomposeAux_single, DirectSum.coeAlgHom_of])
     fun i x => by rw [decomposeAux_coe f x]
 #align add_monoid_algebra.grade_by.graded_algebra AddMonoidAlgebra.gradeBy.gradedAlgebra
 

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

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
 

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 :

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -386,7 +386,7 @@ theorem const_ext {f₁ f₂ g₁ g₂ : R} {U hu₁ hu₂} (h : f₁ * g₂ = f
     const R f₁ g₁ U hu₁ = const R f₂ g₂ U hu₂ :=
   Subtype.eq <|
     funext fun x =>
-      IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])
+      IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm])
 #align algebraic_geometry.structure_sheaf.const_ext AlgebraicGeometry.StructureSheaf.const_ext
 
 theorem const_congr {f₁ f₂ g₁ g₂ : R} {U hu} (hf : f₁ = f₂) (hg : g₁ = g₂) :

Mathlib/Analysis/Analytic/Composition.lean

@@ -115,7 +115,7 @@ theorem applyComposition_ones (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) :
   intro j hjn hj1
   obtain rfl : j = 0 := by linarith
   refine' congr_arg v _
-  rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]
+  rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding]
 #align formal_multilinear_series.apply_composition_ones FormalMultilinearSeries.applyComposition_ones
 
 theorem applyComposition_single (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : 0 < n)
@@ -407,7 +407,7 @@ theorem comp_id (p : FormalMultilinearSeries 𝕜 E F) : p.comp (id 𝕜 E) = p
     intros
     rw [applyComposition_ones]
     refine' congr_arg v _
-    rw [Fin.ext_iff, Fin.coe_castLE, Fin.val_mk]
+    rw [Fin.ext_iff, Fin.coe_castLE]
   show
     ∀ b : Composition n,
       b ∈ Finset.univ → b ≠ Composition.ones n → compAlongComposition p (id 𝕜 E) b = 0

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 :=

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

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

@@ -165,7 +165,7 @@ theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E) :=
   refine' (nhds_basis_abs_convex_open 𝕜 E).to_hasBasis (fun s hs => _) fun s hs => _
   · refine' ⟨s, ⟨_, rfl.subset⟩⟩
     convert (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
-    rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
+    rw [gaugeSeminormFamily_ball]
   refine' ⟨s, ⟨_, rfl.subset⟩⟩
   rw [SeminormFamily.basisSets_iff] at hs
   rcases hs with ⟨t, r, hr, rfl⟩

Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

@@ -262,7 +262,7 @@ def toConstProdContinuousLinearMap : (V →A[𝕜] W) ≃ₗᵢ[𝕜] W × (V 
     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]
+    rw [ContinuousAffineMap.coe_const]
   right_inv := by rintro ⟨v, f⟩; ext <;> simp
   map_add' _ _ := rfl
   map_smul' _ _ := rfl

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) :

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -53,7 +53,7 @@ theorem log_of_pos (hx : 0 < x) : log x = expOrderIso.symm ⟨x, hx⟩ := by
 #align real.log_of_pos Real.log_of_pos
 
 theorem exp_log_eq_abs (hx : x ≠ 0) : exp (log x) = |x| := by
-  rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]
+  rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply]
 #align real.exp_log_eq_abs Real.exp_log_eq_abs
 
 theorem exp_log (hx : 0 < x) : exp (log x) = x := by

Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean

@@ -224,7 +224,7 @@ theorem sin_pi_mul_eq (z : ℂ) (n : ℕ) :
     set A := ∏ j in Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)
     set B := ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)
     set C := ∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n)
-    have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add, mul_one]
+    have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add]
     have : (∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n.succ)) = (2 * (n : ℝ) + 1) / (2 * n + 2) * C := by
       rw [integral_cos_pow_eq]
       dsimp only

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₁ _ _ _ _

Mathlib/Combinatorics/HalesJewett.lean

@@ -360,7 +360,7 @@ theorem exists_mono_homothetic_copy {M κ : Type*} [AddCommMonoid M] (S : Finset
     apply Finset.sum_congr rfl
     intro i hi
     rw [hs, Finset.mem_filter] at hi
-    rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
+    rw [l.apply_none _ _ hi.right]
   · apply Finset.sum_congr rfl
     intro i hi
     rw [hs, Finset.compl_filter, Finset.mem_filter] at hi

Mathlib/Data/Finset/LocallyFinite.lean

@@ -658,7 +658,7 @@ theorem card_Ico_eq_card_Icc_sub_one (a b : α) : (Ico a b).card = (Icc a b).car
     by_cases h : a ≤ b
     · rw [Icc_eq_cons_Ico h, card_cons]
       exact (Nat.add_sub_cancel _ _).symm
-    · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, zero_tsub]
+    · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty]
 #align finset.card_Ico_eq_card_Icc_sub_one Finset.card_Ico_eq_card_Icc_sub_one
 
 theorem card_Ioc_eq_card_Icc_sub_one (a b : α) : (Ioc a b).card = (Icc a b).card - 1 :=
@@ -670,7 +670,7 @@ theorem card_Ioo_eq_card_Ico_sub_one (a b : α) : (Ioo a b).card = (Ico a b).car
     by_cases h : a < b
     · rw [Ico_eq_cons_Ioo h, card_cons]
       exact (Nat.add_sub_cancel _ _).symm
-    · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, zero_tsub]
+    · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty]
 #align finset.card_Ioo_eq_card_Ico_sub_one Finset.card_Ioo_eq_card_Ico_sub_one
 
 theorem card_Ioo_eq_card_Ioc_sub_one (a b : α) : (Ioo a b).card = (Ioc a b).card - 1 :=

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

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]

Mathlib/Data/Nat/Bitwise.lean

@@ -199,7 +199,7 @@ theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n
   induction' n using Nat.binaryRec with b n hn
   · rfl
   · have : b = false := by simpa using h 0
-    rw [this, bit_false, bit0_val, hn fun i => by rw [← h (i + 1), testBit_bit_succ], mul_zero]
+    rw [this, bit_false, bit0_val, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]
 #align nat.zero_of_test_bit_eq_ff Nat.zero_of_testBit_eq_false
 
 theorem testBit_eq_false_of_lt {n i} (h : n < 2 ^ i) : n.testBit i = false := by
@@ -453,8 +453,7 @@ theorem xor_trichotomy {a b c : ℕ} (h : a ≠ b ^^^ c) :
       rfl
     ) h fun j hj => by
       -- Porting note: this was originally `simp [hi' _ hj]`
-      rw [Nat.testBit_xor, hi' _ hj, Bool.xor, Bool.xor_false, eq_self_iff_true]
-      trivial
+      rw [Nat.testBit_xor, hi' _ hj, Bool.xor, Bool.xor_false]
 #align nat.lxor_trichotomy Nat.xor_trichotomy
 
 theorem lt_xor_cases {a b c : ℕ} (h : a < b ^^^ c) : a ^^^ c < b ∨ a ^^^ b < c :=

Mathlib/Data/Nat/Hyperoperation.lean

@@ -45,7 +45,7 @@ def hyperoperation : ℕ → ℕ → ℕ → ℕ
 -- Basic hyperoperation lemmas
 @[simp]
 theorem hyperoperation_zero (m : ℕ) : hyperoperation 0 m = Nat.succ :=
-  funext fun k => by rw [hyperoperation, Nat.succ_eq_add_one]
+  funext fun k => by rw [hyperoperation]
 #align hyperoperation_zero hyperoperation_zero
 
 theorem hyperoperation_ge_three_eq_one (n m : ℕ) : hyperoperation (n + 3) m 0 = 1 := by

Mathlib/Data/Nat/Log.lean

@@ -206,7 +206,7 @@ theorem log_antitone_left {n : ℕ} : AntitoneOn (fun b => log b n) (Set.Ioi 1)
 @[simp]
 theorem log_div_base (b n : ℕ) : log b (n / b) = log b n - 1 := by
   rcases le_or_lt b 1 with hb | hb
-  · rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
+  · rw [log_of_left_le_one hb, log_of_left_le_one hb]
   cases' lt_or_le n b with h h
   · rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
   rw [log_of_one_lt_of_le hb h, add_tsub_cancel_right]

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
 

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

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 : ℕ} :

Mathlib/Data/Polynomial/Mirror.lean

@@ -173,14 +173,14 @@ variable [NoZeroDivisors R]
 
 theorem natDegree_mul_mirror : (p * p.mirror).natDegree = 2 * p.natDegree := by
   by_cases hp : p = 0
-  · rw [hp, zero_mul, natDegree_zero, mul_zero]
+  · rw [hp, zero_mul, natDegree_zero]
   rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]
 #align polynomial.nat_degree_mul_mirror Polynomial.natDegree_mul_mirror
 
 theorem natTrailingDegree_mul_mirror :
     (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree := by
   by_cases hp : p = 0
-  · rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
+  · rw [hp, zero_mul, natTrailingDegree_zero]
   rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]
 #align polynomial.nat_trailing_degree_mul_mirror Polynomial.natTrailingDegree_mul_mirror
 

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'
 

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

Mathlib/Data/Set/Function.lean

@@ -804,7 +804,7 @@ theorem surjOn_iff_exists_map_subtype :
     ⟨_, (mapsTo_image f s).restrict f s _, h, surjective_mapsTo_image_restrict _ _, fun _ => rfl⟩,
     fun ⟨t', g, htt', hg, hfg⟩ y hy =>
     let ⟨x, hx⟩ := hg ⟨y, htt' hy⟩
-    ⟨x, x.2, by rw [hfg, hx, Subtype.coe_mk]⟩⟩
+    ⟨x, x.2, by rw [hfg, hx]⟩⟩
 #align set.surj_on_iff_exists_map_subtype Set.surjOn_iff_exists_map_subtype
 
 theorem surjOn_empty (f : α → β) (s : Set α) : SurjOn f s ∅ :=

Mathlib/FieldTheory/Adjoin.lean

@@ -902,7 +902,7 @@ theorem exists_finset_of_mem_supr'' {ι : Type*} {f : ι → IntermediateField F
   intro x1 hx1
   refine' SetLike.le_def.mp (le_iSup_of_le ⟨i, x1, hx1⟩ _)
     (subset_adjoin F (rootSet (minpoly F x1) E) _)
-  · rw [IntermediateField.minpoly_eq, Subtype.coe_mk]
+  · rw [IntermediateField.minpoly_eq]
   · rw [mem_rootSet_of_ne, minpoly.aeval]
     exact minpoly.ne_zero (isIntegral_iff.mp (h i ⟨x1, hx1⟩).isIntegral)
 #align intermediate_field.exists_finset_of_mem_supr'' IntermediateField.exists_finset_of_mem_supr''

Mathlib/GroupTheory/OrderOfElement.lean

@@ -614,7 +614,7 @@ lemma finEquivPowers_apply (x : G) (hx) {n : Fin (orderOf x)} :
 @[to_additive (attr := simp, nolint simpNF) finEquivMultiples_symm_apply]
 lemma finEquivPowers_symm_apply (x : G) (hx) (n : ℕ) {hn : ∃ m : ℕ, x ^ m = x ^ n} :
     (finEquivPowers x hx).symm ⟨x ^ n, hn⟩ = ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩ := by
-  rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]
+  rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf]
 #align fin_equiv_powers_symm_apply finEquivPowers_symm_apply
 #align fin_equiv_multiples_symm_apply finEquivMultiples_symm_apply