awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
mpr :
  (Sieve.pullback f (Sieve.generate S)).arrows g →
    ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g →
    ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
h : (Sieve.pullback f (Sieve.generate S)).arrows g
mpr :
  ∀ (R : Presieve.{v_1, u_2} Z) (hR1 : R ∈ K.coverings Z) (hR2 : R.FactorsThruAlong T g),
    ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g
⊢ ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g

Tactic:
obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1

Premises used: CategoryTheory.Coverage.pullback
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
h : (Sieve.pullback f (Sieve.generate S)).arrows g
R : Presieve.{v_1, u_2} Z
hR1 : R ∈ K.coverings Z
hR2 : R.FactorsThruAlong T g
⊢ ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g

Tactic:
⟨R, (H _ hR1).isSeparatedFor, hR2⟩

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
h : (Sieve.pullback f (Sieve.generate S)).arrows g
R : Presieve.{v_1, u_2} Z
hR1 : R ∈ K.coverings Z
hR2 : R.FactorsThruAlong T g
⊢ ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g

Tactic:
exact ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
⊢ IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P

Tactic:
⟨fun h ↦ ⟨Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_left) h,
      Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_right) h⟩, fun h ↦ ?_⟩

Premises used: le_sup_left, le_sup_right, CategoryTheory.Coverage.gi, And.intro, Iff.intro, GaloisConnection.monotone_l, CategoryTheory.Presieve.isSheaf_of_le, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
refine : ∀ (h : IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P), IsSheaf (K ⊔ L).toGrothendieck P
⊢ IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P

Tactic:
refine ⟨fun h ↦ ⟨Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_left) h,
      Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_right) h⟩, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R

Tactic:
rw [isSheaf_coverage, isSheaf_coverage] at h

Premises used: CategoryTheory.Presieve.isSheaf_coverage
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
rw : ∀ {X : C}, ∀ R ∈ (K ⊔ L).coverings X, IsSheafFor P R
⊢ IsSheaf (K ⊔ L).toGrothendieck P

Tactic:
rw [isSheaf_coverage]

Premises used: CategoryTheory.Presieve.isSheaf_coverage
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ (K ⊔ L).coverings X
inl : ∀ (hR : R ∈ K.coverings X), IsSheafFor P R
inr : ∀ (hR : R ∈ L.coverings X), IsSheafFor P R
⊢ IsSheafFor P R

Tactic:
rcases hR with hR | hR
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ K.coverings X
⊢ IsSheafFor P R

Tactic:
h.1 R hR

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ K.coverings X
⊢ IsSheafFor P R

Tactic:
exact h.1 R hR

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R

Tactic:
h.2 R hR

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R

Tactic:
exact h.2 R hR

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.HasPullbacks
inst_2 : J.IsStableUnderBaseChange
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
rw : Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
rw₁ :
  Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
rw₂ rw₃ :
  (∀ {X : C}, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R

Tactic:
rw [← J.toCoverage_toPrecoverage, Coverage.toGrothendieck_toPrecoverage,
    Presieve.isSheaf_coverage]

Premises used: CategoryTheory.Coverage.toGrothendieck_toPrecoverage, CategoryTheory.Presieve.isSheaf_coverage, CategoryTheory.Precoverage.toCoverage_toPrecoverage
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
rw :
  (∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R) ↔
    ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
      Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
⊢ Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
      Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)

Tactic:
rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]

Premises used: CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
⊢ (∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R) ↔
    ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
      Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)

Tactic:
⟨fun h X E ↦ h _ E.mem₀, fun h X R hR ↦ ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, Iff.intro, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
refine :
  ∀
    (h :
      ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
        Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover))
    (X : C) (R : Presieve.{v_1, u_2} X) (hR : R ∈ J.coverings X), Presieve.IsSheafFor P R
⊢ (∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R) ↔
    ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
      Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)

Tactic:
refine ⟨fun h X E ↦ h _ E.mem₀, fun h X R hR ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ J.coverings X
obtain : ∀ (E₀ : PreZeroHypercover X) (hR : E₀.presieve₀ ∈ J.coverings X), Presieve.IsSheafFor P E₀.presieve₀
⊢ Presieve.IsSheafFor P R

Tactic:
obtain ⟨E₀, rfl⟩ := R.exists_eq_preZeroHypercover

Premises used: CategoryTheory.Presieve.exists_eq_preZeroHypercover, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
rw : Presieve.IsSheafFor P (Sieve.generate E₀.presieve₀).arrows
⊢ Presieve.IsSheafFor P E₀.presieve₀

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
h₁ :
  (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover)).arrows ≤
    (Sieve.generate E₀.presieve₀).arrows
trans :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P
      (Sieve.pullback f
          (Sieve.generate
            (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover))).arrows
⊢ Presieve.IsSheafFor P (Sieve.generate E₀.presieve₀).arrows

Tactic:
apply Presieve.isSheafFor_subsieve
      (S := .generate <| (ZeroHypercover.restrictIndexOfSmall.{w} E).presieve₀)
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
⊢ PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover ≤ E₀.presieve₀

Tactic:
simp [E]
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
⊢ (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover)).arrows ≤
    (Sieve.generate E₀.presieve₀).arrows

Tactic:
exact Sieve.generate_mono (by simp [E])

Premises used: CategoryTheory.Sieve.generate_mono
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
Y : C
f : Y ⟶ X
trans :
  Presieve.IsSheafFor P
    (PreZeroHypercover.presieve₀.{w, v_1, u_2} (ZeroHypercover.pullback₂ f E.restrictIndexOfSmall).toPreZeroHypercover)
⊢ Presieve.IsSheafFor P
    (Sieve.pullback f
        (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover))).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.isSheafFor_iff_generate,
      ← PreZeroHypercover.presieve₀_pullback₁, ← ZeroHypercover.pullback₂_toPreZeroHypercover]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover, CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.PreZeroHypercover.presieve₀_pullback₁, CategoryTheory.Sieve.pullbackArrows_comm
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P
    (PreZeroHypercover.presieve₀.{w, v_1, u_2} (ZeroHypercover.pullback₂ f E.restrictIndexOfSmall).toPreZeroHypercover)

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
K : Coverage.{v_1, u_1} C
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
simp :
  (∀ (E : D) {X : C}, ∀ R ∈ K.coverings X, Presieve.IsSheafFor (P ⋙ Functor.obj coyoneda (Opposite.op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (E : Dᵒᵖ), Presieve.IsSheafFor (P ⋙ Functor.obj coyoneda E) R
⊢ IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
simp only [Presheaf.IsSheaf, Presieve.isSheaf_coverage, isLimit_iff_isSheafFor,
    ← Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.Presieve.isSheaf_coverage, CategoryTheory.Presheaf.IsSheaf, CategoryTheory.Presheaf.isLimit_iff_isSheafFor
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
K : Coverage.{v_1, u_1} C
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
⊢ (∀ (E : D) {X : C}, ∀ R ∈ K.coverings X, Presieve.IsSheafFor (P ⋙ Functor.obj coyoneda (Opposite.op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (E : Dᵒᵖ), Presieve.IsSheafFor (P ⋙ Functor.obj coyoneda E) R

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
K L : Coverage.{v_1, u_1} C
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
⊢ IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P

Tactic:
⟨fun h ↦ ⟨fun E ↦ ((Presieve.isSheaf_sup K L _).mp (h E)).1, fun E ↦
    ((Presieve.isSheaf_sup K L _).mp (h E)).2⟩,
      fun ⟨h₁, h₂⟩ E ↦ (Presieve.isSheaf_sup K L _).mpr ⟨h₁ E, h₂ E⟩⟩

Premises used: CategoryTheory.Presieve.IsSheaf, Iff.mpr, _private.0.CategoryTheory.Presheaf.isSheaf_sup.match_1, CategoryTheory.coyoneda, CategoryTheory.Functor.comp, CategoryTheory.Coverage.toGrothendieck, And.right, And.left, Max.max, Opposite.op, And.intro, Iff.intro, Iff.mp, CategoryTheory.Functor.obj, CategoryTheory.Presieve.isSheaf_sup
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
mp : J.CoversTop Y → Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
mpr : Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X → J.CoversTop Y
⊢ J.CoversTop Y ↔ Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
mp mp₁ mp₂ mp₃ mp₄ mp₅ mp₆ mp₇ : J.CoversTop Y → Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
⊢ J.CoversTop Y → Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
W : C
apply : Sieve.pullback (hX.from W) (Sieve.ofObjects Y X) ≤ Sieve.ofObjects Y W
⊢ Sieve.ofObjects Y W ∈ (J : (a : C) → Set (Sieve a)) W

Tactic:
apply J.superset_covering _ (J.pullback_stable (hX.from W) h)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Limits.IsTerminal.from, CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
W T : C
a : T ⟶ W
i : I
b : T ⟶ Y i
⊢ Sieve.arrows (Sieve.ofObjects Y W) a

Tactic:
⟨i, ⟨b⟩⟩

Premises used: Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
W T : C
a : T ⟶ W
i : I
b : T ⟶ Y i
⊢ Sieve.arrows (Sieve.ofObjects Y W) a

Tactic:
exact ⟨i, ⟨b⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf.{v, v', u, u'} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h :
  ∀ (i : I),
    Eq (α := X ⟶ F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op (Y i))) (f ≫ c.π.app (Opposite.op (Y i)))
      (g ≫ c.π.app (Opposite.op (Y i)))
⊢ f = g

Tactic:
hc.hom_ext (fun Z => F.2.hom_ext (hY.cover Z.unop) _ _ ?_)

Premises used: CategoryTheory.GrothendieckTopology.CoversTop.cover, CategoryTheory.Limits.Cone.π, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, Opposite.unop, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf.{v, v', u, u'} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h :
  ∀ (i : I),
    Eq (α := X ⟶ F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op (Y i))) (f ≫ c.π.app (Opposite.op (Y i)))
      (g ≫ c.π.app (Opposite.op (Y i)))
refine :
  ∀ (Z : Cᵒᵖ) (I_1 : Cover.Arrow (X := Opposite.unop Z) (hY.cover (Opposite.unop Z))),
    (f ≫ c.π.app Z) ≫ F.obj (P := Presheaf.IsSheaf J).map I_1.f.op =
      (g ≫ c.π.app Z) ≫ F.obj (P := Presheaf.IsSheaf J).map I_1.f.op
⊢ f = g

Tactic:
refine hc.hom_ext (fun Z => F.2.hom_ext (hY.cover Z.unop) _ _ ?_)

Premises used: CategoryTheory.GrothendieckTopology.CoversTop.cover, CategoryTheory.Limits.Cone.π, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, Opposite.unop, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf.{v, v', u, u'} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h :
  ∀ (i : I),
    Eq (α := X ⟶ F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op (Y i))) (f ≫ c.π.app (Opposite.op (Y i)))
      (g ≫ c.π.app (Opposite.op (Y i)))
Z : Cᵒᵖ
W : C
a : W ⟶ Opposite.unop Z
i : I
b : W ⟶ Y i
⊢ Eq (α :=
    X ⟶
      F.obj (P := Presheaf.IsSheaf J).obj
        (Opposite.op (Cover.Arrow.Y (J := J) (S := hY.cover (Opposite.unop Z)) { Y := W, f := a, hf := ⋯ })))
    ((f ≫ c.π.app Z) ≫ F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (Cover.Arrow.f { Y := W, f := a, hf := ⋯ })))
    ((g ≫ c.π.app Z) ≫ F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (Cover.Arrow.f { Y := W, f := a, hf := ⋯ })))

Tactic:
simpa using h i =≫ F.1.map b.op

Premises used: Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u u_2))
h : ∀ (i : I), (↑x : (j : Cᵒᵖ) → F.obj.obj j) (Opposite.op (Y i)) = (↑y : (j : Cᵒᵖ) → F.obj.obj j) (Opposite.op (Y i))
a : ∀ (W : Cᵒᵖ), (↑x : (j : Cᵒᵖ) → F.obj.obj j) W = (↑y : (j : Cᵒᵖ) → F.obj.obj j) W
⊢ x = y

Tactic:
ext W