awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
refine_1 :
  ∀ ⦃X_1 Y : Cᵒᵖ⦄ (f : X_1 ⟶ Y),
    (Sieve.ofArrows X c.inj).functor.map f ≫
        (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))
          Y =
      (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))
          X_1 ≫
        s.pt.obj (P := Presheaf.IsSheaf J).map f
⊢ (Sieve.ofArrows X c.inj).functor ⟶ s.pt.obj (P := Presheaf.IsSheaf J)

Tactic:
refine ⟨fun Y ↦ ↾fun g ↦ ((s.inj (Sieve.ofArrows.i g.2)).hom.app Y)
      (Sieve.ofArrows.h g.2), ?_⟩
-- 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)
⊢ (g ≫ Sieve.ofArrows.h ⋯) ≫ c.inj (Sieve.ofArrows.i ⋯) = Sieve.ofArrows.h ⋯ ≫ c.inj (Sieve.ofArrows.i ⋯)

Tactic:
simp
-- 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)
⊢ 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))

Tactic:
ConcreteCategory.congr_hom ((s.inj _).hom.naturality g.op) _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Limits.Cofan.inj, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.InducedCategory.Hom.hom
-- 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)
⊢ 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))

Tactic:
exact ConcreteCategory.congr_hom ((s.inj _).hom.naturality g.op) _

Premises used: Quiver.Hom.op, CategoryTheory.Limits.Cofan.inj, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.InducedCategory.Hom.hom
-- 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)
j : ι
u : (j : ι) → obj CategoryTheory.yoneda (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun (j : ι) ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
⊢ ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = map CategoryTheory.yoneda (c.inj j)

Tactic:
have (j : ι) : u j ≫ (Sieve.ofArrows _ c.inj).functorInclusion =
      CategoryTheory.yoneda.map (c.inj j) := rfl
-- 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)
j : ι
u : (j : ι) → obj CategoryTheory.yoneda (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun (j : ι) ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = map CategoryTheory.yoneda (c.inj j)
refine_2 :
  u j ≫
      {
        app := fun (Y : Cᵒᵖ) ↦
          ↾fun
              (g :
                { g : unop Y ⟶ c.pt //
                  ∃ (Y_1 : C) (h : unop Y ⟶ Y_1) (g_1 : Y_1 ⟶ c.pt), Presieve.ofArrows X c.inj g_1 ∧ h ≫ g_1 = g }) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
                (a : unop Y ⟶ X (Sieve.ofArrows.i ⋯)) → s.pt.obj.obj Y)
              (Sieve.ofArrows.h ⋯),
        naturality := ⋯ } =
    (s.inj j).hom
⊢ map CategoryTheory.yoneda (c.inj j) ≫
      ⋯.extend
        {
          app := fun (Y : Cᵒᵖ) ↦
            ↾fun
                (g :
                  { g : unop Y ⟶ c.pt //
                    ∃ (Y_1 : C) (h : unop Y ⟶ Y_1) (g_1 : Y_1 ⟶ c.pt), Presieve.ofArrows X c.inj g_1 ∧ h ≫ g_1 = g }) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
                  (a : unop Y ⟶ X (Sieve.ofArrows.i ⋯)) → s.pt.obj.obj Y)
                (Sieve.ofArrows.h ⋯),
          naturality := ⋯ : NatTrans (Sieve.ofArrows X c.inj).functor (s.pt.obj (P := Presheaf.IsSheaf J)) } =
    (s.inj j).hom

Tactic:
simp only [← this, Category.assoc, Presieve.IsSheafFor.functorInclusion_comp_extend]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend
-- 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)
j : ι
u : (j : ι) → obj CategoryTheory.yoneda (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun (j : ι) ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = map CategoryTheory.yoneda (c.inj j)
Z : Cᵒᵖ
g : unop Z ⟶ X j
⊢ (Sieve.ofArrows X c.inj).arrows (g ≫ c.inj j)

Tactic:
have h : Sieve.ofArrows X c.inj (g ≫ c.inj j) :=
      Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ j) _
-- 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)
j : ι
u : (j : ι) → obj CategoryTheory.yoneda (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun (j : ι) ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = map CategoryTheory.yoneda (c.inj j)
Z : Cᵒᵖ
g : unop Z ⟶ X j
h : (Sieve.ofArrows X c.inj).arrows (g ≫ c.inj j)
⊢ Sieve.ofArrows.h h ≫ c.inj (Sieve.ofArrows.i h) = g ≫ c.inj j

Tactic:
simp
-- 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)
j : ι
u : (j : ι) → obj CategoryTheory.yoneda (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun (j : ι) ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = map CategoryTheory.yoneda (c.inj j)
Z : Cᵒᵖ
g : unop Z ⟶ X j
h : (Sieve.ofArrows X c.inj).arrows (g ≫ c.inj j)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (u j ≫
            {
              app := fun (Y : Cᵒᵖ) ↦
                ↾fun
                    (g :
                      { g : unop Y ⟶ c.pt //
                        ∃ (Y_1 : C) (h : unop Y ⟶ Y_1) (g_1 : Y_1 ⟶ c.pt),
                          Presieve.ofArrows X c.inj g_1 ∧ h ≫ g_1 = g }) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                        (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
                      (a : unop Y ⟶ X (Sieve.ofArrows.i ⋯)) → s.pt.obj.obj Y)
                    (Sieve.ofArrows.h ⋯),
              naturality := ⋯ : NatTrans (Sieve.ofArrows X c.inj).functor (s.pt.obj (P := Presheaf.IsSheaf J)) })
          Z))
      g =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app Z)).toFun g

Tactic:
exact heq s (Sieve.ofArrows.h h) g (by simp)

Premises used: CategoryTheory.Sieve.ofArrows.h