awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E'' : Type u_9
inst : Norm F
inst_1 : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ IsLittleO.{u_1, u_9, u_4} (E := E'') l (fun (_x : α) ↦ c) g ↔ Tendsto (β := ℝ) (fun (x : α) ↦ ‖g x‖) l atTop
have simp : IsLittleO.{u_1, u_9, u_4} (E := E'') l (fun (_x : α) ↦ c) g ↔ IsLittleO (E := ℝ) l (fun (_x : α) ↦ 1) g
Tactic: simp only [← isLittleO_one_left_iff ℝ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
⊢ IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ c) g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop
have inl : IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ 0) g'' ↔
  Eq.{u_9 + 1} (α := E'') 0 0 ∨ Tendsto (norm ∘ g'') l atTop
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
inl :
  IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ 0) g'' ↔
    Eq.{u_9 + 1} (α := E'') 0 0 ∨ Tendsto (norm ∘ g'') l atTop
⊢ IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ c) g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop
have inr : ∀ (hc : c ≠ 0), IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ c) g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ c) g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop
have inr : Tendsto (β := ℝ) (fun (x : α) ↦ ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop
Tactic: simp only [hc, false_or, isLittleO_const_left_of_ne hc]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
l : Filter α
inst_2 : l.NeBot
d : E''
c : F''
⊢ (IsLittleO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ d) fun (_x : α) ↦ c) ↔ d = 0
have this : ¬Tendsto (Function.const α ‖c‖) l atTop
Tactic: have : ¬Tendsto (Function.const α ‖c‖) l atTop :=
    not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
l : Filter α
inst_2 : l.NeBot
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ (IsLittleO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ d) fun (_x : α) ↦ c) ↔ d = 0
have simp : Tendsto (Function.comp.{u_1 + 1, u_10 + 1, 1} (β := F'') norm fun (_x : α) ↦ c) l atTop → d = 0
Tactic: simp only [isLittleO_const_left, or_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
⊢ f =o[l] g
have hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
Tactic: apply Asymptotics.isLittleO_of_tendsto'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
⊢ f =o[l] g
have a : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)
Tactic: apply Asymptotics.isLittleO_of_tendsto'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
⊢ ∀ᶠ (x : α) in l, g x = 0 → f x = 0
have hgf : ∀ (x : α), 1 ≤ g x / f x → g x = 0 → f x = 0
Tactic: apply (Filter.Tendsto.eventually_ge_atTop h 1).mono
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h_1 : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
x : α
h : 1 ≤ g x / f x
h0 : g x = 0
⊢ f x = 0
have h₁ : LE.le.{u_17} (α := 𝕜) 1 0
Tactic: simp only [h0, zero_div] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
⊢ Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)
have h₁ : ∀ (x : α), f x / g x = ((fun (r : 𝕜) ↦ r⁻¹) ∘ fun (x : α) ↦ g x / f x) x
Tactic: convert! Tendsto.comp tendsto_inv_atTop_zero h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
⊢ f =o[l] g
have refine : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / -f x) l atTop
Tactic: refine IsLittleO.of_neg_left (IsLittleO.of_tendsto_div_atTop ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
⊢ Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / -f x) l atTop
have rw : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ -(g x / -f x)) l atBot
Tactic: rw [← tendsto_neg_atBot_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
⊢ Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ -(g x / -f x)) l atBot
have h₁ : ∀ (x : α), -(g x / -f x) = g x / f x
Tactic: convert! h using 2
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v
have simp : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
Tactic: simp only [IsBigOWith_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
have refine : ∀ (x : α) (hx : ‖φ x‖ ≤ c), (fun (x : α) (a : R) ↦ ‖a‖ ≤ c * ‖v x‖) x ((φ * v) x)
Tactic: refine h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ (fun (x : α) (a : R) ↦ ‖a‖ ≤ c * ‖v x‖) x ((φ * v) x)
have simp : ‖φ x * v x‖ ≤ c * ‖v x‖
Tactic: simp only [Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x * v x‖ ≤ c * ‖v x‖
have refine : ‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖
Tactic: refine (norm_mul_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖
have ha : 0 ≤ ‖v x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v ↔ ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
have mp : IsBigOWith c l u v → ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ IsBigOWith c l u v ↔ ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
have mpr : (∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v) → IsBigOWith c l u v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
have 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
Tactic: use fun x => u x / v x
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
have h₁ : ∀ (y : α) (hy : ‖u y‖ ≤ c * ‖v y‖), norm.{u_15} (E := 𝕜) ((fun (x : α) ↦ u x / v x) y) ≤ c
Tactic: refine ⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v ↔ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
have mp : u =O[l] v → ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ u =O[l] v ↔ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
have mpr : (∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v) → u =O[l] v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
⊢ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
have mp : ∀ (c : ℝ) (hnnc : c ≥ 0) (hc : IsBigOWith c l u v),
  ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
Tactic: rcases h.exists_nonneg with ⟨c, hnnc, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
have mp : ∀ (φ : α → 𝕜) (hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) (huvφ : u =ᶠ[l] φ * v),
  ∃ (φ : α → 𝕜), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
Tactic: rcases hc.exists_eq_mul hnnc with ⟨φ, hφ, huvφ⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v ↔ ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v
have mp : u =o[l] v → ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
mp : u =o[l] v → ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v
⊢ u =o[l] v ↔ ∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v
have mpr : (∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v
have mpr : (∃ (φ : α → 𝕜), Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l u v
Tactic: simp only [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ IsBigOWith c l u v
have mpr : ∀ (hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε) (huvφ : u =ᶠ[l] φ * v) ⦃c : ℝ⦄ (hpos : 0 < c), IsBigOWith c l u v
Tactic: rw [NormedAddGroup.tendsto_nhds_zero] at hφ
Cleared hypotheses: hφ, huvφ, c, hpos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖
have obtain : ∀ (c : ℝ) (h₀ : c ≥ 0) (hc : IsBigOWith c l f g), IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖
Tactic: obtain ⟨c, h₀, hc⟩ := h.exists_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
have refine : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ‖f x / g x‖ c
Tactic: refine ⟨c, eventually_map.2 (hc.bound.mono fun x hx => ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
have rw : (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (‖f x‖ / ‖g x‖) c
Tactic: rw [norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
have refine : ∀ (h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x / g x‖), f =O[l] g
Tactic: refine ⟨div_isBoundedUnder_of_isBigO, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ f =O[l] g
have obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : ℝ) in map (fun (x : α) ↦ ‖f x / g x‖) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x c), f =O[l] g
Tactic: obtain ⟨c, hc⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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
⊢ f =O[l] g
have hc₁ : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
Tactic: simp only [eventually_map, norm_div] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
have refine : ∀ (x : α) (hx₁ : g x = 0 → f x = 0) (hx₂ : ‖f x‖ / ‖g x‖ ≤ c), ‖f x‖ ≤ c * ‖g x‖
Tactic: refine IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ ‖f x‖ ≤ c * ‖g x‖
have pos : ∀ (hgx : g x = 0), ‖f x‖ ≤ c * ‖g x‖
Tactic: by_cases hgx : g x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ‖f x‖ ≤ c * ‖g x‖
have neg : ∀ (hgx : ¬g x = 0), ‖f x‖ ≤ c * ‖g x‖
Tactic: by_cases hgx : g x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ Tendsto u l (𝓝 0)
have rwa : ∀ (h : Tendsto u l (𝓝 0)), Tendsto u l (𝓝 0)
Tactic: rwa [isLittleO_one_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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)
⊢ Tendsto u l (𝓝 0)
have suffices : IsLittleO.{u_1, u_6, u_15} (F := 𝕜) l u fun (_x : α) ↦ 1
Tactic: suffices h : u =o[l] fun _x => (1 : 𝕜) by
    rwa [isLittleO_one_iff] at h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ IsBigOWith C l f g
have simp : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
Tactic: simp only [IsBigOWith]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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 : α) in l, ‖f x‖ ≤ C * ‖g x‖
have apply : ∀ (x : α), C⁻¹ ≤ ((fun (a : 𝕜) ↦ ‖a‖) ∘ fun (x : α) ↦ g x / f x) x → ‖f x‖ ≤ C * ‖g x‖
Tactic: apply (((continuous_norm.tendsto _).comp h).eventually_const_le ha).mono
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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
⊢ ‖f x‖ ≤ C * ‖g x‖
have hx₁ : C⁻¹ ≤ ‖g x‖ / ‖f x‖
Tactic: simp only [Function.comp_apply, norm_div] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ‖f x‖ ≤ C * ‖g x‖
have pos : ∀ (hf : f x = 0), ‖f x‖ ≤ C * ‖g x‖
Tactic: by_cases hf : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ‖f x‖ ≤ C * ‖g x‖
have neg : ∀ (hf : ¬f x = 0), ‖f x‖ ≤ C * ‖g x‖
Tactic: by_cases hf : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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
⊢ ‖f x‖ ≤ C * ‖g x‖
have hx₁ : C ≤ 0
Tactic: simp [hf] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ ‖f x‖ ≤ C * ‖g x‖
have linarith : C * ‖g x‖ < ‖f x‖ → 0 - C + (C - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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
⊢ ‖f x‖ ≤ C * ‖g x‖
have hx₁ : C⁻¹ * ‖f x‖ ≤ ‖g x‖
Tactic: rw [le_div_iff₀ (by positivity)] at hx
Cleared hypotheses: hx, hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ (‖a‖⁻¹ + 1)⁻¹ < ‖a‖
have field_simp : 1 < 1 + ‖a‖
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ f =O[l] g
have obtain : ∀ (C : ℝ) (hC : 0 < C) (ha : C⁻¹ < ‖a‖), f =O[l] g
Tactic: obtain ⟨C, hC, ha⟩ : ∃ C, 0 < C ∧ C⁻¹ < ‖a‖ := ⟨‖a‖⁻¹ + 1, by positivity, by field_simp; simpa⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ f =O[l] g
have simp : ∃ (c : ℝ), IsBigOWith c l f g
Tactic: simp only [IsBigO]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
m n : ℕ
h : m < n
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ n) fun (x : 𝕜) ↦ x ^ m
have rcases : ∀ (p : ℕ) (hp0 : 0 < p) (h : m < m + p),
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ (m + p)) fun (x : 𝕜) ↦ x ^ m
Tactic: rcases lt_iff_exists_add.1 h with ⟨p, hp0 : 0 < p, rfl⟩
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ (m + p)) fun (x : 𝕜) ↦ x ^ m
have suffices : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ m * x ^ p) fun (x : 𝕜) ↦ x ^ m * HPow.hPow (α := 𝕜) 1 p
Tactic: suffices (fun x : 𝕜 => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p by
    simpa only [pow_add, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ n) fun (x : 𝕜) ↦ x
have h₁ : ∀ (x : 𝕜), x = HPow.hPow (β := ℕ) x 1
Tactic: convert! isLittleO_pow_pow h (𝕜 := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
⊢ IsLittleO (E := ℝ) (F := E') (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ x
have this : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ HPow.hPow (β := ℕ) ‖x‖ 1
Tactic: have := @isLittleO_norm_pow_norm_pow E' _ _ _ h