-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasBasis_nhds_of_ne_top' (xt : x ≠ ∞) :
    (𝓝 x).HasBasis (· ≠ 0) (fun ε => Icc (x - ε) (x + ε))

Proof state:
case inr.refine_1.mk.intro.intro.intro.intro.intro
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Tactic:
refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩

Result:
case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_1
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ (a, b).1 < x - ε ⊓ ↑δ

case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_2
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + ε ⊓ ↑δ < (a, b).2

Proof state:
case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_2
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + ε ⊓ ↑δ < (a, b).2

Tactic:
exact (add_le_add_left (min_le_right _ _) _).trans_lt hδ

Result:
no goals

Proof state:
case inr
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)

Tactic:
refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_

Result:
case inr.refine_1
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.1 < x ∧ x < i.2 → ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.1 i.2

case inr.refine_2
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ i, (i.1 < x ∧ x < i.2) ∧ Ioo i.1 i.2 ⊆ Icc (x - ε) (x + ε)

Proof state:
case inr.refine_1
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.1 < x ∧ x < i.2 → ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.1 i.2

Tactic:
rintro ⟨a, b⟩ ⟨ha, hb⟩

Result:
case inr.refine_1.mk.intro
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Proof state:
x : ℝ≥0∞
xt : x ≠ ⊤
⊢ (𝓝 x).HasBasis (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)

Tactic:
rcases (zero_le x).eq_or_gt with rfl | x0

Result:
case inl
xt : 0 ≠ ⊤
⊢ (𝓝 0).HasBasis (fun x => x ≠ 0) fun ε => Icc (0 - ε) (0 + ε)

case inr
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)

Proof state:
case inr.refine_1.mk.intro
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Tactic:
rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩

Result:
case inr.refine_1.mk.intro.intro.intro
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Proof state:
case inr.refine_1.mk.intro.intro.intro.intro.intro.refine_1
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ (a, b).1 < x - ε ⊓ ↑δ

Tactic:
exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)

Result:
no goals

Proof state:
case inr.refine_2
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ i, (i.1 < x ∧ x < i.2) ∧ Ioo i.1 i.2 ⊆ Icc (x - ε) (x + ε)

Tactic:
exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
  lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩

Result:
no goals

Proof state:
case inr.refine_1.mk.intro.intro.intro
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Tactic:
rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩

Result:
case inr.refine_1.mk.intro.intro.intro.intro.intro
x : ℝ≥0∞
xt : x ≠ ⊤
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Proof state:
case inl
xt : 0 ≠ ⊤
⊢ (𝓝 ⊥).HasBasis (fun x => ⊥ < x) fun ε => Iic ε

Tactic:
exact nhds_bot_basis_Iic

Result:
no goals

Proof state:
case inl
xt : 0 ≠ ⊤
⊢ (𝓝 0).HasBasis (fun x => x ≠ 0) fun ε => Icc (0 - ε) (0 + ε)

Tactic:
simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]

Result:
case inl
xt : 0 ≠ ⊤
⊢ (𝓝 ⊥).HasBasis (fun x => ⊥ < x) fun ε => Iic ε