X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B ↔
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B ↔ Opens.IsBasis (Set.range B.obj)
rw [Opens.isBasis_iff_nbhd]
case mp
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B →
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U

case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B ↔
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
constructor
case mp
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U

case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
case mp
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B →
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U

case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
intro hd U x hx
case mp.intro.intro.intro.intro.mk
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
V : Opens ↑X
f : V ⟶ U
hV : x ∈ V
i : ι
f₁ : V ⟶ B.obj i
f₂ : B.obj i ⟶ U
fac✝ : f₁ ≫ f₂ = f
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U

case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
case mp
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U

case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩
case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
case mp.intro.intro.intro.intro.mk
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
V : Opens ↑X
f : V ⟶ U
hV : x ∈ V
i : ι
f₁ : V ⟶ B.obj i
f₂ : B.obj i ⟶ U
fac✝ : f₁ ≫ f₂ = f
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U

case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩
case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ CoverDense (Opens.grothendieckTopology ↑X) B
case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
intro hb
case mpr.is_cover
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
case mpr
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ CoverDense (Opens.grothendieckTopology ↑X) B
constructor
case mpr.is_cover
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
case mpr.is_cover
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
intro U x hx
case mpr.is_cover.intro.intro.intro.intro
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx✝ : x ∈ U
i : ι
hx : x ∈ B.obj i
hi : B.obj i ≤ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
case mpr.is_cover
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
rcases hb hx with ⟨_, ⟨i, rfl⟩, hx, hi⟩
no goals
case mpr.is_cover.intro.intro.intro.intro
X : TopCat
ι : Type u_2
inst✝ : Category ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx✝ : x ∈ U
i : ι
hx : x ∈ B.obj i
hi : B.obj i ≤ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
exact ⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩