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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C ≤ ⊤

pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊤ ≤ discrete C

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C ≤ ⊤
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊤ ≤ discrete C

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊤ ≤ discrete C
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊤ ≤ discrete C

Tactic:
intro X S _

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
a✝ : S ∈ ⊤ X
⊢ S ∈ (discrete C) X
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ trivial C ≤ ⊥

pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊥ ≤ trivial C

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ trivial C ≤ ⊥
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i : ι' ⊕ α
⊢ (Presieve.ofArrows (fun j ↦ Y (incl i) (fibincl i j)) fun j ↦ g (incl i) (fibincl i j)) ∈ J.coverings (X (incl i))

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i : ι' ⊕ α
⊢ (Presieve.ofArrows (fun j ↦ Y (incl i) (fibincl i j)) fun j ↦ g (incl i) (fibincl i j)) ∈ J.coverings (X (incl i))
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊥ ≤ trivial C

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊥ ≤ trivial C
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ IsIso (pullback.snd g f)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) = Presieve.singleton (pullback.snd g f)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ IsIso (pullback.snd g f)
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), ⊥ ∈ J X
⊢ ⊤ ≤ J

Tactic:
intro X S _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), ⊥ ∈ J X
X : C
S : Sieve X
a✝ : S ∈ ⊤ X
⊢ S ∈ J X
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.fst g f = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f

Tactic:
·

Goal state after:
case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.fst g f = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) = Presieve.singleton (pullback.snd g f)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) = Presieve.singleton (pullback.snd g f)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ IsIso (f ≫ g)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ IsIso (f ≫ g)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ (Presieve.singleton g).bind Ti K → Presieve.singleton (f ≫ g) K

pp: case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ Presieve.singleton (f ≫ g) K → (Presieve.singleton g).bind Ti K

Tactic:
·

Goal state after:
case refine_2.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ (Presieve.singleton g).bind Ti K → Presieve.singleton (f ≫ g) K
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ Presieve.singleton (f ≫ g) K → (Presieve.singleton g).bind Ti K

Tactic:
·

Goal state after:
case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ Presieve.singleton (f ≫ g) K → (Presieve.singleton g).bind Ti K
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows Z g).bind Ti ≤ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst

pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ≤ (ofArrows Z g).bind Ti

Tactic:
·

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows Z g).bind Ti ≤ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ≤ (ofArrows Z g).bind Ti

Tactic:
·

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ≤ (ofArrows Z g).bind Ti
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P → ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) → IsSheaf K.toGrothendieck P

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P → ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) → IsSheaf K.toGrothendieck P

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) → IsSheaf K.toGrothendieck P
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (generate R)).arrows

Tactic:
rw [← pullbackArrows_comm, ← isSheafFor_iff_generate]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (pullbackArrows f R)
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_1
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
i : s.pt
⊢ (Fork.ofι f w).pt

pp: case refine_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ (↾fun i ↦ ?refine_1) ≫ (Fork.ofι f w).ι = s.ι

pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ ?refine_1

Tactic:
·

Goal state after:
case refine_1
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
i : s.pt
⊢ (Fork.ofι f w).pt
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ (↾fun i ↦ Classical.choose ⋯) ≫ (Fork.ofι f w).ι = s.ι

pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯

Tactic:
·

Goal state after:
case refine_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ (↾fun i ↦ Classical.choose ⋯) ≫ (Fork.ofι f w).ι = s.ι
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯

Tactic:
·

Goal state after:
case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g → f = g

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g

Tactic:
·

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g → f = g
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g

Tactic:
·

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h → singleton (pullback.snd g f) h

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ singleton (pullback.snd g f) h → pullbackArrows f (singleton g) h

Tactic:
·

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h → singleton (pullback.snd g f) h
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ singleton (pullback.snd g f) h → pullbackArrows f (singleton g) h

Tactic:
·

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ singleton (pullback.snd g f) h → pullbackArrows f (singleton g) h
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
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✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h → pullbackArrows f (ofArrows Z g) h

pp: case mpr
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✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ pullbackArrows f (ofArrows Z g) h → ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h

Tactic:
·

Goal state after:
case mp
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✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h → pullbackArrows f (ofArrows Z g) h
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m✝ : s.pt ⟶ (Fork.ofι (↾Subtype.val) ⋯).pt
hm : m✝ ≫ (Fork.ofι (↾Subtype.val) ⋯).ι = s.ι
⊢ m✝ = ↾fun i ↦ ⟨(hom s.ι) i, ⋯⟩

Tactic:
by ext x; exact Subtype.ext (by exact congr_hom hm x)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
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✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ pullbackArrows f (ofArrows Z g) h → ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h

Tactic:
·

Goal state after:
case mpr
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✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ pullbackArrows f (ofArrows Z g) h → ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h