-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem coverDense_iff_isBasis [Category ι] (B : ι ⥤ Opens X) :
    B.IsCoverDense (Opens.grothendieckTopology X) ↔ Opens.IsBasis (Set.range B.obj)

Proof state:
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔ Opens.IsBasis (Set.range B.obj)

Tactic:
rw [Opens.isBasis_iff_nbhd]

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

Proof state:
case mpr.is_cover
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ (Opens.grothendieckTopology ↑X) U

Tactic:
intro U x hx

Result:
case mpr.is_cover
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ 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

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

Tactic:
intro hb

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

Proof state:
case mpr.is_cover
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ 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

Tactic:
rcases hb hx with ⟨_, ⟨i, rfl⟩, hx, hi⟩

Result:
case mpr.is_cover.intro.intro.intro.intro
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ 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

Proof state:
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
constructor

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

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

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

Tactic:
rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩

Result:
case mp.intro.intro.intro.intro.mk
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
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' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Proof state:
case mp.intro.intro.intro.intro.mk
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
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' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩

Result:
no goals

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

Tactic:
constructor

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

Proof state:
case mpr.is_cover.intro.intro.intro.intro
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ 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

Tactic:
exact ⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩

Result:
no goals

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

Tactic:
intro hd U x hx

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