awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
⊢ (Continuous[inst, _] fun (a : α) ↦ (↑(f a) : EReal)) ↔ Continuous[inst, _] f

Tactic:
isEmbedding_coe.continuous_iff.symm

Premises used: EReal.isEmbedding_coe, Topology.IsEmbedding.continuous_iff, Iff.symm, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
r : ℝ
⊢ 𝓝 (↑r : EReal) = map Real.toEReal (𝓝 r)

Tactic:
(isOpenEmbedding_coe.map_nhds_eq r).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, EReal.isOpenEmbedding_coe, Eq.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
r p : ℝ
⊢ 𝓝 ((↑r : EReal), (↑p : EReal)) = map (fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal))) (𝓝 (r, p))

Tactic:
((isOpenEmbedding_coe.prodMap isOpenEmbedding_coe).map_nhds_eq (r, p)).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, EReal.isOpenEmbedding_coe, Prod.mk, Prod.map, Eq.symm, Topology.IsOpenEmbedding.prodMap
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
⊢ a ≠ ⊤ ∧ a ≠ ⊥

Tactic:
⟨ha, h'a⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
lift :
  ∀ (a : ℝ) (ha : (↑a : EReal) ≠ ⊤) (h'a : (↑a : EReal) ≠ ⊥), Tendsto toReal (𝓝 (↑a : EReal)) (𝓝 (↑a : EReal).toReal)
⊢ Tendsto toReal (𝓝 a) (𝓝 a.toReal)

Tactic:
lift a to ℝ using ⟨ha, h'a⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
ha : (↑a : EReal) ≠ ⊤
h'a : (↑a : EReal) ≠ ⊥
rw : Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a : EReal).toReal)
⊢ Tendsto toReal (𝓝 (↑a : EReal)) (𝓝 (↑a : EReal).toReal)

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Premises used: EReal.nhds_coe, Filter.tendsto_map'_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
ha : (↑a : EReal) ≠ ⊤
h'a : (↑a : EReal) ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a : EReal).toReal)

Tactic:
tendsto_id

Premises used: Filter.tendsto_id, EReal.toReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
ha : (↑a : EReal) ≠ ⊤
h'a : (↑a : EReal) ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a : EReal).toReal)

Tactic:
exact tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ ContinuousOn toReal {⊥, ⊤}ᶜ

Tactic:
fun _a ha =>
  ContinuousAt.continuousWithinAt (tendsto_toReal (mt Or.inr ha) (mt Or.inl ha))

Premises used: ContinuousAt.continuousWithinAt, mt, ContinuousOn, EReal.tendsto_toReal, Or.inl, Or.inr
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
rw : OrdConnected (α := EReal) (Ici 0)
⊢ (range ENNReal.toEReal).OrdConnected

Tactic:
rw [range_coe_ennreal]

Premises used: EReal.range_coe_ennreal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ OrdConnected (α := EReal) (Ici 0)

Tactic:
ordConnected_Ici

Premises used: Set.ordConnected_Ici
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ OrdConnected (α := EReal) (Ici 0)

Tactic:
exact ordConnected_Ici

Premises used: Set.ordConnected_Ici
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
rw : IsClosed (X := EReal) (Ici 0)
⊢ IsClosed (range ENNReal.toEReal)

Tactic:
rw [range_coe_ennreal]

Premises used: EReal.range_coe_ennreal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ IsClosed (X := EReal) (Ici 0)

Tactic:
isClosed_Ici

Premises used: isClosed_Ici
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ IsClosed (X := EReal) (Ici 0)

Tactic:
exact isClosed_Ici

Premises used: isClosed_Ici
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
f : Filter α
m : α → ℝ≥0∞
a : ℝ≥0∞
⊢ Tendsto (fun (a : α) ↦ (↑(m a) : EReal)) f (𝓝 (↑a : EReal)) ↔ Tendsto m f (𝓝 a)

Tactic:
isEmbedding_coe_ennreal.tendsto_nhds_iff.symm

Premises used: Topology.IsEmbedding.tendsto_nhds_iff, ENNReal.toEReal, EReal.isEmbedding_coe_ennreal, Iff.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Continuous ENNReal.toEReal

Tactic:
isEmbedding_coe_ennreal.continuous

Premises used: EReal.isEmbedding_coe_ennreal, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ≥0∞
⊢ (Continuous[inst, _] fun (a : α) ↦ (↑(f a) : EReal)) ↔ Continuous[inst, _] f

Tactic:
isEmbedding_coe_ennreal.continuous_iff.symm

Premises used: ENNReal.toEReal, EReal.isEmbedding_coe_ennreal, Topology.IsEmbedding.continuous_iff, Iff.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Eq (α := Filter EReal) (⨅ (l : EReal), ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) (⨅ (a : EReal), ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a))

Tactic:
simp only [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ HasBasis (α := EReal) (𝓝 ⊤) (fun (x : ℝ) ↦ True) fun (x : ℝ) ↦ Ioi (↑x : EReal)

Tactic:
(nhds_top_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro, nhds_top_basis, Filter.HasBasis.to_hasBasis, Real.toEReal, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
refine : ∀ (x : EReal) (hx : x < ⊤), ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x
⊢ HasBasis (α := EReal) (𝓝 ⊤) (fun (x : ℝ) ↦ True) fun (x : ℝ) ↦ Ioi (↑x : EReal)

Tactic:
refine (nhds_top_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : x < ⊤
rcases : ∀ (y : ℚ) (hxy : x < (↑(↑y : ℝ) : EReal)), ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x
⊢ ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x

Tactic:
rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩

Premises used: EReal.exists_rat_btwn_of_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : x < ⊤
y : ℚ
hxy : x < (↑(↑y : ℝ) : EReal)
⊢ ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x

Tactic:
⟨_, trivial, Ioi_subset_Ioi hxy.le⟩

Premises used: trivial, LT.lt.le, And.intro, Exists.intro, Set.Ioi_subset_Ioi
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : x < ⊤
y : ℚ
hxy : x < (↑(↑y : ℝ) : EReal)
⊢ ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x

Tactic:
exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Eq (α := Filter EReal) (𝓝 ⊤) (⨅ (a : ℝ), 𝓟 (Ioi (↑a : EReal)))

Tactic:
nhds_top_basis.eq_iInf

Premises used: EReal.nhds_top_basis, Filter.HasBasis.eq_iInf
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
s : Set EReal
⊢ (∃ (i : ℝ), True ∧ Ioi (↑i : EReal) ⊆ s) ↔ ∃ (y : ℝ), Ioi (↑y : EReal) ⊆ s

Tactic:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Ioi (↑i : EReal)) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, (↑x : EReal) < m a

Tactic:
simp only [true_implies, mem_Ioi]

Premises used: Set.mem_Ioi, true_implies
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Eq (α := Filter EReal) (⨅ (l : EReal), ⨅ (_ : ⊥ < l), 𝓟 (Iio l)) (⨅ (a : EReal), ⨅ (_ : a ≠ ⊥), 𝓟 (Iio a))

Tactic:
simp only [bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ HasBasis (α := EReal) (𝓝 ⊥) (fun (x : ℝ) ↦ True) fun (x : ℝ) ↦ Iio (↑x : EReal)

Tactic:
(_root_.nhds_bot_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩

Premises used: nhds_bot_basis, EReal.bot_lt_coe, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
refine : ∀ (x : EReal) (hx : ⊥ < x), ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x
⊢ HasBasis (α := EReal) (𝓝 ⊥) (fun (x : ℝ) ↦ True) fun (x : ℝ) ↦ Iio (↑x : EReal)

Tactic:
refine (_root_.nhds_bot_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩

Premises used: nhds_bot_basis, EReal.bot_lt_coe, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : ⊥ < x
rcases : ∀ (y : ℚ) (hxy : (↑(↑y : ℝ) : EReal) < x), ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x
⊢ ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x

Tactic:
rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩

Premises used: EReal.exists_rat_btwn_of_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : ⊥ < x
y : ℚ
hxy : (↑(↑y : ℝ) : EReal) < x
⊢ ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x

Tactic:
⟨_, trivial, Iio_subset_Iio hxy.le⟩

Premises used: trivial, LT.lt.le, Set.Iio_subset_Iio, And.intro, Exists.intro
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : ⊥ < x
y : ℚ
hxy : (↑(↑y : ℝ) : EReal) < x
⊢ ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x

Tactic:
exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Eq (α := Filter EReal) (𝓝 ⊥) (⨅ (a : ℝ), 𝓟 (Iio (↑a : EReal)))

Tactic:
nhds_bot_basis.eq_iInf

Premises used: EReal.nhds_bot_basis, Filter.HasBasis.eq_iInf
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
s : Set EReal
⊢ (∃ (i : ℝ), True ∧ Iio (↑i : EReal) ⊆ s) ↔ ∃ (y : ℝ), Iio (↑y : EReal) ⊆ s

Tactic:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Iio (↑i : EReal)) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < (↑x : EReal)

Tactic:
simp only [true_implies, mem_Iio]

Premises used: Set.mem_Iio, true_implies
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : ∀ i < ⊤, ∃ (i' : ℝ), True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ
h' : ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'
⊢ 𝓝[≠] ⊤ = map Real.toEReal atTop

Tactic:
apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)

Premises used: Filter.atTop_basis, nhds_top_basis_Ici, Filter.HasBasis.map, nhdsWithin_hasBasis, Filter.HasBasis.ext, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : ∀ i < ⊤, ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici i ∩ {⊤}ᶜ
⊢ ∀ i < ⊤, ∃ (i' : ℝ), True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ

Tactic:
simp only [EReal.image_coe_Ici, true_and]

Premises used: EReal.image_coe_Ici, true_and
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : x < ⊤
pos : ∀ (hx_bot : x = ⊥), ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
neg : ∀ (hx_bot : ¬x = ⊥), ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
by_cases hx_bot : x = ⊥
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : x < ⊤
hx_bot : x = ⊥
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
simp [hx_bot]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : x < ⊤
hx_bot : ¬x = ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨hx.ne_top, hx_bot⟩

Premises used: LT.lt.ne_top, And.intro
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : x < ⊤
hx_bot : ¬x = ⊥
neg :
  ∀ (x : ℝ) (hx : (↑x : EReal) < ⊤) (hx_bot : ¬(↑x : EReal) = ⊥),
    ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici (↑x : EReal) ∩ {⊤}ᶜ
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
lift x to ℝ using ⟨hx.ne_top, hx_bot⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
hx : (↑x : EReal) < ⊤
hx_bot : ¬(↑x : EReal) = ⊥
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici (↑x : EReal) ∩ {⊤}ᶜ

Tactic:
⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩

Premises used: Set.Ici, Compl.compl, Membership.mem, Inter.inter, Exists.intro, _private.0.EReal.nhdsWithin_top.match_1, Top.top, Singleton.singleton, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
hx : (↑x : EReal) < ⊤
hx_bot : ¬(↑x : EReal) = ⊥
neg : ∀ x_1 ∈ Ico (↑x : EReal) ⊤, ∀ (h1 : (↑x : EReal) ≤ x_1) (h2 : x_1 < ⊤), x_1 ∈ Ici (↑x : EReal) ∩ {⊤}ᶜ
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici (↑x : EReal) ∩ {⊤}ᶜ

Tactic:
refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : ℝ
hx : (↑x_1 : EReal) < ⊤
hx_bot : ¬(↑x_1 : EReal) = ⊥
x : EReal
h : x ∈ Ico (↑x_1 : EReal) ⊤
h1 : (↑x_1 : EReal) ≤ x
h2 : x < ⊤
⊢ x ∈ Ici (↑x_1 : EReal) ∩ {⊤}ᶜ

Tactic:
simp [h1, h2.ne_top]

Premises used: LT.lt.ne_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h' : ∀ (i' : ℝ), ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Ico (↑i' : EReal) ⊤
⊢ ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'

Tactic:
simp only [EReal.image_coe_Ici, true_implies]

Premises used: EReal.image_coe_Ici, true_implies
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ ∀ (i' : ℝ), ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Ico (↑i' : EReal) ⊤

Tactic:
fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩

Premises used: Membership.mem, _private.0.EReal.nhdsWithin_top.match_2, Set.Ico, And.intro, Exists.intro, Top.top, Real.toEReal, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h' :
  ∀ (x : ℝ),
    ∀ x_1 ∈ Ici (↑x : EReal) ∩ {⊤}ᶜ,
      ∀ (h1 : (↑x : EReal) ≤ x_1) (h2 : Membership.mem (γ := Set EReal) {⊤}ᶜ x_1), x_1 ∈ Ico (↑x : EReal) ⊤
⊢ ∀ (i' : ℝ), ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Ico (↑i' : EReal) ⊤

Tactic:
refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : ℝ
x : EReal
h : x ∈ Ici (↑x_1 : EReal) ∩ {⊤}ᶜ
h1 : (↑x_1 : EReal) ≤ x
h2 : Membership.mem (γ := Set EReal) {⊤}ᶜ x
⊢ x ∈ Ico (↑x_1 : EReal) ⊤

Tactic:
simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]

Premises used: Ne.lt_top', Eq.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : ∀ (i : EReal), ⊥ < i → ∃ (i' : ℝ), True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ
h' : ∀ (i' : ℝ), True → ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'
⊢ 𝓝[≠] ⊥ = map Real.toEReal atBot

Tactic:
apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)

Premises used: Filter.atBot_basis, Filter.HasBasis.map, nhdsWithin_hasBasis, Filter.HasBasis.ext, nhds_bot_basis_Iic, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : ∀ (i : EReal), ⊥ < i → ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic i ∩ {⊥}ᶜ
⊢ ∀ (i : EReal), ⊥ < i → ∃ (i' : ℝ), True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ

Tactic:
simp only [EReal.image_coe_Iic,
      true_and]

Premises used: EReal.image_coe_Iic, true_and
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : ⊥ < x
pos : ∀ (hx_top : x = ⊤), ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
neg : ∀ (hx_top : ¬x = ⊤), ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
by_cases hx_top : x = ⊤
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : ⊥ < x
hx_top : x = ⊤
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
simp [hx_top]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : ⊥ < x
hx_top : ¬x = ⊤
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨hx_top, hx.ne_bot⟩

Premises used: And.intro, LT.lt.ne_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
hx : ⊥ < x
hx_top : ¬x = ⊤
neg :
  ∀ (x : ℝ) (hx : ⊥ < (↑x : EReal)) (hx_top : ¬(↑x : EReal) = ⊤),
    ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic (↑x : EReal) ∩ {⊥}ᶜ
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
lift x to ℝ using ⟨hx_top, hx.ne_bot⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
hx : ⊥ < (↑x : EReal)
hx_top : ¬(↑x : EReal) = ⊤
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic (↑x : EReal) ∩ {⊥}ᶜ

Tactic:
⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩

Premises used: Compl.compl, Membership.mem, Bot.bot, Inter.inter, Exists.intro, Set.Iic, Singleton.singleton, _private.0.EReal.nhdsWithin_bot.match_1, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
hx : ⊥ < (↑x : EReal)
hx_top : ¬(↑x : EReal) = ⊤
neg : ∀ x_1 ∈ Ioc ⊥ (↑x : EReal), ∀ (h1 : ⊥ < x_1) (h2 : x_1 ≤ (↑x : EReal)), x_1 ∈ Iic (↑x : EReal) ∩ {⊥}ᶜ
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic (↑x : EReal) ∩ {⊥}ᶜ

Tactic:
refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : ℝ
hx : ⊥ < (↑x_1 : EReal)
hx_top : ¬(↑x_1 : EReal) = ⊤
x : EReal
h : x ∈ Ioc ⊥ (↑x_1 : EReal)
h1 : ⊥ < x
h2 : x ≤ (↑x_1 : EReal)
⊢ x ∈ Iic (↑x_1 : EReal) ∩ {⊥}ᶜ

Tactic:
simp [h2, h1.ne_bot]

Premises used: LT.lt.ne_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h' : ∀ (i' : ℝ), ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ (↑i' : EReal)
⊢ ∀ (i' : ℝ), True → ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'

Tactic:
simp only [EReal.image_coe_Iic, true_implies]

Premises used: EReal.image_coe_Iic, true_implies
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ ∀ (i' : ℝ), ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ (↑i' : EReal)

Tactic:
fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩

Premises used: Set.Ioc, _private.0.EReal.nhdsWithin_bot.match_2, EReal.bot_lt_coe, Membership.mem, Bot.bot, And.intro, Exists.intro, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h' :
  ∀ (x : ℝ),
    ∀ x_1 ∈ Iic (↑x : EReal) ∩ {⊥}ᶜ,
      ∀ (h1 : x_1 ≤ (↑x : EReal)) (h2 : Membership.mem (γ := Set EReal) {⊥}ᶜ x_1), x_1 ∈ Ioc ⊥ (↑x : EReal)
⊢ ∀ (i' : ℝ), ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ (↑i' : EReal)

Tactic:
refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : ℝ
x : EReal
h : x ∈ Iic (↑x_1 : EReal) ∩ {⊥}ᶜ
h1 : x ≤ (↑x_1 : EReal)
h2 : Membership.mem (γ := Set EReal) {⊥}ᶜ x
⊢ x ∈ Ioc ⊥ (↑x_1 : EReal)

Tactic:
simp [h1, Ne.bot_lt' fun a ↦ h2 a.symm]

Premises used: Ne.bot_lt', Eq.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
rw : (∀ (x : ℝ), ∀ᶠ (a : α) in l, (↑x : EReal) < (↑(f a) : EReal)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
⊢ Tendsto (β := EReal) (fun (x : α) ↦ (↑(f x) : EReal)) l (𝓝 ⊤) ↔ Tendsto f l atTop

Tactic:
rw [tendsto_nhds_top_iff_real, atTop_basis_Ioi.tendsto_right_iff]

Premises used: Filter.atTop_basis_Ioi, EReal.tendsto_nhds_top_iff_real, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, (↑x : EReal) < (↑(f a) : EReal)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i

Tactic:
simp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Tendsto Real.toEReal atTop (𝓝 ⊤)

Tactic:
tendsto_coe_nhds_top_iff.2 tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, EReal.tendsto_coe_nhds_top_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
rw : (∀ (x : ℝ), ∀ᶠ (a : α) in l, (↑(f a) : EReal) < (↑x : EReal)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Iio i
⊢ Tendsto (β := EReal) (fun (x : α) ↦ (↑(f x) : EReal)) l (𝓝 ⊥) ↔ Tendsto f l atBot

Tactic:
rw [tendsto_nhds_bot_iff_real, atBot_basis_Iio.tendsto_right_iff]

Premises used: Filter.atBot_basis_Iio, Filter.HasBasis.tendsto_right_iff, EReal.tendsto_nhds_bot_iff_real
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, (↑(f a) : EReal) < (↑x : EReal)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Iio i

Tactic:
simp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Tendsto Real.toEReal atBot (𝓝 ⊥)

Tactic:
tendsto_coe_nhds_bot_iff.2 tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, EReal.tendsto_coe_nhds_bot_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
rw : Tendsto (toReal ∘ Real.toEReal) atTop atTop
⊢ Tendsto toReal (𝓝[≠] ⊤) atTop

Tactic:
rw [nhdsWithin_top, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, EReal.nhdsWithin_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Tendsto (toReal ∘ Real.toEReal) atTop atTop

Tactic:
tendsto_id

Premises used: Filter.tendsto_id, EReal.toReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Tendsto (toReal ∘ Real.toEReal) atTop atTop

Tactic:
exact tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
rw : Tendsto (toReal ∘ Real.toEReal) atBot atBot
⊢ Tendsto toReal (𝓝[≠] ⊥) atBot

Tactic:
rw [nhdsWithin_bot, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, EReal.nhdsWithin_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Tendsto (toReal ∘ Real.toEReal) atBot atBot

Tactic:
tendsto_id

Premises used: Filter.tendsto_id, EReal.toReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Tendsto (toReal ∘ Real.toEReal) atBot atBot

Tactic:
exact tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Continuous toENNReal

Tactic:
continuous_iff_continuousAt.mpr fun x ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
refine : ∀ (x : EReal), ContinuousAt toENNReal x
⊢ Continuous toENNReal

Tactic:
refine continuous_iff_continuousAt.mpr fun x ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
pos : ∀ (h_top : x = ⊤), ContinuousAt toENNReal x
neg : ∀ (h_top : ¬x = ⊤), ContinuousAt toENNReal x
⊢ ContinuousAt toENNReal x

Tactic:
by_cases h_top : x = ⊤
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : x = ⊤
pos : Tendsto toENNReal (𝓝 ⊤) (𝓝 ∞)
⊢ ContinuousAt toENNReal x

Tactic:
simp only [ContinuousAt, h_top, toENNReal_top]

Premises used: EReal.toENNReal_top, ContinuousAt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : x = ⊤
⊢ Tendsto toENNReal (𝓝 ⊤) (𝓝 ∞)

Tactic:
ENNReal.tendsto_nhds_top fun n ↦ ?_

Premises used: ENNReal.tendsto_nhds_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : x = ⊤
pos : ∀ (n : ℕ), ∀ᶠ (a : EReal) in 𝓝 ⊤, (↑n : ℝ≥0∞) < a.toENNReal
⊢ Tendsto toENNReal (𝓝 ⊤) (𝓝 ∞)

Tactic:
refine ENNReal.tendsto_nhds_top fun n ↦ ?_

Premises used: ENNReal.tendsto_nhds_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : x = ⊤
n : ℕ
h : ∀ (y : EReal) (hy : (↑(↑n : ℝ) : EReal) < y), (↑n : ℝ≥0∞) < y.toENNReal
⊢ ∀ᶠ (a : EReal) in 𝓝 ⊤, (↑n : ℝ≥0∞) < a.toENNReal

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

Premises used: eventually_gt_nhds, Nat.cast, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
hy : (↑(↑n : ℝ) : EReal) < y
⊢ (↑n : ℝ≥0∞) < y.toENNReal

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

Premises used: EReal.toENNReal_lt_toENNReal, Eq.rec, EReal.toENNReal_coe, EReal.coe_ennreal_nonneg
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
hy : (↑(↑n : ℝ) : EReal) < y
⊢ (↑n : ℝ≥0∞) < y.toENNReal

Tactic:
exact toENNReal_coe (x := n) ▸ toENNReal_lt_toENNReal (coe_ennreal_nonneg _) hy
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousAt toENNReal x

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

Premises used: Iff.mpr, compl_singleton_mem_nhds_iff, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : ¬x = ⊤
neg : ContinuousOn toENNReal {⊤}ᶜ
⊢ ContinuousAt toENNReal x

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

Premises used: Iff.mpr, compl_singleton_mem_nhds_iff, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousOn toENNReal {⊤}ᶜ

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

Premises used: EReal.toENNReal_of_ne_top, continuousOn_of_forall_continuousAt, ContinuousOn.congr
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal
h_top : ¬x = ⊤
neg :
  ∀ (x : EReal) (hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x),
    ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
⊢ ContinuousOn toENNReal {⊤}ᶜ

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

Premises used: EReal.toENNReal_of_ne_top, continuousOn_of_forall_continuousAt, ContinuousOn.congr