-- Module: Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
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 :=
      (↑(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 ⋯))

Tactic:
simpa [overMapPullbackCongr_eq_eqToIso] using
      J.overMapPullback_assoc A h.unop g.unop f.unop

Premises used: Quiver.Hom.unop, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_eq_eqToIso, CategoryTheory.GrothendieckTopology.overMapPullback_assoc