awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
mp : IsBigOWith c l u v → ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
mpr : (∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v) → IsBigOWith c l u v
⊢ IsBigOWith c l u v ↔ ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
constructor
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
h₁ : (∀ᶠ (x : α) in l, norm.{u_15} (E := 𝕜) ((fun (x : α) ↦ u x / v x) x) ≤ c) ∧ u =ᶠ[l] (fun (x : α) ↦ u x / v x) * v
⊢ ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
use fun x => u x / v x

Premises used: HDiv.hDiv
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ (∀ᶠ (x : α) in l, norm.{u_15} (E := 𝕜) ((fun (x : α) ↦ u x / v x) x) ≤ c) ∧ u =ᶠ[l] (fun (x : α) ↦ u x / v x) * v

Tactic:
⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩

Premises used: Asymptotics.IsBigOWith.eventually_mul_div_cancel, Filter.Eventually.mono, And.intro, Asymptotics.IsBigOWith.bound, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
h₁ : ∀ (y : α) (hy : ‖u y‖ ≤ c * ‖v y‖), norm.{u_15} (E := 𝕜) ((fun (x : α) ↦ u x / v x) y) ≤ c
⊢ (∀ᶠ (x : α) in l, norm.{u_15} (E := 𝕜) ((fun (x : α) ↦ u x / v x) x) ≤ c) ∧ u =ᶠ[l] (fun (x : α) ↦ u x / v x) * v

Tactic:
refine ⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
⊢ norm.{u_15} (E := 𝕜) ((fun (x : α) ↦ u x / v x) y) ≤ c

Tactic:
simpa using div_le_of_le_mul₀ (norm_nonneg _) hc hy

Premises used: div_le_of_le_mul₀, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v

Tactic:
isBigOWith_of_eq_mul φ hφ h

Premises used: Asymptotics.isBigOWith_of_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v

Tactic:
exact isBigOWith_of_eq_mul φ hφ h

Premises used: Asymptotics.isBigOWith_of_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
h : IsBigOWith c l u v
hc : 0 ≤ c
⊢ ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
(isBigOWith_iff_exists_eq_mul hc).mp h

Premises used: Asymptotics.isBigOWith_iff_exists_eq_mul, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
mp : u =O[l] v → ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
mpr : (∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v) → u =O[l] v
⊢ u =O[l] v ↔ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
constructor
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
mp :
  ∀ (c : ℝ) (hnnc : c ≥ 0) (hc : IsBigOWith c l u v),
    ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
⊢ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
rcases h.exists_nonneg with ⟨c, hnnc, hc⟩

Premises used: Asymptotics.IsBigO.exists_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
mp :
  ∀ (φ : α → 𝕜) (hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) (huvφ : u =ᶠ[l] φ * v),
    ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
⊢ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
rcases hc.exists_eq_mul hnnc with ⟨φ, hφ, huvφ⟩

Premises used: Asymptotics.IsBigOWith.exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
huvφ : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
⟨φ, ⟨c, hφ⟩, huvφ⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
huvφ : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
exact ⟨φ, ⟨c, hφ⟩, huvφ⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
huvφ : u =ᶠ[l] φ * v
c : ℝ
hφ : ∀ᶠ (x : ℝ) in map (norm ∘ φ) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x c
⊢ u =O[l] v

Tactic:
isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩

Premises used: Iff.mpr, Asymptotics.isBigOWith_of_eq_mul, Exists.intro, Asymptotics.isBigO_iff_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
huvφ : u =ᶠ[l] φ * v
c : ℝ
hφ : ∀ᶠ (x : ℝ) in map (norm ∘ φ) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x c
⊢ u =O[l] v

Tactic:
exact isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩

Premises used: Iff.mpr, Asymptotics.isBigOWith_of_eq_mul, Exists.intro, Asymptotics.isBigO_iff_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
mp : u =o[l] v → ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v
mpr : (∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v
⊢ u =o[l] v ↔ ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Tactic:
constructor
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v → ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Tactic:
fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩

Premises used: Asymptotics.IsLittleO.tendsto_div_nhds_zero, HDiv.hDiv, And.intro, Exists.intro, Asymptotics.IsLittleO.eventually_mul_div_cancel, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v → ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Tactic:
exact fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
mpr : (∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l u v
⊢ (∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v

Tactic:
simp only [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : Tendsto φ l (𝓝 0)
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
mpr : ∀ (hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε) (huvφ : u =ᶠ[l] φ * v) ⦃c : ℝ⦄ (hpos : 0 < c), IsBigOWith c l u v
⊢ IsBigOWith c l u v

Tactic:
rw [NormedAddGroup.tendsto_nhds_zero] at hφ

Premises used: NormedAddGroup.tendsto_nhds_zero
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Tactic:
isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

Premises used: le_of_lt, Asymptotics.isBigOWith_of_eq_mul, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Tactic:
exact isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

Premises used: le_of_lt, Asymptotics.isBigOWith_of_eq_mul, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
obtain :
  ∀ (c : ℝ) (h₀ : c ≥ 0) (hc : IsBigOWith c l f g),
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖

Tactic:
obtain ⟨c, h₀, hc⟩ := h.exists_nonneg

Premises used: Asymptotics.IsBigO.exists_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖

Tactic:
⟨c, eventually_map.2 (hc.bound.mono fun x hx => ?_)⟩

Premises used: Iff.mpr, Filter.IsBounded, Filter.eventually_map, Filter.Eventually.mono, Exists.intro, Asymptotics.IsBigOWith.bound, Filter.IsBoundedUnder
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
refine : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ‖f x / g x‖ c
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖

Tactic:
refine ⟨c, eventually_map.2 (hc.bound.mono fun x hx => ?_)⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
rw : ‖f x‖ / ‖g x‖ ≤ c
⊢ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ‖f x / g x‖ c

Tactic:
rw [norm_div]

Premises used: norm_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (‖f x‖ / ‖g x‖) c

Tactic:
div_le_of_le_mul₀ (norm_nonneg _) h₀ hx

Premises used: div_le_of_le_mul₀, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (‖f x‖ / ‖g x‖) c

Tactic:
exact div_le_of_le_mul₀ (norm_nonneg _) h₀ hx

Premises used: div_le_of_le_mul₀, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
⊢ f =O[l] g ↔ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖

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

Premises used: Asymptotics.div_isBoundedUnder_of_isBigO, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
refine : ∀ (h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖), f =O[l] g
⊢ f =O[l] g ↔ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖

Tactic:
refine ⟨div_isBoundedUnder_of_isBigO, fun h => ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖
obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : ℝ) in map (fun (x : α) ↦ ‖f x / g x‖) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x c), f =O[l] g
⊢ f =O[l] g

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (x : ℝ) in map (fun (x : α) ↦ ‖f x / g x‖) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c

Tactic:
simp only [eventually_map, norm_div] at hc

Premises used: Filter.eventually_map, norm_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
⊢ f =O[l] g

Tactic:
IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
refine : ∀ (x : α) (hx₁ : g x = 0 → f x = 0) (hx₂ : ‖f x‖ / ‖g x‖ ≤ c), ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
refine IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
pos : ∀ (hgx : g x = 0), ‖f x‖ ≤ c * ‖g x‖
neg : ∀ (hgx : ¬g x = 0), ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
by_cases hgx : g x = 0
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
hgx : g x = 0
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp [hx₁ hgx, hgx]
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
hgx : ¬g x = 0
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
(div_le_iff₀ (norm_pos_iff.2 hgx)).mp hx₂

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
hgx : ¬g x = 0
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
exact (div_le_iff₀ (norm_pos_iff.2 hgx)).mp hx₂

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : 𝕜
H : Tendsto (f / g) l (𝓝 c)
⊢ f =O[l] g

Tactic:
(isBigO_iff_div_isBoundedUnder hgf).2 <| H.norm.isBoundedUnder_le

Premises used: Iff.mpr, Filter.Tendsto.isBoundedUnder_le, Asymptotics.isBigO_iff_div_isBoundedUnder, Filter.Tendsto.norm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst : SeminormedAddCommGroup E'
inst_1 : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
h : IsLittleO.{u_1, u_6, u_15} (F := 𝕜) l u fun (_x : α) ↦ 1
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : Tendsto u l (𝓝 0)), Tendsto u l (𝓝 0)
⊢ Tendsto u l (𝓝 0)

Tactic:
rwa [isLittleO_one_iff] at h

Premises used: Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst : SeminormedAddCommGroup E'
inst_1 : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
suffices : IsLittleO.{u_1, u_6, u_15} (F := 𝕜) l u fun (_x : α) ↦ 1
⊢ Tendsto u l (𝓝 0)

Tactic:
suffices h : u =o[l] fun _x => (1 : 𝕜) by
    rwa [isLittleO_one_iff] at h
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst : SeminormedAddCommGroup E'
inst_1 : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ IsLittleO.{u_1, u_6, u_15} (F := 𝕜) l u fun (_x : α) ↦ 1

Tactic:
huv.trans_isBigO (hv.isBigO_one 𝕜)

Premises used: Filter.Tendsto.isBigO_one, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst : SeminormedAddCommGroup E'
inst_1 : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ IsLittleO.{u_1, u_6, u_15} (F := 𝕜) l u fun (_x : α) ↦ 1

Tactic:
exact huv.trans_isBigO (hv.isBigO_one 𝕜)

Premises used: Filter.Tendsto.isBigO_one, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
simp : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
⊢ IsBigOWith C l f g

Tactic:
simp only [IsBigOWith]

Premises used: Asymptotics.IsBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
apply : ∀ (x : α), C⁻¹ ≤ ((fun (a : 𝕜) ↦ ‖a‖) ∘ fun (x : α) ↦ g x / f x) x → ‖f x‖ ≤ C * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖

Tactic:
apply (((continuous_norm.tendsto _).comp h).eventually_const_le ha).mono

Premises used: Filter.Tendsto.eventually_const_le, Filter.Eventually.mono, Continuous.tendsto, Filter.Tendsto.comp, continuous_norm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ((fun (a : 𝕜) ↦ ‖a‖) ∘ fun (x : α) ↦ g x / f x) x
⊢ C⁻¹ ≤ ‖g x‖ / ‖f x‖

Tactic:
simp only [Function.comp_apply, norm_div] at hx

Premises used: norm_div, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
pos : ∀ (hf : f x = 0), ‖f x‖ ≤ C * ‖g x‖
neg : ∀ (hf : ¬f x = 0), ‖f x‖ ≤ C * ‖g x‖
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
by_cases hf : f x = 0
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : f x = 0
⊢ C ≤ 0

Tactic:
simp [hf] at hx
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hf : f x = 0
hx : C ≤ 0
linarith : C * ‖g x‖ < ‖f x‖ → 0 - C + (C - 0) = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
linarith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : ¬f x = 0
⊢ 0 < ‖f x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : ¬f x = 0
⊢ C⁻¹ * ‖f x‖ ≤ ‖g x‖

Tactic:
rw [le_div_iff₀ (by positivity)] at hx

Premises used: le_div_iff₀
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : ¬f x = 0
hx₁ : C⁻¹ * ‖f x‖ ≤ ‖g x‖
⊢ ¬f x = 0

Tactic:
rw [le_div_iff₀ (by positivity)] at hx

Premises used: le_div_iff₀
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ * ‖f x‖ ≤ ‖g x‖
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
field_simp at hx
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hf : ¬f x = 0
hx : ‖f x‖ ≤ C * ‖g x‖
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
hx
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hf : ¬f x = 0
hx : ‖f x‖ ≤ C * ‖g x‖
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
exact hx
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ 0 < ‖a‖⁻¹ + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
field_simp : 1 < 1 + ‖a‖
⊢ (‖a‖⁻¹ + 1)⁻¹ < ‖a‖

Tactic:
field_simp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ 1 < 1 + ‖a‖

Tactic:
simpa
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
obtain : ∀ (C : ℝ) (hC : 0 < C) (ha : C⁻¹ < ‖a‖), f =O[l] g
⊢ f =O[l] g

Tactic:
obtain ⟨C, hC, ha⟩ : ∃ C, 0 < C ∧ C⁻¹ < ‖a‖ := ⟨‖a‖⁻¹ + 1, by positivity, by field_simp; simpa⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
ha_1 : a ≠ 0
C : ℝ
hC : 0 < C
ha : C⁻¹ < ‖a‖
simp : ∃ (c : ℝ), IsBigOWith c l f g
⊢ f =O[l] g

Tactic:
simp only [IsBigO]

Premises used: Asymptotics.IsBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
ha_1 : a ≠ 0
C : ℝ
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ ∃ (c : ℝ), IsBigOWith c l f g

Tactic:
⟨C, isBigOWith_of_div_tendsto_nhds h hC ha⟩

Premises used: Asymptotics.isBigOWith_of_div_tendsto_nhds, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 a)
ha_1 : a ≠ 0
C : ℝ
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ ∃ (c : ℝ), IsBigOWith c l f g

Tactic:
exact ⟨C, isBigOWith_of_div_tendsto_nhds h hC ha⟩