-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
b₀ b₁ b₂ b₃ : Cᵒᵖ
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
h : b₂ ⟶ b₃
⊢ Eq (α :=
    Quiver.Hom (V :=
      Quiver.Hom (V := Cat)
        ((fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₀)
        ((fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₃))
      ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
          (Functor.toCatHom (J.overMapPullback A f.unop) :
            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
        ((f ≫ g) ≫ h))
      ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
          (Functor.toCatHom (J.overMapPullback A f.unop) :
            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
        (f ≫ g ≫ h)))
    (CategoryStruct.comp (Y :=
        CategoryStruct.comp (Y :=
          (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₂)
          ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
              (Functor.toCatHom (J.overMapPullback A f.unop) :
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
            (f ≫ g))
          ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
              (Functor.toCatHom (J.overMapPullback A f.unop) :
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
            h))
        (Iso.hom
          ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
              (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
                Iso (C :=
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                  (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                  (Functor.toCatHom
                    (Functor.comp (D :=
                      (↑((fun (X : Cᵒᵖ) ↦
                              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                            b₁) :
                        Type (max (max (max u' u v) v') v)))
                      (Cat.Hom.toFunctor
                        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                            (Functor.toCatHom (J.overMapPullback A f.unop) :
                              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                          f))
                      (Cat.Hom.toFunctor
                        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                            (Functor.toCatHom (J.overMapPullback A f.unop) :
                              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                          g))))))
            (f ≫ g) h))
        (CategoryStruct.comp (Y :=
          CategoryStruct.comp (Y :=
            (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₂)
            (CategoryStruct.comp (Y :=
              (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₁)
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                f)
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                g))
            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                (Functor.toCatHom (J.overMapPullback A f.unop) :
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
              h))
          (Bicategory.whiskerRight
            (Iso.hom
              ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                  (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
                    Iso (C :=
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                      (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                      (Functor.toCatHom
                        (Functor.comp (D :=
                          (↑((fun (X : Cᵒᵖ) ↦
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                                b₁) :
                            Type (max (max (max u' u v) v') v)))
                          (Cat.Hom.toFunctor
                            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                (Functor.toCatHom (J.overMapPullback A f.unop) :
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                              f))
                          (Cat.Hom.toFunctor
                            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                (Functor.toCatHom (J.overMapPullback A f.unop) :
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                              g))))))
                f g))
            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                (Functor.toCatHom (J.overMapPullback A f.unop) :
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
              h))
          (Iso.hom
              (Bicategory.associator
                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                  f)
                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                  g)
                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                  h)) ≫
            CategoryStruct.comp (Y :=
              CategoryStruct.comp (Y :=
                (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₁)
                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                  f)
                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                  (g ≫ h)))
              (Bicategory.whiskerLeft
                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                  f)
                (Iso.inv
                  ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                      (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
                        Iso (C :=
                          Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                          (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                          (Functor.toCatHom
                            (Functor.comp (D :=
                              (↑((fun (X : Cᵒᵖ) ↦
                                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                                    b₁) :
                                Type (max (max (max u' u v) v') v)))
                              (Cat.Hom.toFunctor
                                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                        Cat.of
                                          (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                                  f))
                              (Cat.Hom.toFunctor
                                ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                    (Functor.toCatHom (J.overMapPullback A f.unop) :
                                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                        Cat.of
                                          (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                                  g))))))
                    g h)))
              (Iso.inv
                ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                    (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
                      Iso (C :=
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                          Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                        (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                        (Functor.toCatHom
                          (Functor.comp (D :=
                            (↑((fun (X : Cᵒᵖ) ↦
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                                  b₁) :
                              Type (max (max (max u' u v) v') v)))
                            (Cat.Hom.toFunctor
                              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                      Cat.of
                                        (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                                f))
                            (Cat.Hom.toFunctor
                              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                      Cat.of
                                        (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                                g))))))
                  f (g ≫ h))))) :
      Quiver.Hom (V :=
        Quiver.Hom (V := Cat)
          ((fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₀)
          ((fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₃))
        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
            (Functor.toCatHom (J.overMapPullback A f.unop) :
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
          ((f ≫ g) ≫ h))
        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
            (Functor.toCatHom (J.overMapPullback A f.unop) :
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
          (f ≫ g ≫ h)))
    (eqToHom ⋯ :
      Quiver.Hom (V :=
        Quiver.Hom (V := Cat)
          ((fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₀)
          ((fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₃))
        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
            (Functor.toCatHom (J.overMapPullback A f.unop) :
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
          ((f ≫ g) ≫ h))
        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
            (Functor.toCatHom (J.overMapPullback A f.unop) :
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
          (f ≫ g ≫ h)))
have h₁ : Eq (α :=
  Quiver.Hom (V :=
    (↑(Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A)) :
        Type (max (max (max u u') v) v')) ⥤
      (↑(Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₃)) (J.over (Opposite.unop b₃)) A)) :
        Type (max (max (max u u') v) v')))
    (Cat.Hom.toFunctor
      ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
          (Functor.toCatHom (J.overMapPullback A f.unop) :
            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
        ((f ≫ g) ≫ h)))
    (Cat.Hom.toFunctor
      ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
          (Functor.toCatHom (J.overMapPullback A f.unop) :
            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
        (f ≫ g ≫ h))))
  (Cat.Hom₂.toNatTrans
    (CategoryStruct.comp (Y :=
      CategoryStruct.comp (Y :=
        (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₂)
        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
            (Functor.toCatHom (J.overMapPullback A f.unop) :
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
          (f ≫ g))
        ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
            (Functor.toCatHom (J.overMapPullback A f.unop) :
              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
          h))
      (Iso.hom
        ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
            (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
              Iso (C :=
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                (Functor.toCatHom
                  (Functor.comp (D :=
                    (↑((fun (X : Cᵒᵖ) ↦
                            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                          b₁) :
                      Type (max (max (max u' u v) v') v)))
                    (Cat.Hom.toFunctor
                      ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                          (Functor.toCatHom (J.overMapPullback A f.unop) :
                            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                        f))
                    (Cat.Hom.toFunctor
                      ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                          (Functor.toCatHom (J.overMapPullback A f.unop) :
                            Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                              Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                        g))))))
          (f ≫ g) h))
      (CategoryStruct.comp (Y :=
        CategoryStruct.comp (Y :=
          (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₂)
          (CategoryStruct.comp (Y :=
            (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₁)
            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                (Functor.toCatHom (J.overMapPullback A f.unop) :
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
              f)
            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                (Functor.toCatHom (J.overMapPullback A f.unop) :
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
              g))
          ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
              (Functor.toCatHom (J.overMapPullback A f.unop) :
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
            h))
        (Bicategory.whiskerRight
          (Iso.hom
            ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
                  Iso (C :=
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                    (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                    (Functor.toCatHom
                      (Functor.comp (D :=
                        (↑((fun (X : Cᵒᵖ) ↦
                                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                              b₁) :
                          Type (max (max (max u' u v) v') v)))
                        (Cat.Hom.toFunctor
                          ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                              (Functor.toCatHom (J.overMapPullback A f.unop) :
                                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                            f))
                        (Cat.Hom.toFunctor
                          ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                              (Functor.toCatHom (J.overMapPullback A f.unop) :
                                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                            g))))))
              f g))
          ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
              (Functor.toCatHom (J.overMapPullback A f.unop) :
                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
            h))
        (Iso.hom
            (Bicategory.associator
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                f)
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                g)
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                h)) ≫
          CategoryStruct.comp (Y :=
            CategoryStruct.comp (Y :=
              (fun (X : Cᵒᵖ) ↦ Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A)) b₁)
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                f)
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                (g ≫ h)))
            (Bicategory.whiskerLeft
              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                f)
              (Iso.inv
                ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                    (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
                      Iso (C :=
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                          Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                        (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                        (Functor.toCatHom
                          (Functor.comp (D :=
                            (↑((fun (X : Cᵒᵖ) ↦
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                                  b₁) :
                              Type (max (max (max u' u v) v') v)))
                            (Cat.Hom.toFunctor
                              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                      Cat.of
                                        (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                                f))
                            (Cat.Hom.toFunctor
                              ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                  (Functor.toCatHom (J.overMapPullback A f.unop) :
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                      Cat.of
                                        (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                                g))))))
                  g h)))
            (Iso.inv
              ((fun {b₀ b₁ b₂ : Cᵒᵖ} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                  (Cat.Hom.isoMk (Iso.symm (J.overMapPullbackComp A g.unop f.unop)) :
                    Iso (C :=
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₀)) (J.over (Opposite.unop b₀)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b₂)) (J.over (Opposite.unop b₂)) A))
                      (Functor.toCatHom (J.overMapPullback A (f ≫ g).unop))
                      (Functor.toCatHom
                        (Functor.comp (D :=
                          (↑((fun (X : Cᵒᵖ) ↦
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                                b₁) :
                            Type (max (max (max u' u v) v') v)))
                          (Cat.Hom.toFunctor
                            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                (Functor.toCatHom (J.overMapPullback A f.unop) :
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                              f))
                          (Cat.Hom.toFunctor
                            ((fun {b b' : Cᵒᵖ} (f : b ⟶ b') ↦
                                (Functor.toCatHom (J.overMapPullback A f.unop) :
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b)) (J.over (Opposite.unop b)) A) ⟶
                                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop b')) (J.over (Opposite.unop b')) A)))
                              g))))))
                f (g ≫ h)))))))
  (Cat.Hom₂.toNatTrans (eqToHom sorry))
Tactic: ext1