fix(Translate): unfold hcongr and congr_simp aux theorems (#37948)

This PR removes the need to tag automatically generated `hcongr` and `congr_simp` lemmas in `to_dual`.

Author: JovanGerb

Mathlib/CategoryTheory/Functor/Category.lean

@@ -113,7 +113,7 @@ def hcomp {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : F ⋙ H ⟶ G ⋙ I wh
 
 -- Horizontal composition has two possible definitions that are dual to each other,
 -- and we need to prove to `to_dual` that these are equivalent.
-attribute [to_dual none] CategoryStruct.comp.hcongr_7 hcomp._proof_2 hcomp._proof_3
+attribute [to_dual none] hcomp._proof_2 hcomp._proof_3
 to_dual_insert_cast hcomp := by ext x; exact β.naturality' (α.app x)
 
 /-- Notation for horizontal composition of natural transformations. -/

Mathlib/CategoryTheory/Iso.lean

@@ -63,7 +63,6 @@ structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
 
 attribute [to_dual existing inv] Iso.hom
 attribute [to_dual self] Iso.mk Iso.casesOn
-attribute [to_dual none] Iso.mk.hcongr_8 -- needed in `Iso.ext`
 
 attribute [reassoc +to_dual (attr := simp), grind =] Iso.hom_inv_id Iso.inv_hom_id
 

Mathlib/CategoryTheory/Limits/Cones.lean

@@ -244,7 +244,7 @@ structure CoconeMorphism (A B : Cocone F) where
   w (j : J) : dsimp% A.ι.app j ≫ hom = B.ι.app j := by cat_disch
 
 attribute [reassoc (attr := simp)] ConeMorphism.w CoconeMorphism.w
-attribute [to_dual existing] ConeMorphism.mk.congr_simp ConeMorphism.casesOn
+attribute [to_dual existing] ConeMorphism.casesOn
 
 @[to_dual]
 instance inhabitedConeMorphism (A : Cone F) : Inhabited (ConeMorphism A A) :=

Mathlib/Tactic/Translate/Core.lean

@@ -680,13 +680,14 @@ def updateAndAddDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
         {ex.toMessageData}"
     throwError "@[{t.attrName}] failed. Nested error message:\n{ex.toMessageData}"
 
-/-- Unfold `simp` and `gcongr` auxlemmas in the type and value.
+/-- Unfold `simp`, `gcongr` and `hcongr`/`congr_simp` auxlemmas in the type and value.
 The reason why we can't just translate them is that they are generated by the `@[simp]` attribute,
 so it would require a change in the implementation of `@[simp]` to add these translations.
 Additionally, these lemmas have very short proofs, so unfolding them is not costly. -/
 def declUnfoldSimpAuxLemmas (decl : ConstantInfo) : MetaM ConstantInfo := do
   let unfold (e : Expr) := deltaExpand e (allowOpaque := true) fun
-    | .str _ s => "_simp_".isPrefixOf s || "_gcongr_".isPrefixOf s
+    | .str _ s => "_simp_".isPrefixOf s || "_gcongr_".isPrefixOf s ||
+        isHCongrReservedNameSuffix s || s == congrSimpSuffix
     | _ => false
   let mut decl := decl
   decl := decl.updateType <| ← unfold decl.type