awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun (x : 𝕜) ↦ f x⁻¹) atBot l
⊢ f = (fun (x : 𝕜) ↦ f x⁻¹) ∘ fun (x : 𝕜) ↦ x⁻¹

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (r : 𝕜) ↦ r⁻¹) atBot (𝓝[<] 0)

Tactic:
inv_atBot₀.le

Premises used: inv_atBot₀, Set.Mem, Eq.le, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (r : 𝕜) ↦ r⁻¹) atBot (𝓝 0)

Tactic:
tendsto_inv_atBot_nhdsLT_zero.mono_right inf_le_left

Premises used: tendsto_inv_atBot_nhdsLT_zero, inf_le_left, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
simp : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)

Tactic:
mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)

Premises used: tendsto_inv_atTop_zero, Eq.rec, MulZeroClass.mul_zero, Filter.Tendsto.mul, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)

Tactic:
exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
simp : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)

Tactic:
mul_zero a ▸ h.mul (tendsto_inv_atBot_zero.comp hg)

Premises used: Eq.rec, tendsto_inv_atBot_zero, MulZeroClass.mul_zero, Filter.Tendsto.mul, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)

Tactic:
exact mul_zero a ▸ h.mul (tendsto_inv_atBot_zero.comp hg)
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
g : α → 𝕜
hg : Tendsto g l atTop
r : 𝕜
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (n : α) ↦ r / g n) l (𝓝 0)

Tactic:
tendsto_const_nhds.div_atTop hg

Premises used: Filter.Tendsto.div_atTop, tendsto_const_nhds
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
g : α → 𝕜
hg : Tendsto g l atBot
r : 𝕜
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (n : α) ↦ r / g n) l (𝓝 0)

Tactic:
tendsto_const_nhds.div_atBot hg

Premises used: tendsto_const_nhds, Filter.Tendsto.div_atBot
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : α → 𝕜
h : Tendsto f l atBot
⊢ Tendsto f⁻¹ l (𝓝 0)

Tactic:
tendsto_inv_atBot_zero.comp h

Premises used: tendsto_inv_atBot_zero, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : α → 𝕜
h : Tendsto f l (𝓝[<] 0)
⊢ Tendsto f⁻¹ l atBot

Tactic:
tendsto_inv_nhdsLT_zero.comp h

Premises used: tendsto_inv_nhdsLT_zero, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
rw : Tendsto.{u_2, u_1} (β := 𝕜) (abs ∘ fun (x : α) ↦ f x * g x) l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l (𝓝 0)

Tactic:
rw [tendsto_zero_iff_abs_tendsto_zero]

Premises used: tendsto_zero_iff_abs_tendsto_zero
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (fun (x : α) ↦ |C * g x|) l (𝓝 |C * 0|)

Tactic:
(hg.const_mul C).abs

Premises used: Filter.Tendsto.abs, Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
h : 0 = |C * 0|
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)

Tactic:
convert! (hg.const_mul C).abs

Premises used: Filter.Tendsto.abs, Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
h : Eq.{u_1 + 1} (α := 𝕜) 0 |0|
⊢ 0 = |C * 0|

Tactic:
simp_rw [mul_zero, abs_zero]

Premises used: MulZeroClass.mul_zero, abs_zero
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)

Tactic:
have hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0) := by
    convert! (hg.const_mul C).abs
    simp_rw [mul_zero, abs_zero]
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
hgf : ∀ᶠ (b : α) in l, LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)
hfh : ∀ᶠ (b : α) in l, (abs ∘ fun (x : α) ↦ f x * g x) b ≤ |C * g b|
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (abs ∘ fun (x : α) ↦ f x * g x) l (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hC

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le'
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
x : α
h : |f x| ≤ C → LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) x)
⊢ |f x| ≤ C → LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) x)

Tactic:
_
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
x : α
h : |f x| ≤ C
⊢ LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) x)

Tactic:
abs_nonneg _

Premises used: abs, abs_nonneg
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ |f x| ≤ C) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (b : α) ↦ LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)) x} x}
      a
h₁ h₂ : ∀ (x : α), |f x| ≤ C → LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) x)
⊢ ∀ᶠ (b : α) in l, LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)

Tactic:
filter_upwards [hf] with x _ using abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
h : ∀ (x : α) (hx : |f x| ≤ C), (abs ∘ fun (x : α) ↦ f x * g x) x ≤ |C * g x|
⊢ ∀ᶠ (b : α) in l, (abs ∘ fun (x : α) ↦ f x * g x) b ≤ |C * g b|

Tactic:
filter_upwards [hf] with x hx
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
h : |f x| * |g x| ≤ |C| * |g x|
⊢ (abs ∘ fun (x : α) ↦ f x * g x) x ≤ |C * g x|

Tactic:
simp only [comp_apply, abs_mul]

Premises used: abs_mul, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ |f x| * |g x| ≤ |C| * |g x|

Tactic:
mul_le_mul_of_nonneg_right (hx.trans (le_abs_self C)) (abs_nonneg _)

Premises used: le_abs_self, mul_le_mul_of_nonneg_right, LE.le.trans, abs_nonneg
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ |f x| * |g x| ≤ |C| * |g x|

Tactic:
exact mul_le_mul_of_nonneg_right (hx.trans (le_abs_self C)) (abs_nonneg _)

Premises used: le_abs_self, mul_le_mul_of_nonneg_right, LE.le.trans, abs_nonneg
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
⊢ -C ≤ b

Tactic:
have hbC : -C ≤ b := neg_le.mpr (le_max_of_le_left (neg_le_abs b))
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
⊢ B ≤ C

Tactic:
have hBC : B ≤ C := le_max_of_le_right (le_abs_self B)
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
hBC : B ≤ C
apply : ∀ᶠ (x : α) in l, |f x| ≤ C
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l (𝓝 0)

Tactic:
apply bdd_le_mul_tendsto_zero' C _ hg

Premises used: bdd_le_mul_tendsto_zero'
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
hBC : B ≤ C
h : ∀ (a : α), b ≤ f a → f a ≤ B → |f a| ≤ C
⊢ ∀ᶠ (x : α) in l, |f x| ≤ C

Tactic:
filter_upwards [hb, hB]
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ (a : α), b ≤ f a → f a ≤ B → |f a| ≤ C

Tactic:
fun x hbx hBx ↦ abs_le.mpr ⟨hbC.trans hbx, hBx.trans hBC⟩

Premises used: Iff.mpr, abs_le, And.intro, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ (a : α), b ≤ f a → f a ≤ B → |f a| ≤ C

Tactic:
exact fun x hbx hBx ↦ abs_le.mpr ⟨hbC.trans hbx, hBx.trans hBC⟩

Premises used: Iff.mpr, abs_le, And.intro, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
simp : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)

Tactic:
bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop

Premises used: bdd_le_mul_tendsto_zero, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)

Tactic:
exact bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop

Premises used: bdd_le_mul_tendsto_zero, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c : 𝕜
hn : n < 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 0)

Tactic:
mul_zero c ▸ Filter.Tendsto.const_mul c (tendsto_zpow_atTop_zero hn)

Premises used: tendsto_zpow_atTop_zero, Eq.rec, Filter.Tendsto.const_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
inl : Tendsto (fun (x : 𝕜) ↦ c * HPow.hPow (β := ℕ) x 0) atTop (𝓝 d) ↔ (c = 0 ∨ Eq (α := ℕ) 0 0) ∧ c = d
inr : ∀ (hn : n ≠ 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
c d : 𝕜
⊢ Tendsto (fun (x : 𝕜) ↦ c * HPow.hPow (β := ℕ) x 0) atTop (𝓝 d) ↔ (c = 0 ∨ Eq (α := ℕ) 0 0) ∧ c = d

Tactic:
simp [tendsto_const_nhds_iff]

Premises used: tendsto_const_nhds_iff
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
inr : ∀ (hc : c < 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
inr₁ : Tendsto (fun (x : 𝕜) ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (Eq.{u_1 + 1} (α := 𝕜) 0 0 ∨ n = 0) ∧ 0 = d
inr₂ : ∀ (hc : 0 < c), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
rcases lt_trichotomy c 0 with (hc | rfl | hc)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ c * x ^ n) atTop atBot

Tactic:
have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
this : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ c * x ^ n) atTop atBot
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]

Premises used: not_tendsto_nhds_of_tendsto_atBot, LT.lt.ne
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun (x : 𝕜) ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (Eq.{u_1 + 1} (α := 𝕜) 0 0 ∨ n = 0) ∧ 0 = d

Tactic:
simp [tendsto_const_nhds_iff]

Premises used: tendsto_const_nhds_iff
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ c * x ^ n) atTop atTop

Tactic:
have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
this : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ c * x ^ n) atTop atTop
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn]

Premises used: not_tendsto_nhds_of_tendsto_atTop, LT.lt.ne'
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d

Tactic:
simp [tendsto_const_mul_pow_nhds_iff', hc]

Premises used: tendsto_const_mul_pow_nhds_iff'
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
refine_1 : ∀ (h : Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)), n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
refine_2 : ∀ (h : n = 0 ∧ c = d ∨ n < 0 ∧ d = 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun (x : 𝕜) ↦ c * x ^ Int.ofNat n) atTop (𝓝 d)
refine_1 : Int.ofNat n = 0 ∧ c = d
⊢ Int.ofNat n = 0 ∧ c = d ∨ Int.ofNat n < 0 ∧ d = 0

Tactic:
left
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun (x : 𝕜) ↦ c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d

Tactic:
simpa [tendsto_const_mul_pow_nhds_iff hc] using h

Premises used: tendsto_const_mul_pow_nhds_iff
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun (x : 𝕜) ↦ c * x ^ Int.negSucc n) atTop (𝓝 d)
⊢ Int.negSucc n < 0

Tactic:
have hn := Int.negSucc_lt_zero n
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun (x : 𝕜) ↦ c * x ^ Int.negSucc n) atTop (𝓝 d)
hn : Int.negSucc n < 0
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0

Tactic:
Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩

Premises used: tendsto_const_mul_zpow_atTop_zero, And.intro, tendsto_nhds_unique, Or.inr