mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case hf
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g

Tactic:
·

Goal state after:
case hf
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mp
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J → K ≤ J.toCoverage

pp: case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ J.toCoverage → K.toGrothendieck ≤ J

Tactic:
·

Goal state after:
case mp
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J → K ≤ J.toCoverage
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ J.toCoverage → K.toGrothendieck ≤ J

Tactic:
·

Goal state after:
case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ J.toCoverage → K.toGrothendieck ≤ J
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ K.toGrothendieck ≤ sInf {J | K ≤ J.toCoverage}

pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ sInf {J | K ≤ J.toCoverage} ≤ K.toGrothendieck

Tactic:
·

Goal state after:
case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ K.toGrothendieck ≤ sInf {J | K ≤ J.toCoverage}
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ sInf {J | K ≤ J.toCoverage} ≤ K.toGrothendieck

Tactic:
·

Goal state after:
case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ sInf {J | K ≤ J.toCoverage} ≤ K.toGrothendieck
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case inl
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hx : S ∈ x.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

pp: case inr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hy : S ∈ y.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
·

Goal state after:
case inl
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hx : S ∈ x.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ∈ J.coverings S

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ∈ K.coverings S

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case inr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hy : S ∈ y.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
·

Goal state after:
case inr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hy : S ∈ y.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ∈ K.coverings S

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ∈ K.coverings S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
h : J.toCoverage.Saturate T S
⊢ ∃ R ∈ J.coverings T, R ≤ S.arrows

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
x✝ : ∃ R ∈ J.coverings T, R ≤ S.arrows
R : Presieve T
hR : R ∈ J.coverings T
hle : R ≤ S.arrows
⊢ J.toCoverage.Saturate T S

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
h : J.toCoverage.Saturate T S
⊢ ∃ R ∈ J.coverings T, R ≤ S.arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ J.coverings S

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ F.X i ⟶ E.X (e.inv.s₀ i)

pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) ?refine_2 (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ F.X i ⟶ E.X (e.inv.s₀ i)

pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) ?refine_2 (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ F.X i ⟶ E.X (e.inv.s₀ i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) (e.inv.h₀ i) (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
·

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) (e.inv.h₀ i) (𝟙 S) (E.f (e.inv.s₀ i))
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1.transitive.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
⊢ (R'.bind fun Y f hf ↦ S' ⋯) ∈ J.coverings X

pp: case refine_1.transitive.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z : C
u : Z ⟶ X
hu : R'.bind (fun Y f hf ↦ S' ⋯) u
⊢ S.arrows u

Tactic:
·

Goal state after:
case refine_1.transitive.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
⊢ (R'.bind fun Y f hf ↦ S' ⋯) ∈ J.coverings X
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1.transitive.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z : C
u : Z ⟶ X
hu : R'.bind (fun Y f hf ↦ S' ⋯) u
⊢ S.arrows u

Tactic:
·

Goal state after:
case refine_1.transitive.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z : C
u : Z ⟶ X
hu : R'.bind (fun Y f hf ↦ S' ⋯) u
⊢ S.arrows u
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
x✝ : ∃ R ∈ J.coverings T, R ≤ S.arrows
R : Presieve T
hR : R ∈ J.coverings T
hle : R ≤ S.arrows
⊢ J.toCoverage.Saturate T S

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
x✝ : ∃ R ∈ J.coverings T, R ≤ S.arrows
R : Presieve T
hR : R ∈ J.coverings T
hle : R ≤ S.arrows
⊢ J.toCoverage.Saturate T S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

pp: case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
·

Goal state after:
case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
·

Goal state after:
case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.H
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ T.FactorsThru (Sieve.pullback f (Sieve.generate S)).arrows

pp: case mpr.hS
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ IsSheafFor P T

pp: case mpr.h
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong T f_1

Tactic:
·

Goal state after:
case mpr.H
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ T.FactorsThru (Sieve.pullback f (Sieve.generate S)).arrows
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.hS
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ IsSheafFor P T

pp: case mpr.h
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong T f_1

Tactic:
·

Goal state after:
case mpr.hS
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ IsSheafFor P T
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.h
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong T f_1

Tactic:
·

Goal state after:
case mpr.h
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong T f_1
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case inl
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : 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 X
hR : R ∈ K.coverings X
⊢ IsSheafFor P R

pp: case inr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : 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 X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R

Tactic:
·

Goal state after:
case inl
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : 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 X
hR : R ∈ K.coverings X
⊢ IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case inr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : 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 X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R

Tactic:
·

Goal state after:
case inr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : 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 X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case h
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ (Sieve.generate E.restrictIndexOfSmall.presieve₀).arrows ≤ (Sieve.generate E₀.presieve₀).arrows

pp: case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows

Tactic:
·

Goal state after:
case h
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ (Sieve.generate E.restrictIndexOfSmall.presieve₀).arrows ≤ (Sieve.generate E₀.presieve₀).arrows
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows

Tactic:
·

Goal state after:
case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P