-- 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₁ : Cᵒᵖ
f : 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 ≫ 𝟙 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 ⋯))

Tactic:
simpa [overMapPullbackCongr_eq_eqToIso] using
      J.overMapPullback_id_comp A f.unop

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