Theorem: le_generateFrom_iff_subset_isOpen (LeanCourse/Lectures/Lecture7.lean)

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
⊢ {s | IsOpen s} ⊆ {s | IsOpen s}
Tactic:
intro s hs
State after:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ s ∈ {s | IsOpen s}

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ s ∈ {s | IsOpen s}
Tactic:
simp
State after:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ IsOpen s

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ IsOpen s
Tactic:
simp at hs
State after:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : IsOpen s
⊢ IsOpen s

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : IsOpen s
⊢ IsOpen s
Tactic:
induction hs
State after:
case basic
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s s✝ : Set α
a✝ : s✝ ∈ g
⊢ IsOpen s✝

case univ
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
⊢ IsOpen Set.univ

case inter
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : IsOpen s✝
a_ih✝ : IsOpen t✝
⊢ IsOpen (s✝ ∩ t✝)

case sUnion
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen g s
a_ih✝ : ∀ s ∈ S✝, IsOpen s
⊢ IsOpen (⋃₀ S✝)

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ IsOpen s
Tactic:
case basic s hs =>
  apply h
  exact hs
State after:
no goals

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
⊢ IsOpen Set.univ
Tactic:
case univ =>
  simp
State after:
no goals

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen (s ∩ s')
Tactic:
case inter s s' _ _ ihs ihs' =>
  apply IsOpen.inter
  exact ihs
  exact ihs'
State after:
no goals

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋃₀ S)
Tactic:
case sUnion S _ hS =>
  apply isOpen_sUnion
  exact hS
State after:
no goals

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ IsOpen s
Tactic:
apply h
State after:
case a
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ s ∈ g

State before:
case a
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ s ∈ g
Tactic:
exact hs
State after:
no goals

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
⊢ IsOpen Set.univ
Tactic:
simp
State after:
no goals

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen (s ∩ s')
Tactic:
apply IsOpen.inter
State after:
case h₁
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s

case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'

State before:
case h₁
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s

case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'
Tactic:
exact ihs
State after:
case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'

State before:
case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'
Tactic:
exact ihs'
State after:
no goals

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋃₀ S)
Tactic:
apply isOpen_sUnion
State after:
case h
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ ∀ t_1 ∈ S, IsOpen t_1

State before:
case h
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ ∀ t_1 ∈ S, IsOpen t_1
Tactic:
exact hS
State after:
no goals