[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
y : T
hy : y ∈ Y
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
[PROOFSTEP]
rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
[PROOFSTEP]
refine' ⟨U ⊓ Y, homOfLE inf_le_right, _, hU, hy⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ (Sieve.pullback f S).arrows (homOfLE (_ : U ⊓ Y ≤ Y))
[PROOFSTEP]
apply S.downward_closed hg (homOfLE inf_le_left)
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) Y
x : T
hx : x ∈ X
⊢ ∃ U f, R.arrows f ∧ x ∈ U
[PROOFSTEP]
rcases hS x hx with ⟨U, f, hf, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
⊢ ∃ U f, R.arrows f ∧ x ∈ U
[PROOFSTEP]
rcases hR hf _ hU with ⟨V, g, hg, hV⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) X
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ (x : T), x ∈ X → ∃ U f, S.arrows f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : (Sieve.pullback f R).arrows g
hV : x ∈ V
⊢ ∃ U f, R.arrows f ∧ x ∈ U
[PROOFSTEP]
exact ⟨_, g ≫ f, hg, hV⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
⊢ ∃ U f_1, Presieve.pullbackArrows f S f_1 ∧ x ∈ U
[PROOFSTEP]
rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ ∃ U f_1, Presieve.pullbackArrows f S f_1 ∧ x ∈ U
[PROOFSTEP]
refine' ⟨_, _, Presieve.pullbackArrows.mk _ _ hg, _⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ x ∈ pullback g f
[PROOFSTEP]
have : U ⊓ Y ≤ pullback g f
[GOAL]
case this
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ U ⊓ Y ≤ pullback g f
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
this : U ⊓ Y ≤ pullback g f
⊢ x ∈ pullback g f
[PROOFSTEP]
refine' leOfHom (pullback.lift (homOfLE inf_le_left) (homOfLE inf_le_right) rfl)
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
this : U ⊓ Y ≤ pullback g f
⊢ x ∈ pullback g f
[PROOFSTEP]
apply this ⟨hU, hx⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) Y
x : T
hx : x ∈ X
⊢ ∃ U f, Presieve.bind S Ti f ∧ x ∈ U
[PROOFSTEP]
rcases hS x hx with ⟨U, f, hf, hU⟩
[GOAL]
case intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
⊢ ∃ U f, Presieve.bind S Ti f ∧ x ∈ U
[PROOFSTEP]
rcases hTi f hf x hU with ⟨V, g, hg, hV⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) X
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => ∀ (x : T), x ∈ X → ∃ U f, R f ∧ x ∈ U) Y
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : Ti f hf g
hV : x ∈ V
⊢ ∃ U f, Presieve.bind S Ti f ∧ x ∈ U
[PROOFSTEP]
exact ⟨_, _, ⟨_, g, f, hf, hg, rfl⟩, hV⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) = pretopology T
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) ≤ pretopology T
[PROOFSTEP]
intro X R hR x hx
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) X
x : T
hx : x ∈ X
⊢ ∃ U f, R f ∧ x ∈ U
[PROOFSTEP]
rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩
[GOAL]
case a.intro.intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hU : x ∈ U
V : Opens T
g₁ : U ⟶ V
g₂ : V ⟶ X
hg₂ : R g₂
right✝ : g₁ ≫ g₂ = f
⊢ ∃ U f, R f ∧ x ∈ U
[PROOFSTEP]
exact ⟨V, g₂, hg₂, g₁.le hU⟩
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)
[PROOFSTEP]
intro X R hR x hx
[GOAL]
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (pretopology T) X
x : T
hx : x ∈ X
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U
[PROOFSTEP]
rcases hR x hx with ⟨U, f, hf, hU⟩
[GOAL]
case a.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Pretopology.coverings (pretopology T) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : R f
hU : x ∈ U
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U
[PROOFSTEP]
exact ⟨U, f, Sieve.le_generate R U hf, hU⟩
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (pretopology T) = grothendieckTopology T
[PROOFSTEP]
rw [← pretopology_ofGrothendieck]
[GOAL]
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) =
    grothendieckTopology T
[PROOFSTEP]
apply (Pretopology.gi (Opens T)).l_u_eq
