case inl
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : 0 ≠ ⊤
⊢ HasBasis (𝓝 0) (fun x => x ≠ 0) fun ε => Icc (0 - ε) (0 + ε)

case inr
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ HasBasis (𝓝 x) (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
⊢ HasBasis (𝓝 x) (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)
rcases (zero_le x).eq_or_gt with rfl | x0
case inl
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : 0 ≠ ⊤
⊢ HasBasis (𝓝 ⊥) (fun x => ⊥ < x) fun ε => Iic ε
case inl
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : 0 ≠ ⊤
⊢ HasBasis (𝓝 0) (fun x => x ≠ 0) fun ε => Icc (0 - ε) (0 + ε)
simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]
no goals
case inl
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : 0 ≠ ⊤
⊢ HasBasis (𝓝 ⊥) (fun x => ⊥ < x) fun ε => Iic ε
exact nhds_bot_basis_Iic
case inr.refine_1
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.fst < x ∧ x < i.snd → ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.fst i.snd

case inr.refine_2
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ i, (i.fst < x ∧ x < i.snd) ∧ Ioo i.fst i.snd ⊆ Icc (x - ε) (x + ε)
case inr
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ HasBasis (𝓝 x) (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)
refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_
case inr.refine_1.mk.intro
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).fst (a, b).snd
case inr.refine_1
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.fst < x ∧ x < i.snd → ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.fst i.snd
rintro ⟨a, b⟩ ⟨ha, hb⟩
case inr.refine_1.mk.intro.intro.intro
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).fst (a, b).snd
case inr.refine_1.mk.intro
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).fst (a, b).snd
rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩
case inr.refine_1.mk.intro.intro.intro.intro.intro
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).snd
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).fst (a, b).snd
case inr.refine_1.mk.intro.intro.intro
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).fst (a, b).snd
rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩
case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_1
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).snd
⊢ (a, b).fst < x - min ε ↑δ

case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_2
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).snd
⊢ x + min ε ↑δ < (a, b).snd
case inr.refine_1.mk.intro.intro.intro.intro.intro
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).snd
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).fst (a, b).snd
refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
no goals
case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_1
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).snd
⊢ (a, b).fst < x - min ε ↑δ
exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)
no goals
case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_2
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).fst < x
hb : x < (a, b).snd
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).fst
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).snd
⊢ x + min ε ↑δ < (a, b).snd
exact (add_le_add_left (min_le_right _ _) _).trans_lt hδ
no goals
case inr.refine_2
α : Type ?u.61484
β : Type ?u.61487
γ : Type ?u.61490
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ i, (i.fst < x ∧ x < i.snd) ∧ Ioo i.fst i.snd ⊆ Icc (x - ε) (x + ε)
exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
  lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩