From 5741ea5a2ae733f3f2eb4844a84603cd840aa927 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 27 Feb 2024 07:41:15 +0000
Subject: [PATCH] chore: classify `was tidy` porting notes (#10937)

Classifies by adding issue number (#10936) to porting notes claiming anything semantically equivalent to:

- "used to be `tidy`"
- "was `tidy `"
---
 Archive/Imo/Imo1998Q2.lean                      |  4 ++--
 Mathlib/Algebra/Category/GroupCat/Limits.lean   |  2 +-
 Mathlib/CategoryTheory/Limits/KanExtension.lean |  2 +-
 Mathlib/CategoryTheory/Sigma/Basic.lean         |  2 +-
 Mathlib/LinearAlgebra/Prod.lean                 | 10 +++++-----
 5 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
index 722fd32cef405..7ee30ba7a5574 100644
--- a/Archive/Imo/Imo1998Q2.lean
+++ b/Archive/Imo/Imo1998Q2.lean
@@ -131,7 +131,7 @@ theorem A_fibre_over_contestant_card (c : C) :
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).card := by
   rw [A_fibre_over_contestant r]
   apply Finset.card_image_of_injOn
-  -- porting note: used to be `tidy`. TODO: remove `ext` after `extCore` to `aesop`.
+  -- Porting note (#10936): used to be `tidy`. TODO: remove `ext` after `extCore` to `aesop`.
   unfold Set.InjOn; intros; ext; all_goals aesop
 #align imo1998_q2.A_fibre_over_contestant_card Imo1998Q2.A_fibre_over_contestant_card
 
@@ -151,7 +151,7 @@ theorem A_fibre_over_judgePair_card {p : JudgePair J} (h : p.Distinct) :
       ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).card := by
   rw [A_fibre_over_judgePair r h]
   apply Finset.card_image_of_injOn
-  -- porting note: used to be `tidy`
+  -- Porting note (#10936): used to be `tidy`
   unfold Set.InjOn; intros; ext; all_goals aesop
 #align imo1998_q2.A_fibre_over_judge_pair_card Imo1998Q2.A_fibre_over_judgePair_card
 
diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean
index f3b10bbf61737..2ec6f74e1177c 100644
--- a/Mathlib/Algebra/Category/GroupCat/Limits.lean
+++ b/Mathlib/Algebra/Category/GroupCat/Limits.lean
@@ -413,7 +413,7 @@ def kernelIsoKer {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
         dsimp
         simp }
   inv := kernel.lift f (AddSubgroup.subtype f.ker) <| by
-    -- Porting note: used to be `tidy`, but `aesop` can't do it
+    -- Porting note (#10936): used to be `tidy`, but `aesop` can't do it
     refine DFunLike.ext _ _ ?_
     rintro ⟨x, (hx : f _ = 0)⟩
     exact hx
diff --git a/Mathlib/CategoryTheory/Limits/KanExtension.lean b/Mathlib/CategoryTheory/Limits/KanExtension.lean
index 4f574180e480c..74b8c749fd67c 100644
--- a/Mathlib/CategoryTheory/Limits/KanExtension.lean
+++ b/Mathlib/CategoryTheory/Limits/KanExtension.lean
@@ -161,7 +161,7 @@ end Ran
 @[simps!]
 def ran [∀ X, HasLimitsOfShape (StructuredArrow X ι) D] : (S ⥤ D) ⥤ L ⥤ D :=
   Adjunction.rightAdjointOfEquiv (fun F G => (Ran.equiv ι G F).symm) (by {
-    -- Porting note: was `tidy`
+    -- Porting note (#10936): was `tidy`
     intros X' X Y f g
     ext t
     apply limit.hom_ext
diff --git a/Mathlib/CategoryTheory/Sigma/Basic.lean b/Mathlib/CategoryTheory/Sigma/Basic.lean
index 9f5a17680b90f..509a59da10453 100644
--- a/Mathlib/CategoryTheory/Sigma/Basic.lean
+++ b/Mathlib/CategoryTheory/Sigma/Basic.lean
@@ -95,7 +95,7 @@ instance (i : I) : Full (incl i : C i ⥤ Σi, C i) where
   witness := fun ⟨_⟩ => rfl
 
 instance (i : I) : Faithful (incl i : C i ⥤ Σi, C i) where
-  -- Porting note: was `tidy`
+  -- Porting note (#10936): was `tidy`
   map_injective {_ _ _ _} h := by injection h
 
 section
diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean
index 2cfdfc5e1ae6d..df41d4a0346a6 100644
--- a/Mathlib/LinearAlgebra/Prod.lean
+++ b/Mathlib/LinearAlgebra/Prod.lean
@@ -632,14 +632,14 @@ def fstEquiv : Submodule.fst R M M₂ ≃ₗ[R] M where
 #align submodule.fst_equiv Submodule.fstEquiv
 
 theorem fst_map_fst : (Submodule.fst R M M₂).map (LinearMap.fst R M M₂) = ⊤ := by
-  -- Porting note: was `tidy`
+  -- Porting note (#10936): was `tidy`
   rw [eq_top_iff]; rintro x -
   simp only [fst, comap_bot, mem_map, mem_ker, snd_apply, fst_apply,
     Prod.exists, exists_eq_left, exists_eq]
 #align submodule.fst_map_fst Submodule.fst_map_fst
 
 theorem fst_map_snd : (Submodule.fst R M M₂).map (LinearMap.snd R M M₂) = ⊥ := by
-  -- Porting note: was `tidy`
+  -- Porting note (#10936): was `tidy`
   rw [eq_bot_iff]; intro x
   simp only [fst, comap_bot, mem_map, mem_ker, snd_apply, eq_comm, Prod.exists, exists_eq_left,
     exists_const, mem_bot, imp_self]
@@ -668,14 +668,14 @@ def sndEquiv : Submodule.snd R M M₂ ≃ₗ[R] M₂ where
 #align submodule.snd_equiv Submodule.sndEquiv
 
 theorem snd_map_fst : (Submodule.snd R M M₂).map (LinearMap.fst R M M₂) = ⊥ := by
-  -- Porting note: was `tidy`
+  -- Porting note (#10936): was `tidy`
   rw [eq_bot_iff]; intro x
   simp only [snd, comap_bot, mem_map, mem_ker, fst_apply, eq_comm, Prod.exists, exists_eq_left,
     exists_const, mem_bot, imp_self]
 #align submodule.snd_map_fst Submodule.snd_map_fst
 
 theorem snd_map_snd : (Submodule.snd R M M₂).map (LinearMap.snd R M M₂) = ⊤ := by
-  -- Porting note: was `tidy`
+  -- Porting note (#10936): was `tidy`
   rw [eq_top_iff]; rintro x -
   simp only [snd, comap_bot, mem_map, mem_ker, snd_apply, fst_apply,
     Prod.exists, exists_eq_right, exists_eq]
@@ -691,7 +691,7 @@ theorem fst_sup_snd : Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂ = ⊤ :=
 #align submodule.fst_sup_snd Submodule.fst_sup_snd
 
 theorem fst_inf_snd : Submodule.fst R M M₂ ⊓ Submodule.snd R M M₂ = ⊥ := by
-  -- Porting note: was `tidy`
+  -- Porting note (#10936): was `tidy`
   rw [eq_bot_iff]; rintro ⟨x, y⟩
   simp only [fst, comap_bot, snd, ge_iff_le, mem_inf, mem_ker, snd_apply, fst_apply, mem_bot,
     Prod.mk_eq_zero, and_comm, imp_self]