-- 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₁ : Cᵒᵖ
f : 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 ≫ 𝟙 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))
    (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)))
            (𝟙 b₁)))
        (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 (𝟙 b₁)))
        (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.hom
              ((fun (X : Cᵒᵖ) ↦
                  (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop X)) :
                    Iso (C :=
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A) ⟶
                        Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                      (Functor.toCatHom (J.overMapPullback A (Quiver.Hom.unop (𝟙 X))))
                      (Functor.toCatHom
                        (𝟭
                          (↑((fun (X : Cᵒᵖ) ↦
                                  Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                                X) :
                            Type (max (max (max u' u v) v') v))))))
                b₁)) ≫
          Iso.hom
            (Bicategory.rightUnitor
              ((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))) :
      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 ≫ 𝟙 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))
    (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 ≫ 𝟙 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))
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 ≫ 𝟙 b₁)))
    (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₂.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)
        ((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)))
          (𝟙 b₁)))
      (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 (𝟙 b₁)))
      (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.hom
            ((fun (X : Cᵒᵖ) ↦
                (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop X)) :
                  Iso (C :=
                    Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A) ⟶
                      Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                    (Functor.toCatHom (J.overMapPullback A (Quiver.Hom.unop (𝟙 X))))
                    (Functor.toCatHom
                      (𝟭
                        (↑((fun (X : Cᵒᵖ) ↦
                                Cat.of (Sheaf (C := Over.{v, u} (Opposite.unop X)) (J.over (Opposite.unop X)) A))
                              X) :
                          Type (max (max (max u' u v) v') v))))))
              b₁)) ≫
        Iso.hom
          (Bicategory.rightUnitor
            ((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₂.toNatTrans (eqToHom sorry))
Tactic: ext1