-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₂, max ?u.411012 ?u.411013, u₂, max (?u.411012 + 1) (?u.411013 + 1)} D Cat
G_1 : Functor.{v₁, v₂, u₁, u₂} C_1 D
C : Type u₁
inst_2 : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst_3 : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X Y : C
f : X ⟶ Y
d : (↑(F.obj X) : Type u₂)
⊢ colimit.ι (ι F X ⋙ map α ⋙ H) d ≫
      (fiberwiseColimit (map α ⋙ H)).map f ≫
        Iso.hom
          ((fun (X : C) ↦
              (Iso.trans (Y := colimit ((α.app X).toFunctor ⋙ ι G X ⋙ H))
                  (HasColimit.isoOfNatIso
                      (((ι F X).associator (map α) H).symm ≪≫
                        isoWhiskerRight (ιCompMap α X) H ≪≫ (α.app X).toFunctor.associator (ι G X) H) :
                    colimit (ι F X ⋙ map α ⋙ H) ≅ colimit ((α.app X).toFunctor ⋙ ι G X ⋙ H))
                  (Final.colimitIso (α.app X).toFunctor (ι G X ⋙ H) :
                    colimit ((α.app X).toFunctor ⋙ ι G X ⋙ H) ≅ colimit (ι G X ⋙ H)) :
                (fiberwiseColimit (map α ⋙ H)).obj X ≅ (fiberwiseColimit H).obj X))
            Y) =
    CategoryStruct.comp (Y := colimit (ι F X ⋙ map α ⋙ H)) (colimit.ι (ι F X ⋙ map α ⋙ H) d)
      (Iso.hom
          ((fun (X : C) ↦
              (Iso.trans (Y := colimit ((α.app X).toFunctor ⋙ ι G X ⋙ H))
                  (HasColimit.isoOfNatIso
                      (((ι F X).associator (map α) H).symm ≪≫
                        isoWhiskerRight (ιCompMap α X) H ≪≫ (α.app X).toFunctor.associator (ι G X) H) :
                    colimit (ι F X ⋙ map α ⋙ H) ≅ colimit ((α.app X).toFunctor ⋙ ι G X ⋙ H))
                  (Final.colimitIso (α.app X).toFunctor (ι G X ⋙ H) :
                    colimit ((α.app X).toFunctor ⋙ ι G X ⋙ H) ≅ colimit (ι G X ⋙ H)) :
                (fiberwiseColimit (map α ⋙ H)).obj X ≅ (fiberwiseColimit H).obj X))
            X) ≫
        (fiberwiseColimit H).map f)
have simp : Eq (α := H.obj { base := X, fiber := (α.app X).toFunctor.obj d : Grothendieck G } ⟶ (fiberwiseColimit H).obj Y)
  (CategoryStruct.comp (Y := H.obj { base := Y, fiber := (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d) })
    (H.map { base := f, fiber := eqToHom sorry })
    (colimit.ι (ι G Y ⋙ H) ((α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d))))
  (CategoryStruct.comp (Y := H.obj { base := Y, fiber := (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d) })
    (H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X).toFunctor.obj d)) })
    (colimit.ι (ι G Y ⋙ H) ((G.map f).toFunctor.obj ((α.app X).toFunctor.obj d))))
Tactic: simp only [map, Cat.Hom.comp_toFunctor, comp_obj, ι_obj,
        fiberwiseColimit_map, ιNatTrans, ιCompMap, Iso.trans_hom, Category.assoc, ι_colimMap_assoc,
        NatTrans.comp_app, whiskerRight_app, Functor.comp_map, Cat.Hom₂.eqToHom_toNatTrans,
        eqToHom_app, map_id, Category.comp_id, associator_hom_app, colimit.ι_pre_assoc,
        HasColimit.isoOfNatIso_ι_hom_assoc, Iso.symm_hom, isoWhiskerRight_hom, associator_inv_app,
        NatIso.ofComponents_hom_app, Iso.refl_hom, Final.ι_colimitIso_hom, Category.id_comp,
        Final.ι_colimitIso_hom_assoc, colimit.ι_pre]