[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
hS : IsClosed J₁ S
Z : C
g : Z ⟶ Y
hg : Covers J₁ (Sieve.pullback f S) g
⊢ Covers J₁ S (g ≫ f)
[PROOFSTEP]
rwa [J₁.covers_iff, Sieve.pullback_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ IsClosed J₁ S ↔ close J₁ S = S
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ IsClosed J₁ S → close J₁ S = S
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S = S
[PROOFSTEP]
apply le_antisymm
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S ≤ S
[PROOFSTEP]
intro Y f hf
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ S.arrows f
[PROOFSTEP]
rw [← J₁.covers_iff_mem_of_isClosed h]
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ Covers J₁ S f
[PROOFSTEP]
apply hf
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ S ≤ close J₁ S
[PROOFSTEP]
apply J₁.le_close
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = S → IsClosed J₁ S
[PROOFSTEP]
intro e
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ S
[PROOFSTEP]
rw [← e]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ (close J₁ S)
[PROOFSTEP]
apply J₁.close_isClosed
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ close J₁ (Sieve.pullback f S) = Sieve.pullback f (close J₁ S)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ close J₁ (Sieve.pullback f S) ≤ Sieve.pullback f (close J₁ S)
[PROOFSTEP]
refine' J₁.le_close_of_isClosed (Sieve.pullback_monotone _ (J₁.le_close S)) _
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ IsClosed J₁ (Sieve.pullback f (close J₁ S))
[PROOFSTEP]
apply J₁.isClosed_pullback _ _ (J₁.close_isClosed _)
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (close J₁ S) ≤ close J₁ (Sieve.pullback f S)
[PROOFSTEP]
intro Z g hg
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ (close J₁ (Sieve.pullback f S)).arrows g
[PROOFSTEP]
change _ ∈ J₁ _
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ sieves J₁ Z
[PROOFSTEP]
rw [← Sieve.pullback_comp]
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J₁ Z
[PROOFSTEP]
apply hg
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = ⊤ ↔ S ∈ sieves J₁ X
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = ⊤ → S ∈ sieves J₁ X
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ S ∈ sieves J₁ X
[PROOFSTEP]
apply J₁.transitive (J₁.top_mem X)
[GOAL]
case mp.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⊤.arrows f → Sieve.pullback f S ∈ sieves J₁ Y
[PROOFSTEP]
intro Y f hf
[GOAL]
case mp.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ Sieve.pullback f S ∈ sieves J₁ Y
[PROOFSTEP]
change J₁.close S f
[GOAL]
case mp.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ (close J₁ S).arrows f
[PROOFSTEP]
rwa [h]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ sieves J₁ X → close J₁ S = ⊤
[PROOFSTEP]
intro hS
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ close J₁ S = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ ⊤ ≤ close J₁ S
[PROOFSTEP]
intro Y f _
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : ⊤.arrows f
⊢ (close J₁ S).arrows f
[PROOFSTEP]
apply J₁.pullback_stable _ hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁)
[PROOFSTEP]
intro X S hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₁) S.arrows
[PROOFSTEP]
rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
      Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows
[PROOFSTEP]
rintro x ⟨M, hM⟩ ⟨N, hN⟩ hM₂ hN₂
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
[PROOFSTEP]
simp only [Functor.closedSieves_obj]
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
[PROOFSTEP]
ext Y f
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
⊢ (↑{ val := M, property := hM }).arrows f ↔ (↑{ val := N, property := hN }).arrows f
[PROOFSTEP]
dsimp only [Subtype.coe_mk]
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
⊢ M.arrows f ↔ N.arrows f
[PROOFSTEP]
rw [← J₁.covers_iff_mem_of_isClosed hM, ← J₁.covers_iff_mem_of_isClosed hN]
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
have q : ∀ ⦃Z : C⦄ (g : Z ⟶ X) (_ : S g), M.pullback g = N.pullback g := fun Z g hg =>
  congr_arg Subtype.val ((hM₂ g hg).trans (hN₂ g hg).symm)
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
have MSNS : M ⊓ S = N ⊓ S := by
  ext Z g
  rw [Sieve.inter_apply, Sieve.inter_apply]
  simp only [and_comm]
  apply and_congr_right
  intro hg
  rw [Sieve.pullback_eq_top_iff_mem, Sieve.pullback_eq_top_iff_mem, q g hg]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ M ⊓ S = N ⊓ S
[PROOFSTEP]
ext Z g
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ (M ⊓ S).arrows g ↔ (N ⊓ S).arrows g
[PROOFSTEP]
rw [Sieve.inter_apply, Sieve.inter_apply]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ M.arrows g ∧ S.arrows g ↔ N.arrows g ∧ S.arrows g
[PROOFSTEP]
simp only [and_comm]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ S.arrows g ∧ M.arrows g ↔ S.arrows g ∧ N.arrows g
[PROOFSTEP]
apply and_congr_right
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ S.arrows g → (M.arrows g ↔ N.arrows g)
[PROOFSTEP]
intro hg
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
hg : S.arrows g
⊢ M.arrows g ↔ N.arrows g
[PROOFSTEP]
rw [Sieve.pullback_eq_top_iff_mem, Sieve.pullback_eq_top_iff_mem, q g hg]
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
constructor
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f → GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
intro hf
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
rw [J₁.covers_iff]
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f N ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (N ⊓ ?m.20423) ∈ GrothendieckTopology.sieves J₁ Y
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve (Opposite.op X).unop
[PROOFSTEP]
rw [← MSNS]
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (M ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.arrow_intersect f M S hf (J₁.pullback_stable _ hS)
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ N f → GrothendieckTopology.Covers J₁ M f
[PROOFSTEP]
intro hf
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ GrothendieckTopology.Covers J₁ M f
[PROOFSTEP]
rw [J₁.covers_iff]
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f M ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (M ⊓ ?m.20633) ∈ GrothendieckTopology.sieves J₁ Y
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve (Opposite.op X).unop
[PROOFSTEP]
rw [MSNS]
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (N ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.arrow_intersect f N S hf (J₁.pullback_stable _ hS)
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
    Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
rw [Presieve.compatible_iff_sieveCompatible] at hx 
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let M := Sieve.bind S fun Y f hf => (x f hf).1
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have : ∀ ⦃Y⦄ (f : Y ⟶ X) (hf : S f), M.pullback f = (x f hf).1 :=
  by
  intro Y f hf
  apply le_antisymm
  · rintro Z u ⟨W, g, f', hf', hg : (x f' hf').1 _, c⟩
    rw [Sieve.pullback_eq_top_iff_mem, ←
      show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]
    conv_lhs => congr; congr;
      rw [← c]
        -- Porting note: Originally `simp_rw [← c]`
    rw [show (x (g ≫ f') _).1 = _ from congr_arg Subtype.val (hx f' g hf')]
    apply Sieve.pullback_eq_top_of_mem _ hg
  · apply Sieve.le_pullback_bind S fun Y f hf => (x f hf).1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
[PROOFSTEP]
intro Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M = ↑(x f hf)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M ≤ ↑(x f hf)
[PROOFSTEP]
rintro Z u ⟨W, g, f', hf', hg : (x f' hf').1 _, c⟩
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ (↑(x f hf)).arrows u
[PROOFSTEP]
rw [Sieve.pullback_eq_top_iff_mem, ←
  show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑(x (u ≫ f) (_ : S.arrows (u ≫ f))) = ⊤
[PROOFSTEP]
conv_lhs => congr; congr;
  rw [← c]
    -- Porting note: Originally `simp_rw [← c]`
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| ↑(x (u ≫ f) (_ : S.arrows (u ≫ f)))
[PROOFSTEP]
congr; congr;
  rw [← c]
    -- Porting note: Originally `simp_rw [← c]`
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| ↑(x (u ≫ f) (_ : S.arrows (u ≫ f)))
[PROOFSTEP]
congr; congr;
  rw [← c]
    -- Porting note: Originally `simp_rw [← c]`
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| ↑(x (u ≫ f) (_ : S.arrows (u ≫ f)))
[PROOFSTEP]
congr
[GOAL]
case self
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| x (u ≫ f) (_ : S.arrows (u ≫ f))
[PROOFSTEP]
congr
[GOAL]
case self.f
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| u ≫ f
[PROOFSTEP]
rw [← c]
  -- Porting note: Originally `simp_rw [← c]`
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑(x (g ≫ f') (_ : S.arrows (g ≫ f'))) = ⊤
[PROOFSTEP]
rw [show (x (g ≫ f') _).1 = _ from congr_arg Subtype.val (hx f' g hf')]
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑((Functor.closedSieves J₁).map g.op (x f' hf')) = ⊤
[PROOFSTEP]
apply Sieve.pullback_eq_top_of_mem _ hg
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(x f hf) ≤ Sieve.pullback f M
[PROOFSTEP]
apply Sieve.le_pullback_bind S fun Y f hf => (x f hf).1
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine' ⟨⟨_, J₁.close_isClosed M⟩, _⟩
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ Presieve.FamilyOfElements.IsAmalgamation x
    { val := GrothendieckTopology.close J₁ M,
      property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }
[PROOFSTEP]
intro Y f hf
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₁).map f.op
      { val := GrothendieckTopology.close J₁ M,
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
[PROOFSTEP]
simp only [Functor.closedSieves_obj]
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₁).map f.op
      { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
[PROOFSTEP]
ext1
[GOAL]
case refine'_2.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₁).map f.op
        { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
          property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }) =
    ↑(x f hf)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf))) = ↑(x f hf)
[PROOFSTEP]
rw [← J₁.pullback_close, this _ hf]
[GOAL]
case refine'_2.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ GrothendieckTopology.close J₁ ↑(x f hf) = ↑(x f hf)
[PROOFSTEP]
apply le_antisymm (J₁.le_close_of_isClosed le_rfl (x f hf).2) (J₁.le_close _)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
⊢ J₁ ≤ J₂
[PROOFSTEP]
intro X S hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ S ∈ GrothendieckTopology.sieves J₂ X
[PROOFSTEP]
rw [← J₂.close_eq_top_iff_mem]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
have : J₂.IsClosed (⊤ : Sieve X) := by
  intro Y f _
  trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ GrothendieckTopology.IsClosed J₂ ⊤
[PROOFSTEP]
intro Y f _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : GrothendieckTopology.Covers J₂ ⊤ f
⊢ ⊤.arrows f
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
suffices (⟨J₂.close S, J₂.close_isClosed S⟩ : Subtype _) = ⟨⊤, this⟩
  by
  rw [Subtype.ext_iff] at this 
  exact this
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this✝ : GrothendieckTopology.IsClosed J₂ ⊤
this :
  { val := GrothendieckTopology.close J₂ S,
      property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    { val := ⊤, property := this✝ }
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
rw [Subtype.ext_iff] at this 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this✝ : GrothendieckTopology.IsClosed J₂ ⊤
this :
  ↑{ val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    ↑{ val := ⊤, property := this✝ }
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
exact this
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ { val := GrothendieckTopology.close J₂ S,
      property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    { val := ⊤, property := this }
[PROOFSTEP]
apply (h S hS).isSeparatedFor.ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      (Functor.closedSieves J₂).map f.op
          { val := GrothendieckTopology.close J₂ S,
            property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
        (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
[PROOFSTEP]
intro Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
[PROOFSTEP]
simp only [Functor.closedSieves_obj]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
[PROOFSTEP]
ext1
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₂).map f.op
        { val := GrothendieckTopology.close J₂ S,
          property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) }) =
    ↑((Functor.closedSieves J₂).map f.op { val := ⊤, property := this })
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (GrothendieckTopology.close J₂ S) = Sieve.pullback f ⊤
[PROOFSTEP]
rw [Sieve.pullback_top, ← J₂.pullback_close, S.pullback_eq_top_of_mem hf, J₂.close_eq_top_iff_mem]
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ∈ GrothendieckTopology.sieves J₂ Y
[PROOFSTEP]
apply J₂.top_mem
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ ↔ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂ J₁ : GrothendieckTopology C
⊢ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
[PROOFSTEP]
intro P
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂ J₁ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type (max v u)
⊢ Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
[PROOFSTEP]
rfl
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ = J₂
[PROOFSTEP]
apply le_antisymm
[GOAL]
case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂
[PROOFSTEP]
apply le_topology_of_closedSieves_isSheaf
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
[PROOFSTEP]
rw [h]
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₂)
[PROOFSTEP]
apply classifier_isSheaf
[GOAL]
case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁
[PROOFSTEP]
apply le_topology_of_closedSieves_isSheaf
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₁)
[PROOFSTEP]
rw [← h]
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁)
[PROOFSTEP]
apply classifier_isSheaf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X => {S | ↑(c X) S = ⊤}) X
⊢ Sieve.pullback f S ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
[PROOFSTEP]
rw [Set.mem_setOf_eq] at hS 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X Y : C
S : Sieve X
f : Y ⟶ X
hS : ↑(c X) S = ⊤
⊢ Sieve.pullback f S ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
[PROOFSTEP]
rw [Set.mem_setOf_eq, hc, hS, Sieve.pullback_top]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : S ∈ (fun X => {S | ↑(c X) S = ⊤}) X
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ R ∈ (fun X => {S | ↑(c X) S = ⊤}) X
[PROOFSTEP]
rw [Set.mem_setOf_eq] at hS 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ R ∈ (fun X => {S | ↑(c X) S = ⊤}) X
[PROOFSTEP]
rw [Set.mem_setOf_eq, ← (c X).idempotent, eq_top_iff, ← hS]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ ↑(c X) S ≤ ↑(c X) (↑(c X) R)
[PROOFSTEP]
apply (c X).monotone fun Y f hf => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ ∀ (Y : C) (f : Y ⟶ X), S.arrows f → (↑(c X) R).arrows f
[PROOFSTEP]
intros Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (↑(c X) R).arrows f
[PROOFSTEP]
rw [Sieve.pullback_eq_top_iff_mem, ← hc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(c Y) (Sieve.pullback f R) = ⊤
[PROOFSTEP]
apply hR hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ topologyOfClosureOperator (GrothendieckTopology.closureOperator J₁)
      (_ :
        ∀ (X Y : C) (f : Y ⟶ X) (S : Sieve X),
          GrothendieckTopology.close J₁ (Sieve.pullback f S) = Sieve.pullback f (GrothendieckTopology.close J₁ S)) =
    J₁
[PROOFSTEP]
ext X S
[GOAL]
case h.h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈
      GrothendieckTopology.sieves
        (topologyOfClosureOperator (GrothendieckTopology.closureOperator J₁)
          (_ :
            ∀ (X Y : C) (f : Y ⟶ X) (S : Sieve X),
              GrothendieckTopology.close J₁ (Sieve.pullback f S) = Sieve.pullback f (GrothendieckTopology.close J₁ S)))
        X ↔
    S ∈ GrothendieckTopology.sieves J₁ X
[PROOFSTEP]
apply GrothendieckTopology.close_eq_top_iff_mem
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
⊢ GrothendieckTopology.close (topologyOfClosureOperator c pb) S = ↑(c X) S
[PROOFSTEP]
ext Y f
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ (GrothendieckTopology.close (topologyOfClosureOperator c pb) S).arrows f ↔ (↑(c X) S).arrows f
[PROOFSTEP]
change c _ (Sieve.pullback f S) = ⊤ ↔ c _ S f
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ↑(c Y) (Sieve.pullback f S) = ⊤ ↔ (↑(c X) S).arrows f
[PROOFSTEP]
rw [pb, Sieve.pullback_eq_top_iff_mem]
