case intro.intro.intro
α : Type ?u.161670
β : Type ?u.161673
γ : Type ?u.161676
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → ¬x ∈ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → ¬x ∈ s
⊢ ∃ s, Set.Countable s ∧ Dense s ∧ ¬0 ∈ s ∧ ¬⊤ ∈ s
α : Type ?u.161670
β : Type ?u.161673
γ : Type ?u.161676
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ ∃ s, Set.Countable s ∧ Dense s ∧ ¬0 ∈ s ∧ ¬⊤ ∈ s
obtain ⟨s, s_count, s_dense, hs⟩ :
  ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s :=
  exists_countable_dense_no_bot_top ℝ≥0∞
no goals
case intro.intro.intro
α : Type ?u.161670
β : Type ?u.161673
γ : Type ?u.161676
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → ¬x ∈ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → ¬x ∈ s
⊢ ∃ s, Set.Countable s ∧ Dense s ∧ ¬0 ∈ s ∧ ¬⊤ ∈ s
exact ⟨s, s_count, s_dense, fun h => hs.1 0 (by simp) h, fun h => hs.2 ∞ (by simp) h⟩
no goals
α : Type ?u.161670
β : Type ?u.161673
γ : Type ?u.161676
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → ¬x ∈ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → ¬x ∈ s
h : 0 ∈ s
⊢ IsBot 0
simp
no goals
α : Type ?u.161670
β : Type ?u.161673
γ : Type ?u.161676
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → ¬x ∈ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → ¬x ∈ s
h : ⊤ ∈ s
⊢ IsTop ⊤
simp