awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η
γ' : Functor.obj (presheafToSheaf J D) P ⟶ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ :=
  { hom := γ }
rw :
  CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D) P)
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P) (Functor.map (sheafToPresheaf J D) γ') =
    η
⊢ γ'.hom =
    InducedCategory.Hom.hom
      ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J D) P
              (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) :
          (a : P ⟶ (sheafToPresheaf J D).obj { obj := Q, property := hQ }) →
            (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ })
        η)

Tactic:
rw [← Sheaf.hom_ext_iff, ← Adjunction.homEquiv_apply_eq, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Sheaf.hom_ext_iff, CategoryTheory.Adjunction.homEquiv_apply_eq
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η
γ' : Functor.obj (presheafToSheaf J D) P ⟶ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ :=
  { hom := γ }
⊢ CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D) P)
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P) (Functor.map (sheafToPresheaf J D) γ') =
    η

Tactic:
h
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η
γ' : Functor.obj (presheafToSheaf J D) P ⟶ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ :=
  { hom := γ }
⊢ CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D) P)
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P) (Functor.map (sheafToPresheaf J D) γ') =
    η

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
a : CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (Iso.inv (isoSheafify J hP)) = 𝟙 P
⊢ Eq (α := sheafify J P ⟶ P) (Iso.inv (isoSheafify J hP)) (sheafifyLift J (𝟙 P) hP)

Tactic:
apply sheafifyLift_unique

Premises used: CategoryTheory.sheafifyLift_unique
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (Iso.inv (isoSheafify J hP)) = 𝟙 P

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
rw : sheafifyLift J (toSheafify J P ≫ η) hQ = γ
⊢ η = γ

Tactic:
rw [sheafifyLift_unique J _ hQ _ h, ← h]

Premises used: CategoryTheory.sheafifyLift_unique
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ sheafifyLift J (toSheafify J P ≫ η) hQ = γ

Tactic:
(sheafifyLift_unique J _ hQ _ h.symm).symm

Premises used: CategoryTheory.sheafifyLift_unique, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ sheafifyLift J (toSheafify J P ≫ η) hQ = γ

Tactic:
exact (sheafifyLift_unique J _ hQ _ h.symm).symm

Premises used: CategoryTheory.sheafifyLift_unique, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
a : CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (sheafifyMap J η ≫ sheafifyLift J γ hR) = η ≫ γ
⊢ Eq (α := sheafify J P ⟶ R) (sheafifyMap J η ≫ sheafifyLift J γ hR) (sheafifyLift J (η ≫ γ) hR)

Tactic:
apply sheafifyLift_unique

Premises used: CategoryTheory.sheafifyLift_unique
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
a : CategoryStruct.comp (Y := sheafify J Q) (toSheafify J P ≫ sheafifyMap J η) (sheafifyLift J γ hR) = η ≫ γ
a₁ : CategoryStruct.comp (Y := sheafify J Q) (η ≫ toSheafify J Q) (sheafifyLift J γ hR) = η ≫ γ
a₂ : η ≫ CategoryStruct.comp (Y := sheafify J Q) (toSheafify J Q) (sheafifyLift J γ hR) = η ≫ γ
a₃ a₄ : η ≫ γ = η ≫ γ
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P) (sheafifyMap J η ≫ sheafifyLift J γ hR) = η ≫ γ

Tactic:
rw [← Category.assoc, ← toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.toSheafify_sheafifyLift, CategoryTheory.toSheafify_naturality
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
F P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
a : F ⟶ P
hP : Presheaf.IsSheaf J P
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ CategoryStruct.comp (Y := sheafify J F) (toSheafify J F) (sheafifyLift J a hP ≫ η) = a ≫ η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
h :
  InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J)))
        { hom := Iso.hom (isoSheafify J ⋯) } { hom := Iso.inv (isoSheafify J ⋯) }) =
    InducedCategory.Hom.hom (𝟙 P)
⊢ CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J)))
      { hom := Iso.hom (isoSheafify J ⋯) } { hom := Iso.inv (isoSheafify J ⋯) } =
    𝟙 P

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J)))
        { hom := Iso.hom (isoSheafify J ⋯) } { hom := Iso.inv (isoSheafify J ⋯) }) =
    InducedCategory.Hom.hom (𝟙 P)

Tactic:
apply (isoSheafify J P.2).hom_inv_id

Premises used: CategoryTheory.isoSheafify, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
h :
  InducedCategory.Hom.hom
      ({ hom := Iso.inv (isoSheafify J ⋯) } ≫
        { hom := Iso.hom (isoSheafify J ⋯) :
          InducedCategory.Hom (D := Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D) (F :=
            ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) P
            (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))) }) =
    InducedCategory.Hom.hom (𝟙 (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))))
⊢ { hom := Iso.inv (isoSheafify J ⋯) } ≫
      { hom := Iso.hom (isoSheafify J ⋯) :
        InducedCategory.Hom (D := Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D) (F :=
          ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) P
          (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))) } =
    𝟙 (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J)))

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
⊢ InducedCategory.Hom.hom
      ({ hom := Iso.inv (isoSheafify J ⋯) } ≫
        { hom := Iso.hom (isoSheafify J ⋯) :
          InducedCategory.Hom (D := Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D) (F :=
            ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) P
            (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))) }) =
    InducedCategory.Hom.hom (𝟙 (Functor.obj (presheafToSheaf J D) (P.obj (P := Presheaf.IsSheaf J))))

Tactic:
apply (isoSheafify J P.2).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.isoSheafify, CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
⊢ IsIso (X := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) P)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) P)

Tactic:
isIso_of_fully_faithful (sheafToPresheaf J D) _

Premises used: CategoryTheory.isIso_of_fully_faithful, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
⊢ IsIso (X := (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) P).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) P))

Tactic:
inferInstanceAs (IsIso ((sheafToPresheaf J D).map _))

Premises used: _private.0.CategoryTheory.instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction._proof_1
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
⊢ IsIso (C := Sheaf.{v₁, v_1, u₁, u_1} J D ⥤ Sheaf.{v₁, v_1, u₁, u_1} J D) (X :=
    sheafToPresheaf J D ⋙ presheafToSheaf J D) (Adjunction.counit (sheafificationAdjunction J D))

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
rw :
  CategoryStruct.comp (Y :=
      (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)).obj
        (P := Presheaf.IsSheaf J))
      (sheafifyLift J (𝟙 P) hP ≫ toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    𝟙 (sheafify J P) ≫
      InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))
⊢ sheafifyLift J (𝟙 P) hP ≫ toSheafify J P = 𝟙 (sheafify J P)

Tactic:
rw [← cancel_mono ((sheafificationAdjunction J D).counit.app ⟨P, hP⟩).hom]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.cancel_mono, CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.counit, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ ⊤ f

Tactic:
trivial

Premises used: trivial
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ ⊥ f ↔ False

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z_1 : C
f : Y ⟶ X
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve.{v₁, u₁} Y
Z : C
h : Z ⟶ X
H : S.bind R h
obtain : ∀ (Y : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S f) (hg : R hf g) (fac : g ≫ f = h), Nonempty (S.BindStruct R h)
⊢ Nonempty (S.BindStruct R h)

Tactic:
obtain ⟨Y, g, f, hf, hg, fac⟩ := H
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve.{v₁, u₁} Y
Z : C
h : Z ⟶ X
Y : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S f
hg : R hf g
fac : g ≫ f = h
⊢ Nonempty (S.BindStruct R h)

Tactic:
⟨{ hf := hf, hg := hg, fac := fac, .. }⟩

Premises used: Nonempty.intro, CategoryTheory.Presieve.BindStruct.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve.{v₁, u₁} Y
Z : C
h : Z ⟶ X
Y : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S f
hg : R hf g
fac : g ≫ f = h
⊢ Nonempty (S.BindStruct R h)

Tactic:
exact ⟨{ hf := hf, hg := hg, fac := fac, .. }⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve.{v₁, u₁} Y
Z : C
h : Z ⟶ X
b : S.BindStruct R h
⊢ S.bind R h

Tactic:
⟨b.Y, b.g, b.f, b.hf, b.hg, b.fac⟩

Premises used: CategoryTheory.Presieve.bind, CategoryTheory.Presieve.BindStruct.Y, CategoryTheory.Presieve.BindStruct.f, And.intro, CategoryTheory.Presieve.BindStruct.g, Exists.intro, CategoryTheory.Presieve.BindStruct.hf, CategoryTheory.Presieve.BindStruct.fac, CategoryTheory.Presieve.BindStruct.hg
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve.{v₁, u₁} Y
g : Z ⟶ Y
h₁ : S f
h₂ : R h₁ g
⊢ S.bind R (g ≫ f)

Tactic:
⟨_, _, _, h₁, h₂, rfl⟩

Premises used: CategoryTheory.Presieve.bind, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
mp : singleton f g → f = g
mpr : f = g → singleton f g
⊢ singleton f g ↔ f = g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
Y : C
⊢ f = f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ singleton f f

Tactic:
apply singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ singleton f f

Tactic:
singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z_1 : C
f : Y ⟶ X
g : Z_1 ⟶ X
inst_2 : HasPullback g f
Z : C
h : Z ⟶ X
⊢ HasPullback g f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
h :
  ∀ (W : C),
    Eq (α := (W ⟶ Y) → Prop) (pullbackArrows f (singleton g)) (singleton (Y := pullback g f) (pullback.snd g f))
⊢ pullbackArrows f (singleton g) = singleton (Y := pullback g f) (pullback.snd g f)

Tactic:
funext W
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
W : C
h : ∀ (h : W ⟶ Y), pullbackArrows f (singleton g) h ↔ singleton (Y := pullback g f) (pullback.snd g f) h
⊢ Eq (α := (W ⟶ Y) → Prop) (pullbackArrows f (singleton g)) (singleton (Y := pullback g f) (pullback.snd g f))

Tactic:
ext h
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
W : C
h : W ⟶ Y
h₁ : pullbackArrows f (singleton g) h → singleton (Y := pullback g f) (pullback.snd g f) h
h₂ : singleton (Y := pullback g f) (pullback.snd g f) h → pullbackArrows f (singleton g) h
⊢ pullbackArrows f (singleton g) h ↔ singleton (Y := pullback g f) (pullback.snd g f) h

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 Z : C
f : Y_1 ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
Y_2 Y : C
⊢ singleton (Y := pullback g f) (pullback.snd g f) (Y := pullback g f) (pullback.snd g f)

Tactic:
singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 Z : C
f : Y_1 ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
Y_2 Y : C
⊢ singleton (Y := pullback g f) (pullback.snd g f) (Y := pullback g f) (pullback.snd g f)

Tactic:
exact singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 Z : C
f : Y_1 ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
Y : C
⊢ pullbackArrows f (singleton g) (Y := pullback g f) (pullback.snd g f)

Tactic:
pullbackArrows.mk Z g singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk, CategoryTheory.Presieve.pullbackArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 Z : C
f : Y_1 ⟶ X
g : Z ⟶ X
inst_1 : HasPullback g f
Y : C
⊢ pullbackArrows f (singleton g) (Y := pullback g f) (pullback.snd g f)

Tactic:
exact pullbackArrows.mk Z g singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk, CategoryTheory.Presieve.pullbackArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
g : Z ⟶ X
i : ι
h : Z = Y i
hg : g = eqToHom h ≫ f i
subst : ∀ {g : Y i ⟶ X} (hg : g = eqToHom ⋯ ≫ f i), ofArrows Y f g
⊢ ofArrows Y f g

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
g : Y i ⟶ X
hg : g = eqToHom ⋯ ≫ f i
⊢ g = f i

Tactic:
simp only [eqToHom_refl, id_comp] at hg

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
g : Y i ⟶ X
hg : g = f i
subst : ofArrows Y f (f i)
⊢ ofArrows Y f g

Tactic:
subst hg
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
⊢ ofArrows Y f (f i)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
h :
  ∀ (T : C),
    Eq (α := (T ⟶ Y) → Prop) (ofArrows (fun (i : ι) ↦ pullback (g i) f) fun (x : ι) ↦ pullback.snd (g x) f)
      (pullbackArrows f (ofArrows Z g))
⊢ (ofArrows (fun (i : ι) ↦ pullback (g i) f) fun (x : ι) ↦ pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)

Tactic:
funext T
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
T : C
h :
  ∀ (h : T ⟶ Y),
    ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h ↔ pullbackArrows f (ofArrows Z g) h
⊢ Eq (α := (T ⟶ Y) → Prop) (ofArrows (fun (i : ι) ↦ pullback (g i) f) fun (x : ι) ↦ pullback.snd (g x) f)
    (pullbackArrows f (ofArrows Z g))

Tactic:
ext h
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
h₁ :
  ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h → pullbackArrows f (ofArrows Z g) h
h₂ :
  pullbackArrows f (ofArrows Z g) h → ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h
⊢ ofArrows (fun (i : ι) ↦ pullback (g i) f) (fun (x : ι) ↦ pullback.snd (g x) f) h ↔ pullbackArrows f (ofArrows Z g) h

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
Y : C
hk : ι
⊢ pullbackArrows f (ofArrows Z g) (Y := pullback (g hk) f) (pullback.snd (g hk) f)

Tactic:
pullbackArrows.mk _ _ (ofArrows.mk hk)

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.pullbackArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
Y : C
hk : ι
⊢ pullbackArrows f (ofArrows Z g) (Y := pullback (g hk) f) (pullback.snd (g hk) f)

Tactic:
exact pullbackArrows.mk _ _ (ofArrows.mk hk)

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.pullbackArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst_1 : ∀ (i : ι), HasPullback (g i) f
Y_2 Y : C
i : ι
⊢ ofArrows (fun (i : ι) ↦ pullback (g i) f) fun (x : ι) ↦ pullback.snd (g x) f (Y := pullback (g i) f)
    (pullback.snd (g i) f)

Tactic:
apply ofArrows.mk

Premises used: CategoryTheory.Presieve.ofArrows.mk