-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
heq :
  ∀ (s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j)
    (hab : a ≫ c.inj i = b ≫ c.inj j),
    Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          a :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          b :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
Y Z : C
g : Z ⟶ Y
u : (Sieve.ofArrows X c.inj).functor.obj (op Y)
refine_1 :
  Eq (α := s.pt.obj (P := Presheaf.IsSheaf J).obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) (op Z)) :
          (a : (J.yoneda.obj (X (Sieve.ofArrows.i ⋯))).obj.obj (op Z)) → s.pt.obj.obj (op Z))
        (g ≫ Sieve.ofArrows.h ⋯) :
      s.pt.obj (P := Presheaf.IsSheaf J).obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.pt.obj (P := Presheaf.IsSheaf J).map (op g)) :
          (a : s.pt.obj.obj (op Y)) → s.pt.obj.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) (op Y)) :
              (a : (J.yoneda.obj (X (Sieve.ofArrows.i ⋯))).obj.obj (op Y)) → s.pt.obj.obj (op Y))
            (Sieve.ofArrows.h ⋯) :
          s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)) :
      s.pt.obj (P := Presheaf.IsSheaf J).obj (op Z))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((Sieve.ofArrows X c.inj).functor.map (op g) ≫
          (fun (Y : Cᵒᵖ) ↦
              (↾fun (g : (Sieve.ofArrows X c.inj).functor.obj Y) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                        (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
                      (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X (Sieve.ofArrows.i ⋯))).obj.obj Y)) →
                        (fun (X : Type v) ↦ X) (s.pt.obj.obj Y))
                    (Sieve.ofArrows.h ⋯) :
                (Sieve.ofArrows X c.inj).functor.obj Y ⟶ s.pt.obj (P := Presheaf.IsSheaf J).obj Y))
            (op Z)))
      u =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (Y : Cᵒᵖ) ↦
              (↾fun (g : (Sieve.ofArrows X c.inj).functor.obj Y) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                        (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
                      (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X (Sieve.ofArrows.i ⋯))).obj.obj Y)) →
                        (fun (X : Type v) ↦ X) (s.pt.obj.obj Y))
                    (Sieve.ofArrows.h ⋯) :
                (Sieve.ofArrows X c.inj).functor.obj Y ⟶ s.pt.obj (P := Presheaf.IsSheaf J).obj Y))
            (op Y) ≫
          s.pt.obj (P := Presheaf.IsSheaf J).map (op g)))
      u

Tactic:
simp only [Sieve.functor_obj, Sieve.generate_apply, Sieve.functor_map, Quiver.Hom.unop_op',
      TypeCat.Fun.toFun_apply, comp_apply, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
      ← heq s (g ≫ Sieve.ofArrows.h u.2)
      (Sieve.ofArrows.h <| Sieve.downward_closed _ u.2 g) (by simp)]

Premises used: CategoryTheory.Sieve.functor_obj, TypeCat.Fun.coe_mk, Quiver.Hom.unop_op', CategoryTheory.Sieve.downward_closed, CategoryTheory.Sieve.ofArrows.h, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, CategoryTheory.CategoryStruct.comp, CategoryTheory.Sieve.functor_map, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Sieve.generate_apply, Subtype.property