-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma continuous_toENNReal : Continuous EReal.toENNReal

Proof state:
case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ ContinuousAt (fun x => ENNReal.ofReal x.toReal) x

Tactic:
refine ENNReal.continuous_ofReal.continuousAt.comp' <| continuousOn_toReal.continuousAt
  <| (toFinite _).isClosed.compl_mem_nhds ?_

Result:
case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ x ∉ {⊥, ⊤}

Proof state:
case h
x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
hy : ↑↑n < y
⊢ ↑n < y.toENNReal

Tactic:
exact toENNReal_coe (x := n) ▸ toENNReal_lt_toENNReal (coe_ennreal_nonneg _) hy

Result:
no goals

Proof state:
case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ x ∉ {⊥, ⊤}

Tactic:
simp_all only [mem_compl_iff, mem_singleton_iff, mem_insert_iff, or_self, not_false_eq_true]

Result:
no goals

Proof state:
case pos
x : EReal
h_top : x = ⊤
⊢ ContinuousAt toENNReal x

Tactic:
simp only [ContinuousAt, h_top, toENNReal_top]

Result:
case pos
x : EReal
h_top : x = ⊤
⊢ Tendsto toENNReal (𝓝 ⊤) (𝓝 ⊤)

Proof state:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ContinuousAt (fun x => ENNReal.ofReal x.toReal) x

Tactic:
refine tendsto_nhds_of_eventually_eq ?_

Result:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun x => ENNReal.ofReal x.toReal) x

Proof state:
case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousAt toENNReal x

Tactic:
refine ContinuousOn.continuousAt ?_ (compl_singleton_mem_nhds_iff.mpr h_top)

Result:
case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousOn toENNReal {⊤}ᶜ

Proof state:
case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousOn toENNReal {⊤}ᶜ

Tactic:
refine (continuousOn_of_forall_continuousAt fun x hx ↦ ?_).congr (fun _ h ↦ toENNReal_of_ne_top h)

Result:
case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
⊢ ContinuousAt (fun x => ENNReal.ofReal x.toReal) x

Proof state:
case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
⊢ ContinuousAt (fun x => ENNReal.ofReal x.toReal) x

Tactic:
by_cases h_bot : x = ⊥

Result:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ContinuousAt (fun x => ENNReal.ofReal x.toReal) x

case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ ContinuousAt (fun x => ENNReal.ofReal x.toReal) x

Proof state:
case pos
x : EReal
h_top : x = ⊤
n : ℕ
⊢ ∀ᶠ (a : EReal) in 𝓝 ⊤, ↑n < a.toENNReal

Tactic:
filter_upwards [eventually_gt_nhds (coe_lt_top n)] with y hy

Result:
case h
x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
hy : ↑↑n < y
⊢ ↑n < y.toENNReal

Proof state:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio ↑i → ENNReal.ofReal x.toReal = (fun x => ENNReal.ofReal x.toReal) ⊥

Tactic:
simp [toReal_bot, ENNReal.ofReal_zero, ENNReal.ofReal_eq_zero, true_and]

Result:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, ∀ ⦃x : EReal⦄, x < ↑i → x.toReal ≤ 0

Proof state:
x : EReal
⊢ ContinuousAt toENNReal x

Tactic:
by_cases h_top : x = ⊤

Result:
case pos
x : EReal
h_top : x = ⊤
⊢ ContinuousAt toENNReal x

case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousAt toENNReal x

Proof state:
case pos
x : EReal
h_top : x = ⊤
⊢ Tendsto toENNReal (𝓝 ⊤) (𝓝 ⊤)

Tactic:
refine ENNReal.tendsto_nhds_top fun n ↦ ?_

Result:
case pos
x : EReal
h_top : x = ⊤
n : ℕ
⊢ ∀ᶠ (a : EReal) in 𝓝 ⊤, ↑n < a.toENNReal

Proof state:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun x => ENNReal.ofReal x.toReal) x

Tactic:
rw [h_bot, nhds_bot_basis.eventually_iff]

Result:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio ↑i → ENNReal.ofReal x.toReal = (fun x => ENNReal.ofReal x.toReal) ⊥

Proof state:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, ∀ ⦃x : EReal⦄, x < ↑i → x.toReal ≤ 0

Tactic:
exact ⟨0, fun _ hx ↦ toReal_nonpos hx.le⟩

Result:
no goals

Proof state:
⊢ Continuous toENNReal

Tactic:
refine continuous_iff_continuousAt.mpr fun x ↦ ?_

Result:
x : EReal
⊢ ContinuousAt toENNReal x