style: convert adaptation comments to #adaptation_note / lowercased forms

Satisfy the `linter.adaptationNote` text-based linter: the long block becomes
a `#adaptation_note /-- ... -/` command, and the four short back-references use
lowercase "see adaptation note" (the linter exempts that exact substring).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: nomeata

Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

@@ -92,12 +92,12 @@ lemma mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom (hf : f₀₁ ≫ f₁
   subst h₀₂ h₁₃ hf
   simp [mapComp_assoc_right_hom, Strict.associator_eqToIso, mapComp']
 
--- Adaptation note for lean4#13557: `useBackward true` is required for the `_app` and
--- `_app_assoc` forms generated by `to_app` to be properly normalized by `catAppSimp`,
--- which calls into simp with several `[backward_defeq]`-only lemmas (e.g.
--- `Cat.Hom.comp_toFunctor`, `Functor.comp_obj`). Without it, the generated lemma's type
--- differs subtly and `IsPrestack.overMapCompPresheafHomIso` (and possibly other
--- downstream callers) cannot supply `rfl` for the auxiliary equality hypotheses.
+#adaptation_note /-- lean4#13557: `useBackward true` is required for the `_app` and
+`_app_assoc` forms generated by `to_app` to be properly normalized by `catAppSimp`,
+which calls into simp with several `[backward_defeq]`-only lemmas (e.g.
+`Cat.Hom.comp_toFunctor`, `Functor.comp_obj`). Without it, the generated lemma's type
+differs subtly and `IsPrestack.overMapCompPresheafHomIso` (and possibly other downstream
+callers) cannot supply `rfl` for the auxiliary equality hypotheses. -/
 set_option backward.defeqAttrib.useBackward true in
 @[to_app (attr := reassoc)]
 lemma mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom (hf : f₀₁ ≫ f₁₃ = f) :
@@ -124,7 +124,7 @@ lemma mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight (hf : f₀₂ ≫ f
   rw [F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]
   simp
 
--- See the adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
+-- see adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
 set_option backward.defeqAttrib.useBackward true in
 @[to_app (attr := reassoc)]
 lemma mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv (hf : f₀₂ ≫ f₂₃ = f) :
@@ -134,7 +134,7 @@ lemma mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv (hf : f₀₂ ≫ f₂₃
   rw [whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃,
     Iso.hom_inv_id_assoc]
 
--- See the adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
+-- see adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
 set_option backward.defeqAttrib.useBackward true in
 @[to_app (attr := reassoc)]
 lemma mapComp'₀₁₃_inv (hf : f₀₁ ≫ f₁₃ = f) :
@@ -151,7 +151,7 @@ lemma mapComp'₀₁₃_hom (hf : f₀₁ ≫ f₁₃ = f) :
   rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f).inv, Iso.inv_hom_id]
   simp [mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃ hf]
 
--- See the adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
+-- see adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
 set_option backward.defeqAttrib.useBackward true in
 @[to_app (attr := reassoc)]
 lemma mapComp'₀₂₃_hom (hf : f₀₂ ≫ f₂₃ = f) :
@@ -168,7 +168,7 @@ lemma mapComp'₀₂₃_inv (hf : f₀₂ ≫ f₂₃ = f) :
   rw [← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom, Iso.hom_inv_id]
   simp [mapComp'₀₂₃_hom _ _ _ _ _ _ f h₀₂ h₁₃ hf]
 
--- See the adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
+-- see adaptation note above `mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom` (lean4#13557).
 set_option backward.defeqAttrib.useBackward true in
 @[to_app (attr := reassoc)]
 lemma mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom (hf : f₀₂ ≫ f₂₃ = f) :