-- Mathlib/Topology/Order/LowerUpperTopology.lean
lemma isTopologicalSpace_basis (U : Set α) : IsOpen U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Proof state:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ ⋂₀ (compl '' S)
c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
⊢ c ≤ b

Tactic:
simp only [sInter_image, mem_iInter] at hb

Result:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
hb : ∀ i ∈ S, b ∈ iᶜ
⊢ c ≤ b

Proof state:
case pos
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : U = univ
⊢ IsOpen U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
simp only [hU, isOpen_univ, compl_Ici, true_or]

Result:
no goals

Proof state:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
hb : ∀ i ∈ S, b ∈ iᶜ
⊢ c ≤ b

Tactic:
rw [← not_lt, ← mem_Iio, ← compl_Ici]

Result:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
hb : ∀ i ∈ S, b ∈ iᶜ
⊢ b ∉ (Ici c)ᶜ

Proof state:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ Ici (sSup {a | (Ici a)ᶜ ∈ S}) ≤ ⋂₀ (compl '' S)

Tactic:
intro b hb

Result:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
⊢ b ∈ ⋂₀ (compl '' S)

Proof state:
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
a : α
ha : (Ici a)ᶜ = U
⊢ U ∈ {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
use a

Result:
no goals

Proof state:
case h.a.intro
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
s : Set α
hs : s ∈ S
a : α
ha : (Ici a)ᶜ = s
⊢ b ∉ s

Tactic:
subst hS2 ha

Result:
case h.a.intro
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hUS : univ ∉ S
b : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
a : α
hU : ¬⋃₀ S = univ
hO : IsOpen (⋃₀ S)
hs : (Ici a)ᶜ ∈ S
⊢ b ∉ (Ici a)ᶜ

Proof state:
case h
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ Ici (sSup {a | (Ici a)ᶜ ∈ S}) = ⋂₀ (compl '' S)

Tactic:
apply le_antisymm

Result:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ Ici (sSup {a | (Ici a)ᶜ ∈ S}) ≤ ⋂₀ (compl '' S)

case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ ⋂₀ (compl '' S) ≤ Ici (sSup {a | (Ici a)ᶜ ∈ S})

Proof state:
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ U = univ

Tactic:
rw [hS2]

Result:
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ ⋃₀ S = univ

Proof state:
case h.right
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
a : α
ha : (Ici a)ᶜ = U
⊢ U = ⋃₀ {U}

Tactic:
rw [sUnion_singleton]

Result:
no goals

Proof state:
case h.a.intro
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hUS : univ ∉ S
b : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
a : α
hU : ¬⋃₀ S = univ
hO : IsOpen (⋃₀ S)
hs : (Ici a)ᶜ ∈ S
⊢ b ∉ (Ici a)ᶜ

Tactic:
simp_all only [compl_Ici, mem_Ici, sSup_le_iff, mem_setOf_eq, mem_Iio, not_lt]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ ⋃₀ S = univ

Tactic:
exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)

Result:
no goals

Proof state:
case neg.h
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ ∃ a, (Ici a)ᶜ = U

Tactic:
convert IsTopologicalBasis.open_eq_sUnion isTopologicalBasis_insert_univ_subbasis hO

Result:
case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ (∃ a, (Ici a)ᶜ = U) ↔ ∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S

Proof state:
case a.mpr
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ ∃ a, (Ici a)ᶜ = U

Tactic:
use sSup {a | (Ici a)ᶜ ∈ S}

Result:
case h
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ (Ici (sSup {a | (Ici a)ᶜ ∈ S}))ᶜ = U

Proof state:
case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ (∃ a, (Ici a)ᶜ = U) ↔ ∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S

Tactic:
constructor

Result:
case a.mp
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ (∃ a, (Ici a)ᶜ = U) → ∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S

case a.mpr
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ (∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S) → ∃ a, (Ici a)ᶜ = U

Proof state:
case neg
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
apply Or.inr

Result:
case neg.h
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ ∃ a, (Ici a)ᶜ = U