-- Mathlib/Topology/Sets/Opens.lean
theorem isBasis_iff_cover {B : Set (Opens α)} :
    IsBasis B ↔ ∀ U : Opens α, ∃ Us, Us ⊆ B ∧ U = sSup Us

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ (∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us) → IsBasis B

Proof state:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⋃₀ {s | s ∈ SetLike.coe '' B ∧ s ⊆ ↑U} = ⋃ i ∈ {V | V ∈ B ∧ V ≤ U}, ↑i

Tactic:
simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]

Result:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⨆ b ∈ B, ⨆ (_ : ↑b ⊆ ↑U), ↑b = ⨆ i ∈ B, ⨆ (_ : i ≤ U), ↑i

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us✝ : Set (Opens α)
hUs : Us✝ ⊆ B
hx : x ∈ sSup Us✝
U : Opens α
Us : U ∈ Us✝
xU : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us✝

Tactic:
exact ⟨U, hUs Us, xU, le_sSup Us⟩

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us : Set (Opens α)
hUs : Us ⊆ B
hx : x ∈ sSup Us
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us

Tactic:
rcases mem_sSup.1 hx with ⟨U, Us, xU⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us✝ : Set (Opens α)
hUs : Us✝ ⊆ B
hx : x ∈ sSup Us✝
U : Opens α
Us : U ∈ Us✝
xU : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us✝

Proof state:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

Tactic:
intro hB U

Result:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us ⊆ B, U = sSup Us

Proof state:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us ⊆ B, U = sSup Us

Tactic:
refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩

Result:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})

Proof state:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
x : α
hx : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
rcases h U with ⟨Us, hUs, rfl⟩

Result:
case mpr.intro.intro
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us : Set (Opens α)
hUs : Us ⊆ B
hx : x ∈ sSup Us
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us

Proof state:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
intro U x hx

Result:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
x : α
hx : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Proof state:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⨆ b ∈ B, ⨆ (_ : ↑b ⊆ ↑U), ↑b = ⨆ i ∈ B, ⨆ (_ : i ≤ U), ↑i

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ (∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us) → IsBasis B

Tactic:
intro h

Result:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ IsBasis B

Proof state:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})

Tactic:
rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]

Result:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⋃₀ {s | s ∈ SetLike.coe '' B ∧ s ⊆ ↑U} = ⋃ i ∈ {V | V ∈ B ∧ V ≤ U}, ↑i

Proof state:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ IsBasis B

Tactic:
rw [isBasis_iff_nbhd]

Result:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U