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

@@ -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
 

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

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

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

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]