fix: remove last sorry

Author: Vtec234

HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean

@@ -56,24 +56,12 @@ section
 variable {B : Type u₁} [Bicategory B]
 variable (F : Pseudofunctor B Cat) {a b : B}
 
-
 @[simp] lemma _root_.CategoryTheory.LocallyDiscrete.Iso.hom_inv {C : Type u₁} [Category C]
     (X Y : LocallyDiscrete C) (e : X ≅ Y) : e.hom.toLoc ≫ e.inv.toLoc = 𝟙 _ :=
   LocallyDiscrete.eq_of_hom ⟨⟨by simp⟩⟩
 
--- Autogenerated by adding @[to_app (attr := reassoc)] to `StrongTrans.naturality_comp_inv`
-def StrongTrans.naturality_comp_inv_app_assoc
-    {B : Type*} [Bicategory B]
-    {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
-    (X : ↑(F.obj a)) {Z : ↑(G.obj c)} (h : (F.map (f ≫ g) ≫ α.app c).obj X ⟶ Z) :
-    (α.naturality (f ≫ g)).inv.app X ≫ h =
-    (G.mapComp f g).hom.app ((α.app a).obj X) ≫
-    (α_ (α.app a) (G.map f) (G.map g)).inv.app X ≫
-    (G.map g).map ((α.naturality f).inv.app X) ≫
-    (α_ (F.map f) (α.app b) (G.map g)).hom.app X ≫
-    (α.naturality g).inv.app ((F.map f).obj X) ≫
-    (α_ (F.map f) (F.map g) (α.app c)).inv.app X ≫ (α.app c).map ((F.mapComp f g).inv.app X) ≫ h :=
-  sorry
+attribute [reassoc] StrongTrans.naturality_comp_inv_app
+
 end
 
 lemma _root_.CategoryTheory.Functor.toPseudofunctor'_map₂ {C : Type u₁} [Category.{v₁} C] (F : C ⥤ Cat)
@@ -1191,7 +1179,7 @@ include hom_id in
 lemma functorFromCompHom_id (c : C) : functorFromCompHom fib hom G (𝟙 c)
     = eqToHom (by simp [Cat.id_eq_id, Functor.id_comp]) := by
   ext x
-  simp [hom_id, eqToHom_map, functorFromCompHom]
+  simp [hom_id, functorFromCompHom]
 
 include hom_comp in
 lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃):
@@ -1200,7 +1188,7 @@ lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂
     Functor.whiskerLeft (F.map f) (functorFromCompHom fib hom G g) ≫
     eqToHom (by simp[Cat.comp_eq_comp, Functor.map_comp, Functor.assoc]) := by
   ext
-  simp [functorFromCompHom, hom_comp, eqToHom_map]
+  simp [functorFromCompHom, hom_comp]
 
 theorem functorFrom_comp : functorFrom fib hom hom_id hom_comp ⋙ G =
     functorFrom (functorFromCompFib fib G) (functorFromCompHom fib hom G)