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
X : Cᵒᵖ
F : Sheaf J (Type (max v v'))
⊢ Eq (α :=
    (((uliftYoneda.{v', v, u} J).op ⋙ coyoneda).obj X).obj F ≅
      ((evaluation Cᵒᵖ (Type (max v v')) ⋙
                obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v v')) (Type (max v v')) (Type (max (max v v') u)))
                    uliftFunctor.{u, max v v'} ⋙
                  obj (whiskeringLeft (Sheaf J (Type (max v v'))) (Cᵒᵖ ⥤ Type (max v v')) (Type (max (max v v') u)))
                    (sheafToPresheaf J (Type (max v v')))).obj
            X).obj
        F)
    (Iso.app (Iso.app J.uliftYonedaOpCompCoyoneda X) F)
    (Equiv.toIso (Equiv.trans J.uliftYonedaEquiv (Equiv.symm Equiv.ulift)))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, TypeCat.Fun.comp, Equiv.toIso, CategoryTheory.ObjectProperty.homMk, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
⊢ PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda

Tactic:
⟨fun {I} _ ↦ ?_⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
refine : ∀ {I : Type u_2} (x : Category.{u_1, u_2} I), PreservesLimitsOfShape I J.yoneda
⊢ PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda

Tactic:
refine ⟨fun {I} _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
I : Type u_2
x : Category.{u_1, u_2} I
⊢ PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J (Type v))

Tactic:
have : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J _) :=
    inferInstanceAs <| PreservesLimitsOfShape I CategoryTheory.yoneda
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
I : Type u_2
x : Category.{u_1, u_2} I
this : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J (Type v))
⊢ PreservesLimitsOfShape I J.yoneda

Tactic:
preservesLimitsOfShape_of_reflects_of_preserves _ (sheafToPresheaf J _)

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
I : Type u_2
x : Category.{u_1, u_2} I
this : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J (Type v))
⊢ PreservesLimitsOfShape I J.yoneda

Tactic:
exact preservesLimitsOfShape_of_reflects_of_preserves _ (sheafToPresheaf J _)

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.sheafToPresheaf
-- 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)
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
pos :
  ∀ (h : i = 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)))
neg :
  ∀ (h : ¬i = 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)))
⊢ 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)))

Tactic:
by_cases h : i = 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)
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
h : i = j
pos :
  ∀ (b : Y ⟶ X i) (hab : a ≫ c.inj i = b ≫ c.inj i),
    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 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)))
          b :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ 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)))

Tactic:
subst h
-- 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)
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
Y : C
i : ι
a b : Y ⟶ X i
hab : a ≫ c.inj i = b ≫ c.inj i
pos pos₁ :
  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)))
        b :
      (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)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ 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 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)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))

Tactic:
rw [(cancel_mono _).mp hab]

Premises used: CategoryTheory.cancel_mono, Iff.mp
-- 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)
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
h : ¬i = j
neg :
  ∀ (h : IsInitial.{v, u} Y),
    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)))
⊢ 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)))

Tactic:
obtain ⟨h⟩ := hdisj h a b hab
-- 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)
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
h_1 : ¬i = j
h : IsInitial.{v, u} Y
neg :
  ∀ (this : Unique (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y))),
    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)))
⊢ 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)))

Tactic:
have := Types.isTerminalEquivUnique _ (Sheaf.isTerminalOfBotCover s.pt _ (hempty Y h))
-- 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)
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
h_1 : ¬i = j
h : IsInitial.{v, u} Y
this : Unique (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y))
⊢ 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)))

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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)
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
h_1 : ¬i = j
h : IsInitial.{v, u} Y
this : Unique (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y))
⊢ 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)))

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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)
⊢ ∀ (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)))

Tactic:
have heq (s : Cofan 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) :
      (s.inj i).hom.app (op Y) a = (s.inj j).hom.app (op Y) b := by
    by_cases h : i = j
    · subst h
      rw [(cancel_mono _).mp hab]
    · obtain ⟨h⟩ := hdisj h a b hab
      have := Types.isTerminalEquivUnique _ (Sheaf.isTerminalOfBotCover s.pt _ (hempty Y h))
      exact Subsingleton.elim _ _
-- 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 : (Sieve.ofArrows X c.inj).functor ⟶ s.pt.obj (P := Presheaf.IsSheaf J)
⊢ (Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ J.yoneda.obj (X i))
          (Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) ↦ J.yoneda.map (c.inj i))).obj
      (P := Presheaf.IsSheaf J) ⟶
    s.pt.obj (P := Presheaf.IsSheaf J)

Tactic:
refine (s.pt.2.isSheafFor _ H).extend ?_

Premises used: CategoryTheory.Presieve.IsSheafFor.extend, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.isSheafFor, CategoryTheory.Limits.Cocone.pt