awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x * a

Tactic:
continuous_iff_continuousAt.2 fun _ => ENNReal.continuousAt_mul_const (Or.inl ha)

Premises used: Iff.mpr, ENNReal.continuousAt_mul_const, Or.inl, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
c : ℝ≥0∞
c_ne_zero : c ≠ 0
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x / c

Tactic:
ENNReal.continuous_mul_const <| ENNReal.inv_ne_top.2 c_ne_zero

Premises used: Iff.mpr, ENNReal.inv_ne_top, DivInvMonoid.div', ENNReal.continuous_mul_const
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) a 0

Tactic:
simp [continuous_const]

Premises used: continuous_const
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
succ : ∀ (x : ℝ≥0∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ n * a) x
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ (n + 1)

Tactic:
simp_rw [pow_add, pow_one, continuous_iff_continuousAt]

Premises used: pow_add, pow_one, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ n * a) x

Tactic:
ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_

Premises used: ENNReal.Tendsto.mul, ContinuousAt, Filter.tendsto_id, Continuous.tendsto
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
succ : x ^ n ≠ 0 ∨ x ≠ ∞
succ₁ : x ≠ 0 ∨ x ^ n ≠ ∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ n * a) x

Tactic:
refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_

Premises used: ENNReal.Tendsto.mul, Filter.tendsto_id, Continuous.tendsto
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
pos : ∀ (H : x = 0), x ^ n ≠ 0 ∨ x ≠ ∞
neg : ∀ (H : ¬x = 0), x ^ n ≠ 0 ∨ x ≠ ∞
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

Tactic:
by_cases H : x = 0
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
pos : ∀ (H : x = 0), x ≠ 0 ∨ x ^ n ≠ ∞
neg : ∀ (H : ¬x = 0), x ≠ 0 ∨ x ^ n ≠ ∞
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

Tactic:
by_cases H : x = 0
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

Tactic:
simp only [H, zero_ne_top, Ne, or_true, not_false_iff]

Premises used: ENNReal.zero_ne_top, Ne, not_false_iff, or_true
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

Tactic:
Or.inl fun h => H (eq_zero_of_pow_eq_zero h)

Premises used: Or.inl, eq_zero_of_pow_eq_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

Tactic:
exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)

Premises used: Or.inl, eq_zero_of_pow_eq_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

Tactic:
simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]

Premises used: false_and, ENNReal.zero_ne_top, Ne, false_or, not_true, not_false_iff, ENNReal.pow_eq_top_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

Tactic:
simp only [H, true_or, Ne, not_false_iff]

Premises used: true_or, Ne, not_false_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
zero : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) a 0
succ :
  ∀ (n : ℕ) (IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n), Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ (n + 1)
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n

Tactic:
induction n with
  | zero => simp [continuous_const]
  | succ n IH =>
    simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
    intro x
    refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
    · simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
    · exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)
    · simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]
    · simp only [H, true_or, Ne, not_false_iff]

Premises used: true_or, continuous_const, false_and, ENNReal.zero_ne_top, pow_add, Ne, false_or, pow_one, not_true, not_false_iff, or_true, ENNReal.pow_eq_top_iff, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x y : ℝ≥0∞
hp : Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, y)
⊢ ¬(x = ∞ ∧ y = ∞)

Tactic:
simp only [Ne, Set.mem_setOf_eq, Prod.mk_inj] at hp

Premises used: Prod.mk_inj, Ne, Set.mem_setOf_eq
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x y : ℝ≥0∞
hp : ¬(x = ∞ ∧ y = ∞)
⊢ ContinuousWithinAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, y)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds (tendsto_sub (not_and_or.mp hp))

Premises used: ContinuousWithinAt, tendsto_nhdsWithin_of_tendsto_nhds, ENNReal.tendsto_sub, not_and_or, Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x y : ℝ≥0∞
hp : ¬(x = ∞ ∧ y = ∞)
⊢ ContinuousWithinAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, y)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (tendsto_sub (not_and_or.mp hp))

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, ENNReal.tendsto_sub, not_and_or, Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
change : Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) (uncurry Sub.sub ∘ fun (x : ℝ≥0∞) ↦ (a, x))
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ a - x

Tactic:
change Continuous (Function.uncurry Sub.sub ∘ (a, ·))

Premises used: Continuous, Function.comp, Prod.mk, Sub.sub, Function.uncurry
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) (uncurry Sub.sub ∘ fun (x : ℝ≥0∞) ↦ (a, x))

Tactic:
continuousOn_sub.comp_continuous (.prodMk_right a) fun x => ?_

Premises used: ContinuousOn.comp_continuous, ENNReal.continuousOn_sub, Continuous.prodMk_right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
refine : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (a, x)
⊢ Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) (uncurry Sub.sub ∘ fun (x : ℝ≥0∞) ↦ (a, x))

Tactic:
refine continuousOn_sub.comp_continuous (.prodMk_right a) fun x => ?_

Premises used: ContinuousOn.comp_continuous, ENNReal.continuousOn_sub, Continuous.prodMk_right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
x : ℝ≥0∞
⊢ Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (a, x)

Tactic:
simp only [a_ne_top, Ne, mem_setOf_eq, Prod.mk_inj, false_and, not_false_iff]

Premises used: false_and, Prod.mk_inj, Ne, Set.mem_setOf_eq, not_false_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑a : ℝ≥0∞) - x

Tactic:
continuous_sub_left coe_ne_top

Premises used: ENNReal.continuous_sub_left, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
⊢ Eq (α := (x : ℝ≥0∞) → ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ a - x) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (a, x))

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
rw :
  ContinuousOn (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (a, x))
    {x : ℝ≥0∞ | x ≠ ∞}
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ a - x) {x : ℝ≥0∞ | x ≠ ∞}

Tactic:
rw [show (fun x => a - x) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨a, x⟩ by rfl]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
⊢ ContinuousOn (Y := ℝ≥0∞ × ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ (a, x)) {x : ℝ≥0∞ | x ≠ ∞}

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
apply : MapsTo (β := ℝ≥0∞ × ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ (a, x)) {x : ℝ≥0∞ | x ≠ ∞} {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)}
⊢ ContinuousOn (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (a, x))
    {x : ℝ≥0∞ | x ≠ ∞}

Tactic:
apply continuousOn_sub.comp (by fun_prop)

Premises used: ENNReal.continuousOn_sub, ContinuousOn.comp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
h : Membership.mem (γ := Set ℝ≥0∞) {x : ℝ≥0∞ | x ≠ ∞} ∞
⊢ False

Tactic:
h none_eq_top

Premises used: ENNReal.none_eq_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
h : Membership.mem (γ := Set ℝ≥0∞) {x : ℝ≥0∞ | x ≠ ∞} ∞
⊢ False

Tactic:
exact h none_eq_top

Premises used: ENNReal.none_eq_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
pos : ∀ (a_infty : a = ∞), Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
neg : ∀ (a_infty : ¬a = ∞), Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a

Tactic:
by_cases a_infty : a = ∞
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_infty : a = ∞
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a

Tactic:
simp [a_infty, continuous_const, tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le, continuous_const
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Eq (α := (x : ℝ≥0∞) → ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x - a) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (x, a))

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_infty : ¬a = ∞
neg : Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (x, a))
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a

Tactic:
rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous (Y := ℝ≥0∞ × ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (x, a)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_infty : ¬a = ∞
neg : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, a)
⊢ Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (x, a))

Tactic:
apply continuousOn_sub.comp_continuous (by fun_prop)

Premises used: ContinuousOn.comp_continuous, ENNReal.continuousOn_sub
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
a_infty : ¬a = ∞
x : ℝ≥0∞
⊢ Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, a)

Tactic:
simp only [a_infty, Ne, mem_setOf_eq, Prod.mk_inj, and_false, not_false_iff]

Premises used: Prod.mk_inj, Ne, Set.mem_setOf_eq, and_false, not_false_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a : ℝ≥0∞
n : ℕ
hm : Tendsto m f (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ m x ^ n) f (𝓝 (a ^ n))

Tactic:
((ENNReal.continuous_pow n).tendsto a).comp hm

Premises used: ENNReal.continuous_pow, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
⊢ Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))

Tactic:
have : Tendsto (· * x) (𝓝[<] 1) (𝓝 (1 * x)) :=
    (ENNReal.continuousAt_mul_const (Or.inr one_ne_zero)).mono_left inf_le_left
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))
⊢ Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)

Tactic:
rw [one_mul] at this

Premises used: one_mul
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y

Tactic:
le_of_tendsto this (eventually_nhdsWithin_iff.2 <| Eventually.of_forall h)

Premises used: Iff.mpr, Filter.Eventually.of_forall, le_of_tendsto, eventually_nhdsWithin_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y

Tactic:
exact le_of_tendsto this (eventually_nhdsWithin_iff.2 <| Eventually.of_forall h)

Premises used: Iff.mpr, Filter.Eventually.of_forall, le_of_tendsto, eventually_nhdsWithin_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
x : ι → ℝ≥0∞
l : Filter ι
⊢ (limsup x l)⁻¹ = liminf (fun (i : ι) ↦ (x i)⁻¹) l

Tactic:
OrderIso.invENNReal.limsup_apply

Premises used: OrderIso.invENNReal, Filter.limsInf, OrderIso.limsup_apply, Filter.liminf, setOf, ENNReal, WithTop, ite
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
x : ι → ℝ≥0∞
l : Filter ι
⊢ (liminf x l)⁻¹ = limsup (fun (i : ι) ↦ (x i)⁻¹) l

Tactic:
OrderIso.invENNReal.liminf_apply

Premises used: Filter.limsSup, OrderIso.invENNReal, setOf, OrderIso.liminf_apply, Filter.limsup, ENNReal, WithTop, ite
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
n : ℕ
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ Int.negSucc n

Tactic:
simpa using (ENNReal.continuous_pow _).inv

Premises used: ENNReal.continuous_pow, Continuous.inv
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
apply : a ≠ 0 ∨ b⁻¹ ≠ ∞
apply₁ : b⁻¹ ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun (a : α) ↦ ma a / mb a) f (𝓝 (a / b))

Tactic:
apply Tendsto.mul hma _ (tendsto_inv_iff.2 hmb) _

Premises used: Iff.mpr, tendsto_inv_iff, ENNReal.Tendsto.mul
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ a ≠ 0 ∨ b⁻¹ ≠ ∞

Tactic:
simp [ha, hb]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ b⁻¹ ≠ 0 ∨ a ≠ ∞

Tactic:
simp [ha, hb]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
apply : b⁻¹ ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun (b : α) ↦ a / m b) f (𝓝 (a / b))

Tactic:
apply Tendsto.const_mul (tendsto_inv_iff.2 hm)

Premises used: Iff.mpr, tendsto_inv_iff, ENNReal.Tendsto.const_mul
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ b⁻¹ ≠ 0 ∨ a ≠ ∞

Tactic:
simp [hb]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
apply : a ≠ 0 ∨ b⁻¹ ≠ ∞
⊢ Tendsto (fun (x : α) ↦ m x / b) f (𝓝 (a / b))

Tactic:
apply Tendsto.mul_const hm

Premises used: ENNReal.Tendsto.mul_const
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ a ≠ 0 ∨ b⁻¹ ≠ ∞

Tactic:
simp [ha]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 0)

Tactic:
ENNReal.inv_top ▸ tendsto_inv_iff.2 tendsto_nat_nhds_top

Premises used: Iff.mpr, tendsto_inv_iff, Eq.rec, ENNReal.tendsto_nat_nhds_top, ENNReal.inv_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
r : ℝ≥0
b : ℝ≥0∞
⊢ Tendsto (fun (b : ℝ≥0∞) ↦ (↑r : ℝ≥0∞) - b) (𝓝 b) (𝓝 ((↑r : ℝ≥0∞) - b))

Tactic:
continuous_nnreal_sub.tendsto _

Premises used: ENNReal.continuous_nnreal_sub, Continuous.tendsto
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ ∃ (s : Set ℝ≥0∞), s.Countable ∧ Dense s ∧ (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s

Tactic:
exists_countable_dense_no_bot_top ℝ≥0∞

Premises used: ENNReal, exists_countable_dense_no_bot_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
obtain :
  ∀ (s : Set ℝ≥0∞) (s_count : s.Countable) (s_dense : Dense s)
    (hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s),
    ∃ (s : Set ℝ≥0∞), s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s
⊢ ∃ (s : Set ℝ≥0∞), s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s

Tactic:
obtain ⟨s, s_count, s_dense, hs⟩ :
    ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s :=
    exists_countable_dense_no_bot_top ℝ≥0∞

Premises used: ENNReal, exists_countable_dense_no_bot_top, Set
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
h : 0 ∈ s
⊢ IsBot (α := ℝ≥0∞) 0

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
h : ∞ ∈ s
⊢ IsTop (α := ℝ≥0∞) ∞

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
⊢ ∃ (s : Set ℝ≥0∞), s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s

Tactic:
exact ⟨s, s_count, s_dense, fun h => hs.1 0 (by simp) h, fun h => hs.2 ∞ (by simp) h⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
by_contra! : ∀ (h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1), False
⊢ ∃ (R : ℝ), ∃ᶠ (n : ι) in l, x n < R

Tactic:
by_contra! h
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
⊢ IsCobounded (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) (map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l)

Tactic:
isBoundedDefault
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
refine :
  ∀ (r : ℝ≥0), ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n
⊢ False

Tactic:
refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)

Premises used: Filter.le_limsInf_of_le, ENNReal.eq_top_of_forall_nnreal_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
simp : ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n

Tactic:
simp only [eventually_map, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe, Filter.eventually_map
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
i : ι
hi : (↑r : ℝ) ≤ x i
⊢ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x i)

Tactic:
hi.trans (le_abs_self (x i))

Premises used: le_abs_self, LE.le.trans, NNReal.toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ (↑r : ℝ) ≤ x x_3) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)) x_2} x_1}
      a
h₂ h₃ : ∀ (i : ι) (hi : (↑r : ℝ) ≤ x i), r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x i)
⊢ ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)

Tactic:
filter_upwards [h r] with i hi using hi.trans (le_abs_self (x i))

Premises used: NNReal.toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
by_contra! : ∀ (h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R), False
⊢ ∃ (R : ℝ), ∃ᶠ (n : ι) in l, R < x n

Tactic:
by_contra! h
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
⊢ IsCobounded (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) (map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l)

Tactic:
isBoundedDefault
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
refine :
  ∀ (r : ℝ≥0), ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n
⊢ False

Tactic:
refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)

Premises used: Filter.le_limsInf_of_le, ENNReal.eq_top_of_forall_nnreal_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
simp : ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n

Tactic:
simp only [eventually_map, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe, Filter.eventually_map
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
i : ι
hi : x i ≤ -(↑r : ℝ)
⊢ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x i)

Tactic:
(le_neg.1 hi).trans (neg_le_abs _)

Premises used: le_neg, neg_le_abs, Iff.mp, LE.le.trans, NNReal.toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ x x_3 ≤ -(↑r : ℝ)) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)) x_2} x_1}
      a
h₂ h₃ : ∀ (i : ι) (hi : x i ≤ -(↑r : ℝ)), r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x i)
⊢ ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)

Tactic:
filter_upwards [h (-r)] with i hi using (le_neg.1 hi).trans (neg_le_abs _)

Premises used: NNReal.toReal, Neg.neg
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (i : ι) ↦ |x i|
⊢ ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x ∨ ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x

Tactic:
rw [isBoundedUnder_le_abs, not_and_or] at hbdd

Premises used: not_and_or, Filter.isBoundedUnder_le_abs