diff --git a/Mathlib/Algebra/Expr.lean b/Mathlib/Algebra/Expr.lean
index 73a6d49606b8e..df4e9330035a2 100644
--- a/Mathlib/Algebra/Expr.lean
+++ b/Mathlib/Algebra/Expr.lean
@@ -9,8 +9,6 @@ import Qq
 /-! # Helpers to invoke functions involving algebra at tactic time
 
 This file provides instances on `x y : Q($α)` such that `x + y = q($x + $y)`.
-
-Porting note: This has been rewritten to use `Qq` instead of `Expr`.
 -/
 open Qq
 
diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean
index d7c8967bbf9a0..78cdb51b06d87 100644
--- a/Mathlib/Algebra/Free.lean
+++ b/Mathlib/Algebra/Free.lean
@@ -260,7 +260,6 @@ end Category
 
 end FreeMagma
 
--- Porting note: changed String to Lean.Format
 #adaptation_note /-- around nightly-2024-02-25, we need to write `mul x y` in the second pattern,
 instead of `x * y`. -/
 /-- Representation of an element of a free magma. -/
diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean
index 02480271a1392..3cbed430844f5 100644
--- a/Mathlib/Algebra/GeomSum.lean
+++ b/Mathlib/Algebra/GeomSum.lean
@@ -31,8 +31,6 @@ which `x` and `y` commute. Even versions not using division or subtraction, vali
 are recorded.
 -/
 
--- Porting note: corrected type in the description of `geom_sum₂_Ico` (in the doc string only).
-
 universe u
 
 variable {α : Type u}
@@ -72,7 +70,6 @@ theorem one_geom_sum (n : ℕ) : ∑ i ∈ range n, (1 : α) ^ i = n := by simp
 theorem op_geom_sum (x : α) (n : ℕ) : op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ i := by
   simp
 
--- Porting note: linter suggested to change left hand side
 @[simp]
 theorem op_geom_sum₂ (x y : α) (n : ℕ) : ∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i =
     ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i) := by
diff --git a/Mathlib/Algebra/Group/Int.lean b/Mathlib/Algebra/Group/Int.lean
index 7748ade5f0533..d0d47342d4add 100644
--- a/Mathlib/Algebra/Group/Int.lean
+++ b/Mathlib/Algebra/Group/Int.lean
@@ -146,13 +146,10 @@ lemma ofNat_isUnit {n : ℕ} : IsUnit (n : ℤ) ↔ IsUnit n := by simp [isUnit_
 lemma isUnit_mul_self (hu : IsUnit u) : u * u = 1 :=
   (isUnit_eq_one_or hu).elim (fun h ↦ h.symm ▸ rfl) fun h ↦ h.symm ▸ rfl
 
--- Porting note: this was proven in mathlib3 with `tidy` which hasn't been ported yet
 lemma isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b)
     (hc : IsUnit c) (hd : IsUnit d) : a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c := by
   rw [isUnit_iff] at ha hb hc hd
-  cases ha <;> cases hb <;> cases hc <;> cases hd <;>
-      subst a <;> subst b <;> subst c <;> subst d <;>
-    simp (config := {decide := true})
+  aesop
 
 lemma eq_one_or_neg_one_of_mul_eq_neg_one (h : u * v = -1) : u = 1 ∨ u = -1 :=
   Or.elim (eq_one_or_neg_one_of_mul_eq_neg_one' h) (fun H => Or.inl H.1) fun H => Or.inr H.1