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

Goal state before:
pp: case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ J₁.Covers M f → J₁.Covers N f

pp: case refine_1.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ J₁.Covers N f → J₁.Covers M f

Tactic:
·

Goal state after:
case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ J₁.Covers M f → J₁.Covers N f
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ J₁.Covers N f → J₁.Covers M f

Tactic:
·

Goal state after:
case refine_1.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ J₁.Covers N f → J₁.Covers M f
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.left)

pp: case left.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.right)

pp: case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)

pp: case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)

pp: case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case left.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.left)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.right)

pp: case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)

pp: case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)

pp: case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case left.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.right)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)

pp: case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)

pp: case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)

pp: case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M ≤ ↑(x f hf)

pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(x f hf) ≤ Sieve.pullback f M

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M ≤ ↑(x f hf)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
·

Goal state after:
case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ (pullback₂ f E).presieve₀ ≤ Presieve.pullbackArrows f E.presieve₀

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ Presieve.pullbackArrows f E.presieve₀ ≤ (pullback₂ f E).presieve₀

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ (pullback₂ f E).presieve₀ ≤ Presieve.pullbackArrows f E.presieve₀
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ Presieve.pullbackArrows f E.presieve₀ ≤ (pullback₂ f E).presieve₀

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ Presieve.pullbackArrows f E.presieve₀ ≤ (pullback₂ f E).presieve₀
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(x f hf) ≤ Sieve.pullback f M

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(x f hf) ≤ Sieve.pullback f M
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f ≤ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f

pp: case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f ≤ Presieve.ofArrows (E.sum F).X (E.sum F).f

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f ≤ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a.inl
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Z : C
g : Z ⟶ S
val✝ : E.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f (Sum.inl val✝))

pp: case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Z : C
g : Z ⟶ S
val✝ : F.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f (Sum.inr val✝))

Tactic:
·

Goal state after:
case a.inl
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Z : C
g : Z ⟶ S
val✝ : E.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f (Sum.inl val✝))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Z : C
g : Z ⟶ S
val✝ : F.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f (Sum.inr val✝))

Tactic:
·

Goal state after:
case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Z : C
g : Z ⟶ S
val✝ : F.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f (Sum.inr val✝))
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ (F.mapCone c).π.app j = s.π.app j

Tactic:
·

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f ≤ Presieve.ofArrows (E.sum F).X (E.sum F).f

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f ≤ Presieve.ofArrows (E.sum F).X (E.sum F).f
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a.inl
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : E.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (E.f i)

pp: case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)

Tactic:
·

Goal state after:
case a.inl
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : E.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (E.f i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)

Tactic:
·

Goal state after:
case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ (F.mapCone c).π.app j = s.π.app j

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ (F.mapCone c).π.app j = s.π.app j
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂

pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁

Tactic:
·

Goal state after:
case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
⊢ J.toGrothendieck ≤ sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}

pp: case refine_2
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
⊢ sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X} ≤ J.toGrothendieck

Tactic:
·

Goal state after:
case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
⊢ J.toGrothendieck ≤ sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_2
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
⊢ sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X} ≤ J.toGrothendieck

Tactic:
·

Goal state after:
case refine_2
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
⊢ sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X} ≤ J.toGrothendieck
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

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

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

Tactic:
·

Goal state after:
case mp
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows