diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index fd318fbb80454..62732d1f94a16 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -147,8 +147,7 @@ theorem CharP.intCast_eq_intCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b
 #align char_p.int_cast_eq_int_cast CharP.intCast_eq_intCast
 
 theorem CharP.natCast_eq_natCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} :
-    (a : R) = b ↔ a ≡ b [MOD p] :=
-  by
+    (a : R) = b ↔ a ≡ b [MOD p] := by
   rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
   exact (CharP.intCast_eq_intCast _ _).trans Int.coe_nat_modEq_iff
 #align char_p.nat_cast_eq_nat_cast CharP.natCast_eq_natCast
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index 86582722abb6c..6aa32f94108f6 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -496,7 +496,7 @@ theorem inv_mul' : (a * b)⁻¹ = a⁻¹ / b := by simp
 #align inv_mul' inv_mul'
 #align neg_add' neg_add'
 
-@[to_additive (attr := simp)]
+@[to_additive] -- Porting note: this is tagged simp in mathlib3, but simp in mathlib4 can prove this
 theorem inv_div_inv : a⁻¹ / b⁻¹ = b / a := by simp
 #align inv_div_inv inv_div_inv
 #align neg_sub_neg neg_sub_neg
diff --git a/Mathlib/Data/Int/GCD.lean b/Mathlib/Data/Int/GCD.lean
index 9c9fb3cd076a1..7854766550a9f 100644
--- a/Mathlib/Data/Int/GCD.lean
+++ b/Mathlib/Data/Int/GCD.lean
@@ -307,11 +307,11 @@ theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * natAbs j :
 #align int.gcd_mul_right Int.gcd_mul_right
 
 theorem gcd_pos_of_ne_zero_left {i : ℤ} (j : ℤ) (hi : i ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_left _ $ natAbs_pos.2 hi
+  Nat.gcd_pos_of_pos_left _ <| natAbs_pos.2 hi
 #align int.gcd_pos_of_ne_zero_left Int.gcd_pos_of_ne_zero_left
 
 theorem gcd_pos_of_ne_zero_right (i : ℤ) {j : ℤ} (hj : j ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_right _ $ natAbs_pos.2 hj
+  Nat.gcd_pos_of_pos_right _ <| natAbs_pos.2 hj
 #align int.gcd_pos_of_ne_zero_right Int.gcd_pos_of_ne_zero_right
 
 theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := by
diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index 8e64443a3b94a..13ef84dcd8b0a 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -128,8 +128,7 @@ protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m]
   modEq_iff_dvd.2 <| d.trans h.dvd
 #align int.modeq.of_dvd Int.ModEq.of_dvd
 
-protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=
-  by
+protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] := by
   obtain hc | rfl | hc := lt_trichotomy c 0
   · rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
     simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
@@ -305,8 +304,7 @@ theorem mod_coprime {a b : ℕ} (hab : Nat.coprime a b) : ∃ y : ℤ, a * y ≡
 
 theorem exists_unique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) :
     ∃ z : ℤ, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b] :=
-  ⟨a % b, emod_nonneg _ (ne_of_gt hb),
-    by
+  ⟨a % b, emod_nonneg _ (ne_of_gt hb), by
     have : a % b < |b| := emod_lt _ (ne_of_gt hb)
     rwa [abs_of_pos hb] at this, by simp [ModEq]⟩
 #align int.exists_unique_equiv Int.exists_unique_equiv
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index 52aabaa51ce8f..2ff111fd2de6f 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -637,8 +637,7 @@ instance (n : ℕ) : Inv (ZMod n) :=
 theorem inv_zero : ∀ n : ℕ, (0 : ZMod n)⁻¹ = 0
   | 0 => Int.sign_zero
   | n + 1 =>
-    show (Nat.gcdA _ (n + 1) : ZMod (n + 1)) = 0
-      by
+    show (Nat.gcdA _ (n + 1) : ZMod (n + 1)) = 0 by
       rw [val_zero]
       unfold Nat.gcdA Nat.xgcd Nat.xgcdAux
       rfl
@@ -654,8 +653,7 @@ theorem mul_inv_eq_gcd {n : ℕ} (a : ZMod n) : a * a⁻¹ = Nat.gcd a.val n :=
   · calc
       a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
         rw [nat_cast_self, MulZeroClass.zero_mul, add_zero]
-      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) :=
-        by
+      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
         push_cast
         rw [nat_cast_zmod_val]
         rfl
@@ -768,8 +766,7 @@ def chineseRemainder {m n : ℕ} (h : m.coprime n) : ZMod (m * n) ≃+* ZMod m 
       haveI : NeZero (m * n) := ⟨hmn0⟩
       haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
       haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
-      have left_inv : Function.LeftInverse inv_fun to_fun :=
-        by
+      have left_inv : Function.LeftInverse inv_fun to_fun := by
         intro x
         dsimp only [dvd_mul_left, dvd_mul_right, ZMod.castHom_apply]
         conv_rhs => rw [← ZMod.nat_cast_zmod_val x]
@@ -802,15 +799,13 @@ theorem le_div_two_iff_lt_neg (n : ℕ) [hn : Fact ((n : ℕ) % 2 = 1)] {x : ZMo
       simp [fact_iff] at hn⟩
   have _hn2 : (n : ℕ) / 2 < n :=
     Nat.div_lt_of_lt_mul ((lt_mul_iff_one_lt_left <| NeZero.pos n).2 (by decide))
-  have hn2' : (n : ℕ) - n / 2 = n / 2 + 1 :=
-    by
+  have hn2' : (n : ℕ) - n / 2 = n / 2 + 1 := by
     conv =>
       lhs
       congr
       rw [← Nat.succ_sub_one n, Nat.succ_sub <| NeZero.pos n]
     rw [← Nat.two_mul_odd_div_two hn.1, two_mul, ← Nat.succ_add, add_tsub_cancel_right]
-  have hxn : (n : ℕ) - x.val < n :=
-    by
+  have hxn : (n : ℕ) - x.val < n := by
     rw [tsub_lt_iff_tsub_lt x.val_le le_rfl, tsub_self]
     rw [← ZMod.nat_cast_zmod_val x] at hx0
     exact Nat.pos_of_ne_zero fun h => by simp [h] at hx0
@@ -960,8 +955,8 @@ theorem valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) : a.valMinAbs * 2 = n 
     exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le
 #align zmod.val_min_abs_mul_two_eq_iff ZMod.valMinAbs_mul_two_eq_iff
 
-theorem valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs * 2 ∈ Set.Ioc (-n : ℤ) n :=
-  by
+theorem valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) :
+    x.valMinAbs * 2 ∈ Set.Ioc (-n : ℤ) n := by
   simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]; split_ifs with h
   · refine' ⟨(neg_lt_zero.2 <| by exact_mod_cast NeZero.pos n).trans_le (mul_nonneg _ _), h⟩
     exacts[Nat.cast_nonneg _, zero_le_two]
@@ -975,8 +970,7 @@ theorem valMinAbs_spec {n : ℕ} [NeZero n] (x : ZMod n) (y : ℤ) :
     x.valMinAbs = y ↔ x = y ∧ y * 2 ∈ Set.Ioc (-n : ℤ) n :=
   ⟨by
     rintro rfl
-    exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩, fun h =>
-    by
+    exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩, fun h => by
     rw [← sub_eq_zero]
     apply @Int.eq_zero_of_abs_lt_dvd n
     · rw [← int_cast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
@@ -1089,8 +1083,7 @@ theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
 
 --porting note: There was an extraneous `nat_` in the mathlib name
 @[simp]
-theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 :=
-  by
+theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 := by
   refine' ⟨fun ha => _, valMinAbs_natCast_of_le_half⟩
   rw [← Int.natAbs_ofNat a, ← ha]
   exact natAbs_valMinAbs_le a