awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
hd : DiscreteTopology α
inst_1 : Countable α
i : α
⊢ Eq (α := TopologicalSpace (↑{i} : Type u_1))
    (instTopologicalSpaceSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) {i} x)) (generateFrom {univ})

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : SuccOrder α
x : TopologicalSpace α := Preorder.topology α
⊢ OrderTopology α

Tactic:
have : OrderTopology α := ⟨rfl⟩
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : SuccOrder α
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ ⊥ = Preorder.topology α

Tactic:
DiscreteTopology.of_predOrder_succOrder.eq_bot.symm

Premises used: DiscreteTopology.eq_bot, Eq.symm
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : SuccOrder α
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ ⊥ = Preorder.topology α

Tactic:
exact DiscreteTopology.of_predOrder_succOrder.eq_bot.symm

Premises used: DiscreteTopology.eq_bot, Eq.symm
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : PredOrder α
inst_3 : SuccOrder α
⊢ DiscreteTopology α ↔ OrderTopology α

Tactic:
⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩

Premises used: DiscreteTopology.of_predOrder_succOrder, OrderTopology.mk, Iff.intro
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : PredOrder α
inst_3 : SuccOrder α
refine : ∀ (h : DiscreteTopology α), inst = Preorder.topology α
⊢ DiscreteTopology α ↔ OrderTopology α

Tactic:
refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : PredOrder α
inst_3 : SuccOrder α
h : DiscreteTopology α
rw : ⊥ = Preorder.topology α
rw₁ rw₂ : Preorder.topology α = Preorder.topology α
⊢ inst = Preorder.topology α

Tactic:
rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_preorderTopology]

Premises used: LinearOrder.bot_topologicalSpace_eq_preorderTopology, DiscreteTopology.eq_bot
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : PredOrder α
inst_3 : SuccOrder α
inst_4 : DiscreteTopology α
⊢ OrderTopology α

Tactic:
discreteTopology_iff_orderTopology_of_pred_succ.mp ‹_›

Premises used: Iff.mp, discreteTopology_iff_orderTopology_of_pred_succ
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DiscreteTopology α
⊢ OrderTopology α

Tactic:
haveI := LinearLocallyFiniteOrder.succOrder α
  haveI := LinearLocallyFiniteOrder.predOrder α
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal
Goal:
⊢ Continuous toENNReal

Tactic:
OrderTopology.continuous_iff.mpr fun a ↦ ⟨?_, ?_⟩

Premises used: Iff.mpr, OrderTopology.continuous_iff, And.intro
-- Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal
Goal:
refine_1 : ∀ (a : ENNReal), IsOpen (toENNReal ⁻¹' Set.Ioi a)
refine_2 : ∀ (a : ENNReal), IsOpen (toENNReal ⁻¹' Set.Iio a)
⊢ Continuous toENNReal

Tactic:
refine OrderTopology.continuous_iff.mpr fun a ↦ ⟨?_, ?_⟩

Premises used: Iff.mpr, OrderTopology.continuous_iff, And.intro
-- Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal
Goal:
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Ioi a)

Tactic:
simpa using isOpen_Ioi

Premises used: isOpen_Ioi
-- Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal
Goal:
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Iio a)

Tactic:
simpa using isOpen_Iio

Premises used: isOpen_Iio
-- Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal
Goal:
⊢ Topology.IsClosedEmbedding toENNReal

Tactic:
continuous_toENNReal.isClosedEmbedding toENNReal_strictMono.injective

Premises used: ENat.toENNReal_strictMono, Continuous.isClosedEmbedding, StrictMono.injective, ENat.continuous_toENNReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ IsOpen (X := ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞}

Tactic:
isOpen_ne

Premises used: isOpen_ne
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0∞
rw : IsOpen (Iio b)
⊢ IsOpen (Ico 0 b)

Tactic:
rw [ENNReal.Ico_eq_Iio]

Premises used: ENNReal.Ico_eq_Iio
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0∞
⊢ IsOpen (Iio b)

Tactic:
isOpen_Iio

Premises used: isOpen_Iio
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0∞
⊢ IsOpen (Iio b)

Tactic:
exact isOpen_Iio

Premises used: isOpen_Iio
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
r : ℝ≥0
⊢ range ofNNReal ∈ 𝓝 (↑r : ℝ≥0∞)

Tactic:
IsOpen.mem_nhds isOpenEmbedding_coe.isOpen_range <| mem_range_self _

Premises used: Set.mem_range_self, ENNReal.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isOpen_range, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Continuous ofNNReal

Tactic:
isEmbedding_coe.continuous

Premises used: ENNReal.isEmbedding_coe, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
nth_rewrite : Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 (↑a.toNNReal : ℝ≥0∞))
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 a)

Tactic:
nth_rewrite 2 [← coe_toNNReal ha]

Premises used: ENNReal.coe_toNNReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 (↑a.toNNReal : ℝ≥0∞))

Tactic:
continuous_coe.tendsto _

Premises used: Continuous.tendsto, ENNReal.continuous_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 (↑a.toNNReal : ℝ≥0∞))

Tactic:
exact continuous_coe.tendsto _

Premises used: Continuous.tendsto, ENNReal.continuous_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
inst : TopologicalSpace α
f : α → ℝ≥0
⊢ (Continuous[inst, _] fun (a : α) ↦ (↑(f a) : ℝ≥0∞)) ↔ Continuous[inst, _] f

Tactic:
isEmbedding_coe.continuous_iff.symm

Premises used: ENNReal.ofNNReal, WithTop.some, Topology.IsEmbedding.continuous_iff, Iff.symm, ENNReal.isEmbedding_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
r : ℝ≥0
⊢ 𝓝 (↑r : ℝ≥0∞) = map ofNNReal (𝓝 r)

Tactic:
(isOpenEmbedding_coe.map_nhds_eq r).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, ENNReal.isOpenEmbedding_coe, Eq.symm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
rw : Tendsto f (map ofNNReal (𝓝 x)) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
rw₁ rw₂ : Tendsto (f ∘ ofNNReal) (𝓝 x) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
⊢ Tendsto f (𝓝 (↑x : ℝ≥0∞)) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, ENNReal.nhds_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
inst : TopologicalSpace α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ ContinuousAt f (↑x : ℝ≥0∞) ↔ ContinuousAt (f ∘ ofNNReal) x

Tactic:
tendsto_nhds_coe_iff

Premises used: ContinuousAt, ENNReal.tendsto_nhds_coe_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Continuous ENNReal.ofReal

Tactic:
(continuous_coe_iff.2 continuous_id).comp continuous_real_toNNReal

Premises used: Iff.mpr, ENNReal.ofNNReal, ENNReal.ofReal, Continuous.comp, ENNReal.continuous_coe_iff, NNReal.mk, WithTop.some, continuous_id, continuous_real_toNNReal, Real.toNNReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ
a : ℝ
h : Tendsto m f (𝓝 a)
⊢ Tendsto (fun (a : α) ↦ ENNReal.ofReal (m a)) f (𝓝 (ENNReal.ofReal a))

Tactic:
(continuous_ofReal.tendsto a).comp h

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.continuous_ofReal, WithTop.some, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≠ ∞

Tactic:
ha
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
lift : ∀ (a : ℝ≥0), Tendsto ENNReal.toNNReal (𝓝 (↑a : ℝ≥0∞)) (𝓝 (↑a : ℝ≥0∞).toNNReal)
⊢ Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 a.toNNReal)

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
rw : Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a : ℝ≥0∞).toNNReal)
⊢ Tendsto ENNReal.toNNReal (𝓝 (↑a : ℝ≥0∞)) (𝓝 (↑a : ℝ≥0∞).toNNReal)

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, ENNReal.nhds_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a : ℝ≥0∞).toNNReal)

Tactic:
tendsto_id

Premises used: Filter.tendsto_id, ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a : ℝ≥0∞).toNNReal)

Tactic:
exact tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal) ↔ Tendsto f u (𝓝 a)

Tactic:
⟨fun h => ?_, fun h => (ENNReal.tendsto_toNNReal ha).comp h⟩

Premises used: ENNReal.tendsto_toNNReal, Iff.intro, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
refine : ∀ (h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)), Tendsto f u (𝓝 a)
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal) ↔ Tendsto f u (𝓝 a)

Tactic:
refine ⟨fun h => ?_, fun h => (ENNReal.tendsto_toNNReal ha).comp h⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
rw : Tendsto ((fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f) u (𝓝 a)
⊢ Tendsto f u (𝓝 a)

Tactic:
rw [← coe_comp_toNNReal_comp hf]

Premises used: ENNReal.coe_comp_toNNReal_comp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto ((fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f) u (𝓝 a)

Tactic:
(tendsto_coe_toNNReal ha).comp h

Premises used: ENNReal.tendsto_coe_toNNReal, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto ((fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f) u (𝓝 a)

Tactic:
exact (tendsto_coe_toNNReal ha).comp h

Premises used: ENNReal.tendsto_coe_toNNReal, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ∞
rw : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (↑a : ℝ≥0∞).toNNReal) ↔ Tendsto f u (𝓝 (↑(↑a : ℝ≥0∞).toNNReal : ℝ≥0∞))
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a) ↔ Tendsto f u (𝓝 (↑a : ℝ≥0∞))

Tactic:
rw [← toNNReal_coe a]

Premises used: ENNReal.toNNReal_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (↑a : ℝ≥0∞).toNNReal) ↔ Tendsto f u (𝓝 (↑(↑a : ℝ≥0∞).toNNReal : ℝ≥0∞))

Tactic:
tendsto_toNNReal_iff coe_ne_top hf

Premises used: ENNReal.toNNReal, ENNReal.tendsto_toNNReal_iff, WithTop.untopD, WithTop.recTopCoe, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (↑a : ℝ≥0∞).toNNReal) ↔ Tendsto f u (𝓝 (↑(↑a : ℝ≥0∞).toNNReal : ℝ≥0∞))

Tactic:
exact tendsto_toNNReal_iff coe_ne_top hf

Premises used: ENNReal.tendsto_toNNReal_iff, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : l.EventuallyEq (β := ℝ) (fun (x : α) ↦ (f x).toReal) fun (x : α) ↦ (g x).toReal
a : α
hfx : f a ≠ ∞
hgx : g a ≠ ∞
h : (f a).toReal = (g a).toReal → f a = g a
⊢ (f a).toReal = (g a).toReal → f a = g a

Tactic:
_
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : l.EventuallyEq (β := ℝ) (fun (x : α) ↦ (f x).toReal) fun (x : α) ↦ (g x).toReal
h : ∀ (a : α) (hfx : f a ≠ ∞) (hgx : g a ≠ ∞), (f a).toReal = (g a).toReal → f a = g a
⊢ f =ᶠ[l] g

Tactic:
filter_upwards [hfi, hgi, hfg] with _ hfx hgx _
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : l.EventuallyEq (β := ℝ) (fun (x : α) ↦ (f x).toReal) fun (x : α) ↦ (g x).toReal
a : α
hfx : f a ≠ ∞
hgx : g a ≠ ∞
h_1 h h₁ h₂ h₃ : (f a).toReal = (g a).toReal
⊢ f a = g a

Tactic:
rwa [← ENNReal.toReal_eq_toReal_iff' hfx hgx]

Premises used: ENNReal.toReal_eq_toReal_iff'
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ ContinuousOn ENNReal.toNNReal {a : ℝ≥0∞ | a ≠ ∞}

Tactic:
fun _a ha =>
  ContinuousAt.continuousWithinAt (tendsto_toNNReal ha)

Premises used: ContinuousAt.continuousWithinAt, ENNReal.tendsto_toNNReal, ContinuousOn
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ENNReal.toReal (𝓝 a) (𝓝 a.toReal)

Tactic:
NNReal.tendsto_coe.2 <| tendsto_toNNReal ha

Premises used: Iff.mpr, ENNReal.tendsto_toNNReal, ENNReal.toReal, NNReal.tendsto_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ ContinuousOn ENNReal.toReal {a : ℝ≥0∞ | a ≠ ∞}

Tactic:
NNReal.continuous_coe.comp_continuousOn continuousOn_toNNReal

Premises used: Continuous.comp_continuousOn, NNReal.continuous_coe, ENNReal.toReal, ENNReal.continuousOn_toNNReal, NNReal.toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
⊢ ContinuousAt ENNReal.toReal x

Tactic:
continuousOn_toReal.continuousAt (isOpen_ne_top.mem_nhds_iff.mpr hx)

Premises used: Iff.mpr, ENNReal.isOpen_ne_top, IsOpen.mem_nhds_iff, ENNReal.continuousOn_toReal, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b : ℝ≥0∞
r : ℝ≥0
x ε : ℝ≥0∞
refine : Eq (α := Set ℝ≥0∞) {a : ℝ≥0∞ | a < ∞} {a : ℝ≥0∞ | a ≠ ∞}
⊢ (↑{a : ℝ≥0∞ | a < ∞} : Type) ≃ₜ ℝ≥0

Tactic:
refine (Homeomorph.setCongr ?_).trans neTopHomeomorphNNReal

Premises used: ENNReal.neTopHomeomorphNNReal, Homeomorph.trans, Homeomorph.setCongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b : ℝ≥0∞
r : ℝ≥0
x ε : ℝ≥0∞
⊢ Eq (α := Set ℝ≥0∞) {a : ℝ≥0∞ | a < ∞} {a : ℝ≥0∞ | a ≠ ∞}

Tactic:
simp only [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Eq (α := Filter ℝ≥0∞) (⨅ (l : ℝ≥0∞), ⨅ (_ : l < ∞), 𝓟 (Ioi l)) (⨅ (a : ℝ≥0∞), ⨅ (_ : a ≠ ∞), 𝓟 (Ioi a))

Tactic:
simp [lt_top_iff_ne_top, Ioi]

Premises used: Set.Ioi, lt_top_iff_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Eq (α := Filter ℝ≥0∞) (𝓝 ∞) (⨅ (r : ℝ≥0), 𝓟 (Ioi (↑r : ℝ≥0∞)))

Tactic:
nhds_top.trans <| iInf_ne_top _

Premises used: ENNReal.iInf_ne_top, ENNReal.nhds_top, Eq.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ HasBasis (α := ℝ≥0∞) (𝓝 ∞) (fun (a : ℝ≥0∞) ↦ a < ∞) fun (a : ℝ≥0∞) ↦ Ioi a

Tactic:
_root_.nhds_top_basis

Premises used: nhds_top_basis
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
⊢ Tendsto m f (𝓝 ∞) ↔ ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, (↑x : ℝ≥0∞) < m a

Tactic:
simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]

Premises used: ENNReal.nhds_top', Set.mem_Ioi, Filter.tendsto_principal, Filter.tendsto_iInf
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
h : ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, (↑x : ℝ≥0∞) < m a
n : ℕ
⊢ ∀ᶠ (a : α) in f, (↑n : ℝ≥0∞) < m a

Tactic:
simpa only [ENNReal.coe_natCast] using h n

Premises used: Nat.cast, ENNReal.coe_natCast
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, (↑n : ℝ≥0∞) < m a
x : ℝ≥0
n : ℕ
hn : x < (↑n : ℝ≥0)
x_1 : α
rwa : (↑x : ℝ≥0∞) < (↑(↑n : ℝ≥0) : ℝ≥0∞)
rwa₁ rwa₂ rwa₃ rwa₄ : x < (↑n : ℝ≥0)
⊢ (↑x : ℝ≥0∞) < (↑n : ℝ≥0∞)

Tactic:
rwa [← ENNReal.coe_natCast, coe_lt_coe]

Premises used: ENNReal.coe_lt_coe, ENNReal.coe_natCast
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, (↑n : ℝ≥0∞) < m a
⊢ Tendsto m f (𝓝 ∞)

Tactic:
tendsto_nhds_top_iff_nat.2 h

Premises used: Iff.mpr, ENNReal.tendsto_nhds_top_iff_nat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)) atTop (𝓝 ∞)

Tactic:
tendsto_nhds_top fun n =>
    mem_atTop_sets.2 ⟨n + 1, fun _m hm => mem_setOf.2 <| Nat.cast_lt.2 <| Nat.lt_of_succ_le hm⟩

Premises used: Iff.mpr, Filter.mem_atTop_sets, Nat.lt_of_succ_le, Set.mem_setOf, HAdd.hAdd, Exists.intro, OfNat.ofNat, Nat.cast_lt, ENNReal.tendsto_nhds_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ≥0
l : Filter α
rw : (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, (↑x : ℝ≥0∞) < (↑(f a) : ℝ≥0∞)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) l (𝓝 ∞) ↔ Tendsto f l atTop

Tactic:
rw [tendsto_nhds_top_iff_nnreal, atTop_basis_Ioi.tendsto_right_iff]

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

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (f x)) l (𝓝 ∞) ↔ Tendsto f l atTop

Tactic:
tendsto_coe_nhds_top.trans Real.tendsto_toNNReal_atTop_iff

Premises used: Real.tendsto_toNNReal_atTop_iff, ENNReal.ofReal, Iff.trans, ENNReal.tendsto_coe_nhds_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Tendsto ENNReal.ofReal atTop (𝓝 ∞)

Tactic:
tendsto_ofReal_nhds_top.2 tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, ENNReal.tendsto_ofReal_nhds_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Eq (α := Filter ℝ≥0∞) (⨅ (l : ℝ≥0∞), ⨅ (_ : ⊥ < l), 𝓟 (Iio l)) (⨅ (a : ℝ≥0∞), ⨅ (_ : a ≠ 0), 𝓟 (Iio a))

Tactic:
simp [pos_iff_ne_zero, Iio]

Premises used: Set.Iio, pos_iff_ne_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ HasBasis (α := ℝ≥0∞) (𝓝 0) (fun (a : ℝ≥0∞) ↦ 0 < a) fun (a : ℝ≥0∞) ↦ Iio a

Tactic:
nhds_bot_basis

Premises used: nhds_bot_basis
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ HasBasis (𝓝 0) (fun (a : ℝ≥0∞) ↦ 0 < a) Iic

Tactic:
nhds_bot_basis_Iic

Premises used: nhds_bot_basis_Iic
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
r : ℝ≥0
⊢ (𝓝[>] (↑r : ℝ≥0∞)).NeBot

Tactic:
nhdsGT_neBot_of_exists_gt ⟨∞, ENNReal.coe_lt_top⟩

Premises used: Exists.intro, nhdsGT_neBot_of_exists_gt, Top.top, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ NeBot (α := ℝ≥0∞) (𝓝[>] 0)

Tactic:
nhdsGT_coe_neBot

Premises used: ENNReal.nhdsGT_coe_neBot
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ NeBot (α := ℝ≥0∞) (𝓝[>] 1)

Tactic:
nhdsGT_coe_neBot

Premises used: ENNReal.nhdsGT_coe_neBot
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
⊢ NeBot (α := ℝ≥0∞) (𝓝[>] (↑n : ℝ≥0∞))

Tactic:
nhdsGT_coe_neBot

Premises used: ENNReal.ofNNReal, ENNReal.nhdsGT_coe_neBot, WithTop.some
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ NeBot (α := ℝ≥0∞) (𝓝[>] OfNat.ofNat n)

Tactic:
nhdsGT_coe_neBot

Premises used: ENNReal.ofNNReal, ENNReal.nhdsGT_coe_neBot, WithTop.some
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
inst : NeZero x
⊢ (𝓝[<] x).NeBot

Tactic:
nhdsLT_neBot_of_exists_lt ⟨0, NeZero.pos x⟩

Premises used: nhdsLT_neBot_of_exists_lt, Exists.intro, NeZero.pos, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
inl :
  ∀ (xt : Ne (α := ℝ≥0∞) 0 ∞), HasBasis (α := ℝ≥0∞) (𝓝 0) (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (0 - ε) (0 + ε)
inr : ∀ (x0 : 0 < x), (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)

Tactic:
rcases eq_zero_or_pos x with rfl | x0

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
xt : Ne (α := ℝ≥0∞) 0 ∞
inl : HasBasis (α := ℝ≥0∞) (𝓝 ⊥) (fun (x : ℝ≥0∞) ↦ ⊥ < x) fun (ε : ℝ≥0∞) ↦ Iic ε
⊢ HasBasis (α := ℝ≥0∞) (𝓝 0) (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (0 - ε) (0 + ε)

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

Premises used: ENNReal.bot_eq_zero, bot_lt_iff_ne_bot, zero_add, Set.Icc_bot, zero_tsub
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
xt : Ne (α := ℝ≥0∞) 0 ∞
⊢ HasBasis (α := ℝ≥0∞) (𝓝 ⊥) (fun (x : ℝ≥0∞) ↦ ⊥ < x) fun (ε : ℝ≥0∞) ↦ Iic ε

Tactic:
nhds_bot_basis_Iic

Premises used: nhds_bot_basis_Iic
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
xt : Ne (α := ℝ≥0∞) 0 ∞
⊢ HasBasis (α := ℝ≥0∞) (𝓝 ⊥) (fun (x : ℝ≥0∞) ↦ ⊥ < x) fun (ε : ℝ≥0∞) ↦ Iic ε

Tactic:
exact nhds_bot_basis_Iic

Premises used: nhds_bot_basis_Iic
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)

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

Premises used: nhds_basis_Ioo', Ne.lt_top, Exists.intro, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
inr : ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.1 < x ∧ x < i.2 → ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.1 i.2
inr₁ : ∀ (ε : ℝ≥0∞) (ε0 : ε ≠ 0), ∃ (i : ℝ≥0∞ × ℝ≥0∞), (i.1 < x ∧ x < i.2) ∧ Ioo i.1 i.2 ⊆ Icc (x - ε) (x + ε)
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)

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

Premises used: nhds_basis_Ioo', Ne.lt_top, Exists.intro, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
inr :
  ∀ (ε : ℝ≥0∞) (ε0 : 0 < ε) (hε : ε < x - (a, b).1),
    ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
⊢ ∃ (i' : ℝ≥0∞), 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ε⟩

Premises used: exists_between, tsub_pos_of_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
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
inr :
  ∀ (δ : ℝ≥0) (δ0 : 0 < δ) (hδ : x + (↑δ : ℝ≥0∞) < (a, b).2),
    ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
⊢ ∃ (i' : ℝ≥0∞), 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δ⟩

Premises used: ENNReal.lt_iff_exists_add_pos_lt, Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
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 + (↑δ : ℝ≥0∞) < (a, b).2
⊢ ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

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

Premises used: Iff.mpr, ENNReal.ofNNReal, lt_min, LT.lt.ne', ENNReal.coe_pos, And.intro, Exists.intro, Set.Icc_subset_Ioo, Min.min