[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J J₁ J₂ : GrothendieckTopology C
h : J₁.sieves = J₂.sieves
⊢ J₁ = J₂
[PROOFSTEP]
cases J₁
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J J₂ : GrothendieckTopology C
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝,
        transitive' := transitive'✝ }.sieves =
    J₂.sieves
⊢ { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ } = J₂
[PROOFSTEP]
cases J₂
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
sieves✝¹ : (X : C) → Set (Sieve X)
top_mem'✝¹ : ∀ (X : C), ⊤ ∈ sieves✝¹ X
pullback_stable'✝¹ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝¹ X → Sieve.pullback f S ∈ sieves✝¹ Y
transitive'✝¹ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝¹ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝¹ Y) → R ∈ sieves✝¹ X
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹,
        transitive' := transitive'✝¹ }.sieves =
    { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝,
        transitive' := transitive'✝ }.sieves
⊢ { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹, transitive' := transitive'✝¹ } =
    { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ }
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
⊢ R ∈ sieves J X
[PROOFSTEP]
apply J.transitive sjx R fun Y f hf => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
⊢ ∀ (Y : C) (f : Y ⟶ X), S.arrows f → Sieve.pullback f R ∈ sieves J Y
[PROOFSTEP]
intros Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R ∈ sieves J Y
[PROOFSTEP]
apply covering_of_eq_top
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R = ⊤
[PROOFSTEP]
rw [← top_le_iff, ← S.pullback_eq_top_of_mem hf]
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f S ≤ Sieve.pullback f R
[PROOFSTEP]
apply Sieve.pullback_monotone _ Hss
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
⊢ R ⊓ S ∈ sieves J X
[PROOFSTEP]
apply J.transitive rj _ fun Y f Hf => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
⊢ ∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ sieves J Y
[PROOFSTEP]
intros Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ sieves J Y
[PROOFSTEP]
rw [Sieve.pullback_inter, R.pullback_eq_top_of_mem hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ sieves J Y
[PROOFSTEP]
simp [sj]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Sieve X
⊢ S ∈ sieves J X ↔ Covers J S (𝟙 X)
[PROOFSTEP]
simp [covers_iff]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ Covers J S f
[PROOFSTEP]
rw [Covers, (Sieve.pullback_eq_top_iff_mem f).1 hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ ⊤ ∈ sieves J Y
[PROOFSTEP]
apply J.top_mem
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Covers J S f
Z : C
g : Z ⟶ Y
⊢ Covers J S (g ≫ f)
[PROOFSTEP]
rw [covers_iff] at h ⊢
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Sieve.pullback f S ∈ sieves J Y
Z : C
g : Z ⟶ Y
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J Z
[PROOFSTEP]
simp [h, Sieve.pullback_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
⊢ (∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g) → Covers J R f
[PROOFSTEP]
intro k
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ Covers J R f
[PROOFSTEP]
apply J.transitive h
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ sieves J Y_1
[PROOFSTEP]
intro Z g hg
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ sieves J Z
[PROOFSTEP]
rw [← Sieve.pullback_comp]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ sieves J Z
[PROOFSTEP]
apply k (g ≫ f) hg
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
hS : Covers J S f
hR : Covers J R f
⊢ Covers J (S ⊓ R) f
[PROOFSTEP]
simpa [covers_iff] using And.intro hS hR
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X => {⊤}) X
⊢ Sieve.pullback f S ∈ (fun X => {⊤}) Y
[PROOFSTEP]
rw [Set.mem_singleton_iff] at hf ⊢
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
f : Y ⟶ X
hf : S = ⊤
⊢ Sieve.pullback f S = ⊤
[PROOFSTEP]
simp [hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ (fun X => {⊤}) X
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {⊤}) Y
⊢ R ∈ (fun X => {⊤}) X
[PROOFSTEP]
rw [Set.mem_singleton_iff, ← Sieve.id_mem_iff_eq_top] at hS 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S.arrows (𝟙 X)
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {⊤}) Y
⊢ R ∈ (fun X => {⊤}) X
[PROOFSTEP]
simpa using hR hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ (X : C), ⊤ ∈ (fun X => Set.univ) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S R : Sieve X✝
J : GrothendieckTopology C
X Y : C
f : Sieve X
⊢ ∀ (f_1 : Y ⟶ X), f ∈ (fun X => Set.univ) X → Sieve.pullback f_1 f ∈ (fun X => Set.univ) Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X => Set.univ) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => Set.univ) Y) → R ∈ (fun X => Set.univ) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
T : Set (GrothendieckTopology C)
⊢ ∀ (X : C), ⊤ ∈ sInf (sieves '' T) X
[PROOFSTEP]
rintro X S ⟨⟨_, J, hJ, rfl⟩, rfl⟩
[GOAL]
case intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X : C
J : GrothendieckTopology C
hJ : J ∈ T
⊢ ⊤ ∈ (fun f => ↑f X) { val := J.sieves, property := (_ : ∃ a, a ∈ T ∧ a.sieves = J.sieves) }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
T : Set (GrothendieckTopology C)
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sInf (sieves '' T) X → Sieve.pullback f S ∈ sInf (sieves '' T) Y
[PROOFSTEP]
rintro X Y S hS f _ ⟨⟨_, J, hJ, rfl⟩, rfl⟩
[GOAL]
case intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X Y : C
S : Sieve X
hS : Y ⟶ X
f : S ∈ sInf (sieves '' T) X
J : GrothendieckTopology C
hJ : J ∈ T
⊢ Sieve.pullback hS S ∈ (fun f => ↑f Y) { val := J.sieves, property := (_ : ∃ a, a ∈ T ∧ a.sieves = J.sieves) }
[PROOFSTEP]
apply J.pullback_stable _ (f _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
T : Set (GrothendieckTopology C)
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sInf (sieves '' T) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sInf (sieves '' T) Y) → R ∈ sInf (sieves '' T) X
[PROOFSTEP]
rintro X S hS R h _ ⟨⟨_, J, hJ, rfl⟩, rfl⟩
[GOAL]
case intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X : C
S : Sieve X
hS : S ∈ sInf (sieves '' T) X
R : Sieve X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sInf (sieves '' T) Y
J : GrothendieckTopology C
hJ : J ∈ T
⊢ R ∈ (fun f => ↑f X) { val := J.sieves, property := (_ : ∃ a, a ∈ T ∧ a.sieves = J.sieves) }
[PROOFSTEP]
apply J.transitive (hS _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩) _ fun Y f hf => h hf _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ IsGLB s (sInf s)
[PROOFSTEP]
refine' @IsGLB.of_image _ _ _ _ sieves _ _ _ _
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
x✝ y✝ : GrothendieckTopology C
⊢ x✝.sieves ≤ y✝.sieves ↔ x✝ ≤ y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves
[PROOFSTEP]
exact _root_.isGLB_sInf _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C = ⊤
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C ≤ ⊤
[PROOFSTEP]
exact @CompleteLattice.le_top _ (completeLatticeOfInf _ isGLB_sInf) (discrete C)
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊤ ≤ discrete C
[PROOFSTEP]
intro X S _
[GOAL]
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 ∈ sieves ⊤ X
⊢ S ∈ sieves (discrete C) X
[PROOFSTEP]
apply Set.mem_univ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ trivial C = ⊥
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ trivial C ≤ ⊥
[PROOFSTEP]
intro X S hS
[GOAL]
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
hS : S ∈ sieves (trivial C) X
⊢ S ∈ sieves ⊥ X
[PROOFSTEP]
rw [trivial_covering] at hS 
[GOAL]
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
hS : S = ⊤
⊢ S ∈ sieves ⊥ X
[PROOFSTEP]
apply covering_of_eq_top _ hS
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊥ ≤ trivial C
[PROOFSTEP]
refine' @CompleteLattice.bot_le _ (completeLatticeOfInf _ isGLB_sInf) (trivial C)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Sieve X
f : Y ⟶ X
⊢ Covers ⊥ S f ↔ S.arrows f
[PROOFSTEP]
rw [covers_iff, bot_covering, ← Sieve.pullback_eq_top_iff_mem]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Sieve X
f : Y ⟶ X
⊢ Covers ⊤ S f
[PROOFSTEP]
simp [covers_iff]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X →
      Sieve.pullback f S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
[PROOFSTEP]
intro X Y S h H Z f
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
Z : C
f : Z ⟶ Y
⊢ ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)
[PROOFSTEP]
rcases H (f ≫ h) with ⟨W, g, H'⟩
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)
[PROOFSTEP]
exact ⟨W, g, by simpa⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ (Sieve.pullback h S).arrows (g ≫ f)
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
            S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y) →
          R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
[PROOFSTEP]
intro X S H₁ R H₂ Y f
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
⊢ ∃ Z g, R.arrows (g ≫ f)
[PROOFSTEP]
rcases H₁ f with ⟨Z, g, H₃⟩
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
⊢ ∃ Z g, R.arrows (g ≫ f)
[PROOFSTEP]
rcases H₂ H₃ (𝟙 Z) with ⟨W, h, H₄⟩
[GOAL]
case intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ ∃ Z g, R.arrows (g ≫ f)
[PROOFSTEP]
exact ⟨W, h ≫ g, by simpa using H₄⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ R.arrows ((h ≫ g) ≫ f)
[PROOFSTEP]
simpa using H₄
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
hro : RightOreCondition C
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ (fun X S => ∃ Y f, S.arrows f) X → Sieve.pullback f S ∈ (fun X S => ∃ Y f, S.arrows f) Y
[PROOFSTEP]
rintro X Y S h ⟨Z, f, hf⟩
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
⊢ Sieve.pullback h S ∈ (fun X S => ∃ Y f, S.arrows f) Y
[PROOFSTEP]
rcases hro h f with ⟨W, g, k, comm⟩
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ Sieve.pullback h S ∈ (fun X S => ∃ Y f, S.arrows f) Y
[PROOFSTEP]
refine' ⟨_, g, _⟩
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ (Sieve.pullback h S).arrows g
[PROOFSTEP]
simp [comm, hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
hro : RightOreCondition C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X S => ∃ Y f, S.arrows f) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ Y f, S.arrows f) Y) →
          R ∈ (fun X S => ∃ Y f, S.arrows f) X
[PROOFSTEP]
rintro X S ⟨Y, f, hf⟩ R h
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X : C
S : Sieve X
Y : C
f : Y ⟶ X
hf : S.arrows f
R : Sieve X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ Y f, S.arrows f) Y
⊢ R ∈ (fun X S => ∃ Y f, S.arrows f) X
[PROOFSTEP]
rcases h hf with ⟨Z, g, hg⟩
[GOAL]
case intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X : C
S : Sieve X
Y : C
f : Y ⟶ X
hf : S.arrows f
R : Sieve X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ Y f, S.arrows f) Y
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ R ∈ (fun X S => ∃ Y f, S.arrows f) X
[PROOFSTEP]
exact ⟨_, _, hg⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
src✝ : Preorder (Cover J X) := inferInstance
S : Cover J X
Y : C
f : Y ⟶ X
x✝ : ((fun a => ↑a) S).arrows f
⊢ ((fun a => ↑a) ⊤).arrows f
[PROOFSTEP]
tauto
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
src✝ : Preorder (Cover J X) := inferInstance
S T : Cover J X
h1 : S ≤ T
h2 : T ≤ S
Y : C
f : Y ⟶ X
⊢ (sieve S).arrows f → (sieve T).arrows f
[PROOFSTEP]
apply h1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
src✝ : Preorder (Cover J X) := inferInstance
S T : Cover J X
h1 : S ≤ T
h2 : T ≤ S
Y : C
f : Y ⟶ X
⊢ (sieve T).arrows f → (sieve S).arrows f
[PROOFSTEP]
apply h2
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Cover J X
I : Relation (pullback S f)
⊢ I.g₁ ≫ I.f₁ ≫ f = I.g₂ ≫ I.f₂ ≫ f
[PROOFSTEP]
simp [reassoc_of% I.w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Cover J X
Y : C
f : Y ⟶ X
⊢ (sieve (pullback S (𝟙 X))).arrows f ↔ (sieve S).arrows f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝¹ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y✝ Z : C
S : Cover J X
f✝ : Z ⟶ Y✝
g : Y✝ ⟶ X
Y : C
f : Y ⟶ Z
⊢ (sieve (pullback S (f✝ ≫ g))).arrows f ↔ (sieve (pullback (pullback S g) f✝)).arrows f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
⊢ bind S T ≤ S
[PROOFSTEP]
rintro Y f ⟨Z, e1, e2, h1, _, h3⟩
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (sieve S).arrows e2
left✝ : ((fun Y f hf => sieve (T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ ((fun a => ↑a) S).arrows f
[PROOFSTEP]
rw [← h3]
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (sieve S).arrows e2
left✝ : ((fun Y f hf => sieve (T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ ((fun a => ↑a) S).arrows (e1 ≫ e2)
[PROOFSTEP]
apply Sieve.downward_closed
[GOAL]
case intro.intro.intro.intro.intro.x
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (sieve S).arrows e2
left✝ : ((fun Y f hf => sieve (T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ ((fun a => ↑a) S).arrows e2
[PROOFSTEP]
exact h1
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
⊢ ∀ (b : (index S P).R),
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) b) ≫ Limits.MulticospanIndex.fst (index S P) b =
      (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) b) ≫ Limits.MulticospanIndex.snd (index S P) b
[PROOFSTEP]
intro I
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
I : (index S P).R
⊢ (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) I) ≫ Limits.MulticospanIndex.fst (index S P) I =
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) I) ≫ Limits.MulticospanIndex.snd (index S P) I
[PROOFSTEP]
dsimp [index]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
I : (index S P).R
⊢ P.map I.f₁.op ≫ P.map I.g₁.op = P.map I.f₂.op ≫ P.map I.g₂.op
[PROOFSTEP]
simp only [← P.map_comp, ← op_comp, I.w]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (index S P)
⊢ ∀ (b : (index S P).R),
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) b) ≫ Limits.MulticospanIndex.fst (index S P) b =
      (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) b) ≫ Limits.MulticospanIndex.snd (index S P) b
[PROOFSTEP]
intro I
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (index S P)
I : (index S P).R
⊢ (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) I) ≫ Limits.MulticospanIndex.fst (index S P) I =
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) I) ≫ Limits.MulticospanIndex.snd (index S P) I
[PROOFSTEP]
dsimp only [index, Relation.fst, Relation.snd]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (index S P)
I : (index S P).R
⊢ P.map I.f₁.op ≫ P.map I.g₁.op = P.map I.f₂.op ≫ P.map I.g₂.op
[PROOFSTEP]
simp only [← P.map_comp, ← op_comp, I.w]
