From 48a296cda0100e649fda683cef0262b9ae23e1ec Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 18 Jan 2025 14:49:41 +0000
Subject: [PATCH] chore: cleanup many porting notes in Combinatorics (#20823)

---
 Mathlib/Combinatorics/Additive/Energy.lean        |  5 +----
 Mathlib/Combinatorics/Configuration.lean          |  3 ---
 Mathlib/Combinatorics/Derangements/Basic.lean     |  3 +--
 Mathlib/Combinatorics/Enumerative/Catalan.lean    | 15 +--------------
 .../Combinatorics/Enumerative/Composition.lean    |  6 ------
 Mathlib/Combinatorics/HalesJewett.lean            |  1 -
 Mathlib/Combinatorics/Hindman.lean                |  3 ---
 Mathlib/Combinatorics/Quiver/Covering.lean        |  7 ++-----
 Mathlib/Combinatorics/Quiver/Prefunctor.lean      |  1 -
 Mathlib/Combinatorics/Quiver/Subquiver.lean       |  4 ++--
 Mathlib/Combinatorics/Quiver/Symmetric.lean       |  2 +-
 .../Combinatorics/SetFamily/Compression/Down.lean |  2 +-
 Mathlib/Combinatorics/SetFamily/LYM.lean          |  2 --
 Mathlib/Combinatorics/SetFamily/Shadow.lean       |  4 +---
 Mathlib/Combinatorics/SimpleGraph/Basic.lean      |  6 ------
 Mathlib/Combinatorics/SimpleGraph/Coloring.lean   |  2 --
 Mathlib/Combinatorics/SimpleGraph/Dart.lean       |  3 ---
 Mathlib/Combinatorics/SimpleGraph/Density.lean    |  3 +--
 Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean  |  2 +-
 Mathlib/Combinatorics/SimpleGraph/Finite.lean     |  5 -----
 Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean  |  8 ++------
 Mathlib/Combinatorics/SimpleGraph/Path.lean       |  4 +---
 Mathlib/Combinatorics/SimpleGraph/Prod.lean       |  2 --
 .../SimpleGraph/Regularity/Bound.lean             |  8 +++-----
 .../SimpleGraph/Regularity/Equitabilise.lean      |  5 +----
 .../SimpleGraph/StronglyRegular.lean              |  5 +----
 Mathlib/Combinatorics/SimpleGraph/Walk.lean       |  6 +-----
 Mathlib/Combinatorics/Young/YoungDiagram.lean     |  5 +----
 28 files changed, 22 insertions(+), 100 deletions(-)

diff --git a/Mathlib/Combinatorics/Additive/Energy.lean b/Mathlib/Combinatorics/Additive/Energy.lean
index e1f1d36d3e389..8e9f4b0c90c20 100644
--- a/Mathlib/Combinatorics/Additive/Energy.lean
+++ b/Mathlib/Combinatorics/Additive/Energy.lean
@@ -84,10 +84,7 @@ lemma mulEnergy_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : Eₘ[s₁, t₁
 @[to_additive] lemma le_mulEnergy : s.card * t.card ≤ Eₘ[s, t] := by
   rw [← card_product]
   refine
-    card_le_card_of_injOn (@fun x => ((x.1, x.1), x.2, x.2)) (by
-    -- Porting note: changed this from a `simp` proof without `only` because of a timeout
-      simp only [← and_imp, mem_product, Prod.forall, mem_filter, and_self, and_true, imp_self,
-        implies_true]) fun a _ b _ => ?_
+    card_le_card_of_injOn (@fun x => ((x.1, x.1), x.2, x.2)) (by simp) fun a _ b _ => ?_
   simp only [Prod.mk.inj_iff, and_self_iff, and_imp]
   exact Prod.ext
 
diff --git a/Mathlib/Combinatorics/Configuration.lean b/Mathlib/Combinatorics/Configuration.lean
index 91afb4626b98f..92e86eaa7e632 100644
--- a/Mathlib/Combinatorics/Configuration.lean
+++ b/Mathlib/Combinatorics/Configuration.lean
@@ -42,18 +42,15 @@ variable (P L : Type*) [Membership P L]
 def Dual :=
   P
 
--- Porting note: was `this` instead of `h`
 instance [h : Inhabited P] : Inhabited (Dual P) :=
   h
 
 instance [Finite P] : Finite (Dual P) :=
   ‹Finite P›
 
--- Porting note: was `this` instead of `h`
 instance [h : Fintype P] : Fintype (Dual P) :=
   h
 
--- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: figure out if this is needed.
 set_option synthInstance.checkSynthOrder false in
 instance : Membership (Dual L) (Dual P) :=
   ⟨Function.swap (Membership.mem : L → P → Prop)⟩
diff --git a/Mathlib/Combinatorics/Derangements/Basic.lean b/Mathlib/Combinatorics/Derangements/Basic.lean
index ac4e2f3b84276..de6307552ceae 100644
--- a/Mathlib/Combinatorics/Derangements/Basic.lean
+++ b/Mathlib/Combinatorics/Derangements/Basic.lean
@@ -96,9 +96,8 @@ def atMostOneFixedPointEquivSum_derangements [DecidableEq α] (a : α) :
       · rw [Set.eq_empty_iff_forall_not_mem]
         exact ⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩
     _ ≃ derangements ({a}ᶜ : Set α) ⊕ derangements α := by
-      -- Porting note: was `subtypeEquiv _` but now needs the placeholder to be provided explicitly
       refine
-        Equiv.sumCongr ((derangements.subtypeEquiv (· ∈ ({a}ᶜ : Set α))).trans <|
+        Equiv.sumCongr ((derangements.subtypeEquiv _).trans <|
             subtypeEquivRight fun x => ?_).symm
           (subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)
       rw [eq_comm, Set.ext_iff]
diff --git a/Mathlib/Combinatorics/Enumerative/Catalan.lean b/Mathlib/Combinatorics/Enumerative/Catalan.lean
index b69b6c29f6a33..0ba1191b7ca95 100644
--- a/Mathlib/Combinatorics/Enumerative/Catalan.lean
+++ b/Mathlib/Combinatorics/Enumerative/Catalan.lean
@@ -150,11 +150,7 @@ def treesOfNumNodesEq : ℕ → Finset (Tree Unit)
   | 0 => {nil}
   | n + 1 =>
     (antidiagonal n).attach.biUnion fun ijh =>
-      -- Porting note: `unusedHavesSuffices` linter is not happy with this. Commented out.
-      -- have := Nat.lt_succ_of_le (fst_le ijh.2)
-      -- have := Nat.lt_succ_of_le (snd_le ijh.2)
       pairwiseNode (treesOfNumNodesEq ijh.1.1) (treesOfNumNodesEq ijh.1.2)
-  -- Porting note: Add this to satisfy the linter.
   decreasing_by
     · simp_wf; have := fst_le ijh.2; omega
     · simp_wf; have := snd_le ijh.2; omega
@@ -192,15 +188,6 @@ theorem treesOfNumNodesEq_card_eq_catalan (n : ℕ) : #(treesOfNumNodesEq n) = c
     rintro ⟨i, j⟩ H
     rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]
   · simp_rw [disjoint_left]
-    rintro ⟨i, j⟩ _ ⟨i', j'⟩ _
-    -- Porting note: was clear * -; tidy
-    intros h a
-    cases' a with a l r
-    · intro h; simp at h
-    · intro h1 h2
-      apply h
-      trans (numNodes l, numNodes r)
-      · simp at h1; simp [h1]
-      · simp at h2; simp [h2]
+    aesop
 
 end Tree
diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean
index e1bf3970d658a..b7b6c98651639 100644
--- a/Mathlib/Combinatorics/Enumerative/Composition.lean
+++ b/Mathlib/Combinatorics/Enumerative/Composition.lean
@@ -574,9 +574,6 @@ This makes sense mostly when `n = l.length`, but this is not necessary for the d
 def splitWrtComposition (l : List α) (c : Composition n) : List (List α) :=
   splitWrtCompositionAux l c.blocks
 
--- Porting note: can't refer to subeqn in Lean 4 this way, and seems to definitionally simp
---attribute [local simp] splitWrtCompositionAux.equations._eqn_1
-
 @[local simp]
 theorem splitWrtCompositionAux_cons (l : List α) (n ns) :
     l.splitWrtCompositionAux (n::ns) = take n l::(drop n l).splitWrtCompositionAux ns := by
@@ -645,7 +642,6 @@ theorem getElem_splitWrtComposition' (l : List α) (c : Composition n) {i : ℕ}
     (l.splitWrtComposition c)[i] = (l.take (c.sizeUpTo (i + 1))).drop (c.sizeUpTo i) :=
   getElem_splitWrtCompositionAux _ _ hi
 
--- Porting note: restatement of `get_splitWrtComposition`
 theorem getElem_splitWrtComposition (l : List α) (c : Composition n)
     (i : Nat) (h : i < (l.splitWrtComposition c).length) :
     (l.splitWrtComposition c)[i] = (l.take (c.sizeUpTo (i + 1))).drop (c.sizeUpTo i) :=
@@ -666,7 +662,6 @@ theorem get_splitWrtComposition' (l : List α) (c : Composition n) {i : ℕ}
     (l.splitWrtComposition c).get ⟨i, hi⟩ = (l.take (c.sizeUpTo (i + 1))).drop (c.sizeUpTo i) := by
   simp [getElem_splitWrtComposition']
 
--- Porting note: restatement of `get_splitWrtComposition`
 @[deprecated getElem_splitWrtComposition (since := "2024-06-12")]
 theorem get_splitWrtComposition (l : List α) (c : Composition n)
     (i : Fin (l.splitWrtComposition c).length) :
@@ -922,7 +917,6 @@ theorem Composition.toCompositionAsSet_blocks (c : Composition n) :
     eq_of_sum_take_eq length_eq H
   intro i hi
   have i_lt : i < d.boundaries.card := by
-    -- Porting note: relied on `convert` unfolding definitions, switched to using a `simpa`
     simpa [CompositionAsSet.blocks, length_ofFn,
       d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
   have i_lt' : i < c.boundaries.card := i_lt
diff --git a/Mathlib/Combinatorics/HalesJewett.lean b/Mathlib/Combinatorics/HalesJewett.lean
index 082fd89e47b72..bc53c5115dbe1 100644
--- a/Mathlib/Combinatorics/HalesJewett.lean
+++ b/Mathlib/Combinatorics/HalesJewett.lean
@@ -420,7 +420,6 @@ private theorem exists_mono_in_high_dimension' :
     -- and adding to this the vertical line obtained by the focus point and `l`.
     refine Or.inl ⟨⟨(s.lines.map ?_).cons ⟨(l'.map some).vertical s.focus, C' s.focus, fun x => ?_⟩,
             Sum.elim s.focus (l'.map some none), ?_, ?_⟩, ?_⟩
-    -- Porting note: Needed to reorder the following two goals
     -- The product lines are almost monochromatic.
     · refine fun p => ⟨p.line.prod (l'.map some), p.color, fun x => ?_⟩
       rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]
diff --git a/Mathlib/Combinatorics/Hindman.lean b/Mathlib/Combinatorics/Hindman.lean
index 59d2bb754770f..312ae28fa0af6 100644
--- a/Mathlib/Combinatorics/Hindman.lean
+++ b/Mathlib/Combinatorics/Hindman.lean
@@ -79,9 +79,6 @@ theorem Ultrafilter.continuous_mul_left {M} [Semigroup M] (V : Ultrafilter M) :
 
 namespace Hindman
 
--- Porting note: mathport wants these names to be `fS`, `fP`, etc, but this does violence to
--- mathematical naming conventions, as does `fs`, `fp`, so we just followed `mathlib` 3 here
-
 /-- `FS a` is the set of finite sums in `a`, i.e. `m ∈ FS a` if `m` is the sum of a nonempty
 subsequence of `a`. We give a direct inductive definition instead of talking about subsequences. -/
 inductive FS {M} [AddSemigroup M] : Stream' M → Set M
diff --git a/Mathlib/Combinatorics/Quiver/Covering.lean b/Mathlib/Combinatorics/Quiver/Covering.lean
index 0e30025d9de92..ba60602599454 100644
--- a/Mathlib/Combinatorics/Quiver/Covering.lean
+++ b/Mathlib/Combinatorics/Quiver/Covering.lean
@@ -190,11 +190,8 @@ theorem Prefunctor.pathStar_injective (hφ : ∀ u, Injective (φ.star u)) (u :
     rintro ⟨y₂, p₂⟩ <;>
     cases' p₂ with x₂ _ p₂ e₂ <;>
     intro h <;>
-    -- Porting note: added `Sigma.mk.inj_iff`
-    simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons,
-      Sigma.mk.inj_iff] at h
-  · -- Porting note: goal not present in lean3.
-    rfl
+    simp at h
+  · rfl
   · exfalso
     cases' h with h h'
     rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'
diff --git a/Mathlib/Combinatorics/Quiver/Prefunctor.lean b/Mathlib/Combinatorics/Quiver/Prefunctor.lean
index 2a0468c73b08f..fc0496ac6f85e 100644
--- a/Mathlib/Combinatorics/Quiver/Prefunctor.lean
+++ b/Mathlib/Combinatorics/Quiver/Prefunctor.lean
@@ -22,7 +22,6 @@ structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{
 
 namespace Prefunctor
 
--- Porting note: added during port.
 -- These lemmas can not be `@[simp]` because after `whnfR` they have a variable on the LHS.
 -- Nevertheless they are sometimes useful when building functors.
 lemma mk_obj {V W : Type*} [Quiver V] [Quiver W] {obj : V → W} {map} {X : V} :
diff --git a/Mathlib/Combinatorics/Quiver/Subquiver.lean b/Mathlib/Combinatorics/Quiver/Subquiver.lean
index 6cf35fb02f3e5..365c0628c73d1 100644
--- a/Mathlib/Combinatorics/Quiver/Subquiver.lean
+++ b/Mathlib/Combinatorics/Quiver/Subquiver.lean
@@ -25,7 +25,7 @@ def WideSubquiver (V) [Quiver.{v + 1} V] :=
 
 /-- A type synonym for `V`, when thought of as a quiver having only the arrows from
 some `WideSubquiver`. -/
--- Porting note: no hasNonemptyInstance linter yet
+-- Porting note: no hasNonemptyInstance linter yet https://github.com/leanprover-community/mathlib4/issues/5171
 @[nolint unusedArguments]
 def WideSubquiver.toType (V) [Quiver V] (_ : WideSubquiver V) : Type u :=
   V
@@ -50,7 +50,7 @@ noncomputable instance {V} [Quiver V] : Inhabited (WideSubquiver V) :=
 
 -- TODO Unify with `CategoryTheory.Arrow`? (The fields have been named to match.)
 /-- `Total V` is the type of _all_ arrows of `V`. -/
--- Porting note: no hasNonemptyInstance linter yet
+-- Porting note: no hasNonemptyInstance linter yet https://github.com/leanprover-community/mathlib4/issues/5171
 @[ext]
 structure Total (V : Type u) [Quiver.{v} V] : Sort max (u + 1) v where
   /-- the source vertex of an arrow -/
diff --git a/Mathlib/Combinatorics/Quiver/Symmetric.lean b/Mathlib/Combinatorics/Quiver/Symmetric.lean
index bb83a91439731..39e75756c695f 100644
--- a/Mathlib/Combinatorics/Quiver/Symmetric.lean
+++ b/Mathlib/Combinatorics/Quiver/Symmetric.lean
@@ -26,7 +26,7 @@ namespace Quiver
 
 /-- A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow).
     NB: this does not work for `Prop`-valued quivers. It requires `[Quiver.{v+1} V]`. -/
--- Porting note: no hasNonemptyInstance linter yet
+-- Porting note: no hasNonemptyInstance linter yet https://github.com/leanprover-community/mathlib4/issues/5171
 def Symmetrify (V : Type*) := V
 
 instance symmetrifyQuiver (V : Type u) [Quiver V] : Quiver (Symmetrify V) :=
diff --git a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
index c0a526d8fdd86..5b55945f6fd4f 100644
--- a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
+++ b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
@@ -212,7 +212,7 @@ def compression (a : α) (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
 
 @[inherit_doc]
 scoped[FinsetFamily] notation "𝓓 " => Down.compression
--- Porting note: had to open this
+
 open FinsetFamily
 
 /-- `a` is in the down-compressed family iff it's in the original and its compression is in the
diff --git a/Mathlib/Combinatorics/SetFamily/LYM.lean b/Mathlib/Combinatorics/SetFamily/LYM.lean
index 24ec53fa6da54..82b28f2f04888 100644
--- a/Mathlib/Combinatorics/SetFamily/LYM.lean
+++ b/Mathlib/Combinatorics/SetFamily/LYM.lean
@@ -71,8 +71,6 @@ theorem card_mul_le_card_shadow_mul (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
   refine le_trans ?_ tsub_tsub_le_tsub_add
   rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]
   refine card_le_card fun t ht => ?_
-  -- Porting note: commented out the following line
-  -- infer_instance
   rw [mem_bipartiteAbove] at ht
   have : ∅ ∉ 𝒜 := by
     rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
diff --git a/Mathlib/Combinatorics/SetFamily/Shadow.lean b/Mathlib/Combinatorics/SetFamily/Shadow.lean
index 98557ae4406a6..ceaa40eb5da72 100644
--- a/Mathlib/Combinatorics/SetFamily/Shadow.lean
+++ b/Mathlib/Combinatorics/SetFamily/Shadow.lean
@@ -58,9 +58,8 @@ elements from any set in `𝒜`. -/
 def shadow (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
   𝒜.sup fun s => s.image (erase s)
 
--- Porting note: added `inherit_doc` to calm linter
 @[inherit_doc] scoped[FinsetFamily] notation:max "∂ " => Finset.shadow
--- Porting note: had to open FinsetFamily
+
 open FinsetFamily
 
 /-- The shadow of the empty set is empty. -/
@@ -183,7 +182,6 @@ variable [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {s t : Finset
 def upShadow (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
   𝒜.sup fun s => sᶜ.image fun a => insert a s
 
--- Porting note: added `inherit_doc` to calm linter
 @[inherit_doc] scoped[FinsetFamily] notation:max "∂⁺ " => Finset.upShadow
 
 /-- The upper shadow of the empty set is empty. -/
diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
index 0c0f567f36892..6b07045236942 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -37,13 +37,9 @@ This module defines simple graphs on a vertex type `V` as an irreflexive symmetr
   look like.
 -/
 
--- Porting note: using `aesop` for automation
-
--- Porting note: These attributes are needed to use `aesop` as a replacement for `obviously`
 attribute [aesop norm unfold (rule_sets := [SimpleGraph])] Symmetric
 attribute [aesop norm unfold (rule_sets := [SimpleGraph])] Irreflexive
 
--- Porting note: a thin wrapper around `aesop` for graph lemmas, modelled on `aesop_cat`
 /--
 A variant of the `aesop` tactic for use in the graph library. Changes relative
 to standard `aesop`:
@@ -93,7 +89,6 @@ structure SimpleGraph (V : Type u) where
   Adj : V → V → Prop
   symm : Symmetric Adj := by aesop_graph
   loopless : Irreflexive Adj := by aesop_graph
--- Porting note: changed `obviously` to `aesop` in the `structure`
 
 initialize_simps_projections SimpleGraph (Adj → adj)
 
@@ -139,7 +134,6 @@ theorem SimpleGraph.fromRel_adj {V : Type u} (r : V → V → Prop) (v w : V) :
     (SimpleGraph.fromRel r).Adj v w ↔ v ≠ w ∧ (r v w ∨ r w v) :=
   Iff.rfl
 
--- Porting note: attributes needed for `completeGraph`
 attribute [aesop safe (rule_sets := [SimpleGraph])] Ne.symm
 attribute [aesop safe (rule_sets := [SimpleGraph])] Ne.irrefl
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
index ad526f0fa08e0..54483becc0906 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
@@ -105,8 +105,6 @@ theorem Coloring.colorClasses_finite [Finite α] : C.colorClasses.Finite :=
 theorem Coloring.card_colorClasses_le [Fintype α] [Fintype C.colorClasses] :
     Fintype.card C.colorClasses ≤ Fintype.card α := by
   simp only [colorClasses]
-  -- Porting note: brute force instance declaration `[Fintype (Setoid.classes (Setoid.ker C))]`
-  haveI : Fintype (Setoid.classes (Setoid.ker C)) := by assumption
   convert Setoid.card_classes_ker_le C
 
 theorem Coloring.not_adj_of_mem_colorClass {c : α} {v w : V} (hv : v ∈ C.colorClass c)
diff --git a/Mathlib/Combinatorics/SimpleGraph/Dart.lean b/Mathlib/Combinatorics/SimpleGraph/Dart.lean
index 57d70b692b762..c36fe1186e465 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Dart.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Dart.lean
@@ -37,9 +37,6 @@ theorem Dart.ext_iff (d₁ d₂ : G.Dart) : d₁ = d₂ ↔ d₁.toProd = d₂.t
 theorem Dart.ext (d₁ d₂ : G.Dart) (h : d₁.toProd = d₂.toProd) : d₁ = d₂ :=
   (Dart.ext_iff d₁ d₂).mpr h
 
--- Porting note: deleted `Dart.fst` and `Dart.snd` since they are now invalid declaration names,
--- even though there is not actually a `SimpleGraph.Dart.fst` or `SimpleGraph.Dart.snd`.
-
 @[simp]
 theorem Dart.fst_ne_snd (d : G.Dart) : d.fst ≠ d.snd :=
   fun h ↦ G.irrefl (h ▸ d.adj)
diff --git a/Mathlib/Combinatorics/SimpleGraph/Density.lean b/Mathlib/Combinatorics/SimpleGraph/Density.lean
index 487d1b1620a3e..27c6603abcc93 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Density.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Density.lean
@@ -338,8 +338,7 @@ theorem edgeDensity_add_edgeDensity_compl (hs : s.Nonempty) (ht : t.Nonempty) (h
     G.edgeDensity s t + Gᶜ.edgeDensity s t = 1 := by
   rw [edgeDensity_def, edgeDensity_def, div_add_div_same, div_eq_one_iff_eq]
   · exact mod_cast card_interedges_add_card_interedges_compl _ h
-  -- Porting note: Wrote a workaround for `positivity` tactic.
-  · apply mul_ne_zero <;> exact mod_cast Nat.pos_iff_ne_zero.1 (Nonempty.card_pos ‹_›)
+  · positivity
 
 end DecidableEq
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean b/Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
index 1f6be300ede03..3502f86120c33 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
@@ -84,7 +84,7 @@ protected def lift {β : Sort*} (f : ∀ ⦃v⦄ (_ : v ∉ K), β)
     · rintro h'
       exact (h u.prop v.prop a).trans (ih h'.of_cons)
 
-@[elab_as_elim] -- Porting note: added
+@[elab_as_elim]
 protected theorem ind {β : G.ComponentCompl K → Prop}
     (f : ∀ ⦃v⦄ (hv : v ∉ K), β (G.componentComplMk hv)) : ∀ C : G.ComponentCompl K, β C := by
   apply ConnectedComponent.ind
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index cd15c4a2cff97..6bfa2d702da52 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -136,7 +136,6 @@ theorem edgeFinset_deleteEdges [DecidableEq V] [Fintype G.edgeSet] (s : Finset (
 
 section DeleteFar
 
--- Porting note: added `Fintype (Sym2 V)` argument.
 variable {𝕜 : Type*} [OrderedRing 𝕜]
   [Fintype G.edgeSet] {p : SimpleGraph V → Prop} {r r₁ r₂ : 𝕜}
 
@@ -205,10 +204,6 @@ theorem singleton_disjoint_neighborFinset : Disjoint {v} (G.neighborFinset v) :=
 /-- `G.degree v` is the number of vertices adjacent to `v`. -/
 def degree : ℕ := #(G.neighborFinset v)
 
--- Porting note: in Lean 3 we could do `simp [← degree]`, but that gives
--- "invalid '←' modifier, 'SimpleGraph.degree' is a declaration name to be unfolded".
--- In any case, having this lemma is good since there's no guarantee we won't still change
--- the definition of `degree`.
 @[simp]
 theorem card_neighborFinset_eq_degree : #(G.neighborFinset v) = G.degree v := rfl
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
index 56b39afefb146..13f35d5e5fc37 100644
--- a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
@@ -94,12 +94,8 @@ theorem incMatrix_apply_eq_zero_iff : G.incMatrix R a e = 0 ↔ e ∉ G.incidenc
   simp only [incMatrix_apply, Set.indicator_apply_eq_zero, Pi.one_apply, one_ne_zero]
 
 theorem incMatrix_apply_eq_one_iff : G.incMatrix R a e = 1 ↔ e ∈ G.incidenceSet a := by
-  -- Porting note: was `convert one_ne_zero.ite_eq_left_iff; infer_instance`
-  unfold incMatrix Set.indicator
-  simp only [Pi.one_apply]
-  apply Iff.intro <;> intro h
-  · split at h <;> simp_all only [zero_ne_one]
-  · simp_all only [ite_true]
+  convert one_ne_zero.ite_eq_left_iff
+  infer_instance
 
 end MulZeroOneClass
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Path.lean b/Mathlib/Combinatorics/SimpleGraph/Path.lean
index 6487fc983ad0a..3211d0a9774fe 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Path.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Path.lean
@@ -83,7 +83,7 @@ structure IsPath {u v : V} (p : G.Walk u v) extends IsTrail p : Prop where
   support_nodup : p.support.Nodup
 
 -- Porting note: used to use `extends to_trail : is_trail p` in structure
-protected lemma IsPath.isTrail {p : Walk G u v}(h : IsPath p) : IsTrail p := h.toIsTrail
+protected lemma IsPath.isTrail {p : Walk G u v} (h : IsPath p) : IsTrail p := h.toIsTrail
 
 /-- A *circuit* at `u : V` is a nonempty trail beginning and ending at `u`. -/
 @[mk_iff isCircuit_def]
@@ -376,7 +376,6 @@ protected theorem IsPath.takeUntil {u v w : V} {p : G.Walk v w} (hc : p.IsPath)
     (h : u ∈ p.support) : (p.takeUntil u h).IsPath :=
   IsPath.of_append_left (q := p.dropUntil u h) (by rwa [← take_spec _ h] at hc)
 
--- Porting note: p was previously accidentally an explicit argument
 protected theorem IsPath.dropUntil {u v w : V} {p : G.Walk v w} (hc : p.IsPath)
     (h : u ∈ p.support) : (p.dropUntil u h).IsPath :=
   IsPath.of_append_right (p := p.takeUntil u h) (q := p.dropUntil u h)
@@ -1203,7 +1202,6 @@ theorem reachable_deleteEdges_iff_exists_cycle.aux [DecidableEq V] {u v w : V}
     ← List.append_assoc, ← Walk.edges_append] at hc
   exact List.disjoint_of_nodup_append hc hbq hpq'
 
--- Porting note: the unused variable checker helped eliminate a good amount of this proof (!)
 theorem adj_and_reachable_delete_edges_iff_exists_cycle {v w : V} :
     G.Adj v w ∧ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔
       ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges := by
diff --git a/Mathlib/Combinatorics/SimpleGraph/Prod.lean b/Mathlib/Combinatorics/SimpleGraph/Prod.lean
index e094ff9729ec2..ee5c57ef5e760 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Prod.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Prod.lean
@@ -30,8 +30,6 @@ variable {α β γ : Type*}
 
 namespace SimpleGraph
 
--- Porting note: pruned variables to keep things out of local contexts, which
--- can impact how generalization works, or what aesop does.
 variable {G : SimpleGraph α} {H : SimpleGraph β}
 
 /-- Box product of simple graphs. It relates `(a₁, b)` and `(a₂, b)` if `G` relates `a₁` and `a₂`,
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
index 038a7f498f743..6e1c8c2dbb00b 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
@@ -74,8 +74,6 @@ private theorem m_pos [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α
 
 /-- Local extension for the `positivity` tactic: A few facts that are needed many times for the
 proof of Szemerédi's regularity lemma. -/
--- Porting note: positivity extensions must now be global, and this did not seem like a good
--- match for positivity anymore, so I wrote a new tactic (kmill)
 scoped macro "sz_positivity" : tactic =>
   `(tactic|
       { try have := m_pos ‹_›
@@ -220,9 +218,9 @@ theorem add_div_le_sum_sq_div_card (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜)
   have h₃ := mul_sq_le_sum_sq hst (fun i => (f i - (∑ j ∈ t, f j) / #t)) h₂ hscard.ne'
   apply (add_le_add_left h₃ _).trans
   -- Porting note: was
-  -- `simp [← mul_div_right_comm _ (#t : 𝕜), sub_div' _ _ _ htcard.ne', ← sum_div, ← add_div,`
-  -- `  mul_pow, div_le_iff₀ (sq_pos_of_ne_zero htcard.ne'), sub_sq, sum_add_distrib, ← sum_mul,`
-  -- `  ← mul_sum]`
+  -- simp [← mul_div_right_comm _ (#t : 𝕜), sub_div' _ _ _ htcard.ne', ← sum_div, ← add_div,
+  --   mul_pow, div_le_iff₀ (sq_pos_of_ne_zero htcard.ne'), sub_sq, sum_add_distrib, ← sum_mul,
+  --   ← mul_sum]
   simp_rw [sub_div' _ _ _ htcard.ne']
   conv_lhs => enter [2, 2, x]; rw [div_pow]
   rw [div_pow, ← sum_div, ← mul_div_right_comm _ (#t : 𝕜), ← add_div,
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
index bad7217bbede8..899a2fefad2f7 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
@@ -119,10 +119,7 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = #s) :
       refine
         (card_le_card fun i => ?_).trans
           (hR₂ (u \ t) <| P.mem_avoid.2 ⟨u, hu₁, fun i => hut <| i.antisymm htu, rfl⟩)
-      -- Porting note: `not_and` required because `∃ x ∈ s, p x` is defined differently
-      simp only [not_exists, not_and, mem_biUnion, and_imp, mem_union, mem_filter, mem_sdiff,
-        id, not_or]
-      exact fun hi₁ hi₂ hi₃ =>
+      simpa using fun hi₁ hi₂ hi₃ =>
         ⟨⟨hi₁, hi₂⟩, fun x hx hx' => hi₃ _ hx <| hx'.trans sdiff_subset⟩
     · apply sdiff_subset_sdiff Subset.rfl (biUnion_subset_biUnion_of_subset_left _ _)
       exact filter_subset_filter _ (subset_insert _ _)
diff --git a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
index 191e072fd1e6e..40d4f961b4861 100644
--- a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
@@ -80,10 +80,7 @@ theorem IsSRGWith.card_neighborFinset_union_eq {v w : V} (h : G.IsSRGWith n k 
       2 * k - Fintype.card (G.commonNeighbors v w) := by
   apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))
   rw [Nat.sub_add_cancel, ← Set.toFinset_card]
-  -- Porting note: Set.toFinset_inter needs workaround to use unification to solve for one of the
-  -- instance arguments:
-  · simp [commonNeighbors, @Set.toFinset_inter _ _ _ _ _ _ (_),
-      ← neighborFinset_def, Finset.card_union_add_card_inter, card_neighborFinset_eq_degree,
+  · simp [commonNeighbors, ← neighborFinset_def, Finset.card_union_add_card_inter,
       h.regular.degree_eq, two_mul]
   · apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
     simp [h.regular.degree_eq, two_mul]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk.lean b/Mathlib/Combinatorics/SimpleGraph/Walk.lean
index 935f0c84e508f..06aaabee0f997 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Walk.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Walk.lean
@@ -596,8 +596,7 @@ theorem chain_dartAdj_darts {d : G.Dart} {v w : V} (h : d.snd = v) (p : G.Walk v
     List.Chain G.DartAdj d p.darts := by
   induction p generalizing d with
   | nil => exact List.Chain.nil
-  -- Porting note: needed to defer `h` and `rfl` to help elaboration
-  | cons h' p ih => exact List.Chain.cons (by exact h) (ih (by rfl))
+  | cons h' p ih => exact List.Chain.cons h (ih rfl)
 
 theorem chain'_dartAdj_darts {u v : V} : ∀ (p : G.Walk u v), List.Chain' G.DartAdj p.darts
   | nil => trivial
@@ -1304,9 +1303,6 @@ theorem support_transfer (hp) : (p.transfer H hp).support = p.support := by
 theorem length_transfer (hp) : (p.transfer H hp).length = p.length := by
   induction p <;> simp [*]
 
--- Porting note: this failed the simpNF linter since it was originally of the form
--- `(p.transfer H hp).transfer K hp' = p.transfer K hp''` with `hp'` a function of `hp` and `hp'`.
--- This was a mistake and it's corrected here.
 @[simp]
 theorem transfer_transfer (hp) {K : SimpleGraph V} (hp') :
     (p.transfer H hp).transfer K hp' = p.transfer K (p.edges_transfer hp ▸ hp') := by
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index b4ca1dc27ecfb..7fcf8eff369ae 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -400,10 +400,7 @@ protected theorem mem_cellsOfRowLens {w : List ℕ} {c : ℕ × ℕ} :
     c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ h : c.fst < w.length, c.snd < w[c.fst] := by
   induction' w with w_hd w_tl w_ih generalizing c <;> rw [YoungDiagram.cellsOfRowLens]
   · simp [YoungDiagram.cellsOfRowLens]
-  · rcases c with ⟨⟨_, _⟩, _⟩
-    · simp
-    -- Porting note: was `simpa`
-    · simp [w_ih, -Finset.singleton_product, Nat.succ_lt_succ_iff]
+  · rcases c with ⟨⟨_, _⟩, _⟩ <;> simp_all
 
 /-- Young diagram from a sorted list -/
 def ofRowLens (w : List ℕ) (hw : w.Sorted (· ≥ ·)) : YoungDiagram where