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

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

State before:
X : Type
x : ℝ
hx : x ∈ Set.univ
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ Set.univ
Tactic:
use 37
State after:
case h
X : Type
x : ℝ
hx : x ∈ Set.univ
⊢ 37 > 0 ∧ ∀ (y : ℝ), x - 37 < y ∧ y < x + 37 → y ∈ Set.univ

State before:
case h
X : Type
x : ℝ
hx : x ∈ Set.univ
⊢ 37 > 0 ∧ ∀ (y : ℝ), x - 37 < y ∧ y < x + 37 → y ∈ Set.univ
Tactic:
norm_num
State after:
no goals