Theorem: Section10sheet1Solutions.Real.isOpen_sUnion (FormalisingMathematics2024/Solutions/Section10TopologicalSpaces/Sheet1.lean)

State before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
⊢ IsOpen (⋃₀ F)
Tactic:
intro x hx
State after:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : x ∈ ⋃₀ F
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ ⋃₀ F

State before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : x ∈ ⋃₀ F
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ ⋃₀ F
Tactic:
simp_rw [Set.mem_sUnion] at hx ⊢
State after:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : ∃ t ∈ F, x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t

State before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
hx : ∃ t ∈ F, x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
rcases hx with ⟨t, htF, hxt⟩
State after:
case intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t

State before:
case intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
obtain ⟨δ, hδpos, h⟩ := hF t htF x hxt
State after:
case intro.intro.intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t

State before:
case intro.intro.intro.intro
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
use δ, hδpos
State after:
case right
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t

State before:
case right
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
⊢ ∀ (y : ℝ), x - δ < y ∧ y < x + δ → ∃ t ∈ F, y ∈ t
Tactic:
peel h with h1 y hyt
State after:
case right.h.h
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
y : ℝ
hyt : x - δ < y ∧ y < x + δ
h1 : y ∈ t
⊢ ∃ t ∈ F, y ∈ t

State before:
case right.h.h
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
x : ℝ
t : Set ℝ
htF : t ∈ F
hxt : x ∈ t
δ : ℝ
hδpos : δ > 0
h : ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ t
y : ℝ
hyt : x - δ < y ∧ y < x + δ
h1 : y ∈ t
⊢ ∃ t ∈ F, y ∈ t
Tactic:
use t, htF
State after:
no goals