awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
mp :
  ∀ (C : ℝ) (hC₀ : C > 0) (hC : IsBigOWith.{u_1, u_9, u_6} (E := E'') C l (fun (_x : α) ↦ c) f'),
    ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
rcases h.exists_pos with ⟨C, hC₀, hC⟩

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith.{u_1, u_9, u_6} (E := E'') C l (fun (_x : α) ↦ c) f'
⊢ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, HDiv.hDiv, And.intro, Exists.intro, div_pos
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith.{u_1, u_9, u_6} (E := E'') C l (fun (_x : α) ↦ c) f'
mp : ∀ᶠ (x : α) in l, ‖c‖ / C ≤ ‖f' x‖
⊢ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith.{u_1, u_9, u_6} (E := E'') C l (fun (_x : α) ↦ c) f'
⊢ ∀ᶠ (x : α) in l, ‖c‖ / C ≤ ‖f' x‖

Tactic:
hC.bound.mono fun x => (div_le_iff₀' hC₀).2

Premises used: Iff.mpr, Filter.Eventually.mono, Asymptotics.IsBigOWith.bound, div_le_iff₀'
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith.{u_1, u_9, u_6} (E := E'') C l (fun (_x : α) ↦ c) f'
⊢ ∀ᶠ (x : α) in l, ‖c‖ / C ≤ ‖f' x‖

Tactic:
exact hC.bound.mono fun x => (div_le_iff₀' hC₀).2

Premises used: Iff.mpr, Filter.Eventually.mono, Asymptotics.IsBigOWith.bound, div_le_iff₀'
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'

Tactic:
IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)

Premises used: Norm.norm, HDiv.hDiv, Filter.Eventually.mono, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
mpr : ∀ (x : α) (hx : b ≤ ‖f' x‖), ‖c‖ ≤ ‖c‖ / b * ‖f' x‖
⊢ IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'

Tactic:
refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)

Premises used: Norm.norm, HDiv.hDiv, Filter.Eventually.mono, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
mpr : ‖c‖ ≤ ‖c‖ * (‖f' x‖ / b)
⊢ ‖c‖ ≤ ‖c‖ / b * ‖f' x‖

Tactic:
rw [div_mul_eq_mul_div, mul_div_assoc]

Premises used: mul_div_assoc, div_mul_eq_mul_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ * (‖f' x‖ / b)

Tactic:
le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)

Premises used: Iff.mpr, le_mul_of_one_le_right, one_le_div, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ * (‖f' x‖ / b)

Tactic:
exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)

Premises used: Iff.mpr, le_mul_of_one_le_right, one_le_div, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
l : Filter α
hfg : f'' =O[l] g''
hg : Tendsto g'' l (𝓝 0)
⊢ Tendsto f'' l (𝓝 0)

Tactic:
(isLittleO_one_iff ℝ).1 <| hfg.trans_isLittleO <| (isLittleO_one_iff ℝ).2 hg

Premises used: Iff.mpr, Real, Iff.mp, Asymptotics.IsBigO.trans_isLittleO, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
l : Filter α
hfg : f'' =o[l] g''
hg : Tendsto g'' l (𝓝 0)
⊢ Tendsto f'' l (𝓝 0)

Tactic:
hfg.isBigO.trans_tendsto hg

Premises used: Asymptotics.IsLittleO.isBigO, Asymptotics.IsBigO.trans_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
inst_2 : One F''
inst_3 : NeZero.{u_10} (R := F'') 1
⊢ IsLittleO.{u_9, u_9, u_10} (E := E'') (F := F'') (𝓝 0) (fun (x : E'') ↦ x) 1

Tactic:
isLittleO_id_const one_ne_zero

Premises used: Asymptotics.isLittleO_id_const, one_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_17
E : Type u_18
inst : NormedRing E
inst_1 : NormOneClass E
inst_2 : TopologicalSpace α
f : α → E
x : α
⊢ ContinuousAt f x ↔ IsLittleO.{u_17, u_18, u_18} (E := E) (F := E) (𝓝 x) (fun (y : α) ↦ f y - f x) fun (x : α) ↦ 1

Tactic:
simp [ContinuousAt, ← tendsto_sub_nhds_zero_iff]

Premises used: ContinuousAt, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
rcases : ∀ (C : ℝ) (_hC₀ : C > 0) (hC : IsBigOWith C l (f ^ n) (g ^ n)), f =O[l] g
⊢ f =O[l] g

Tactic:
rcases h.exists_pos with ⟨C, _hC₀, hC⟩

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
obtain : ∀ (c : ℝ) (hc₀ : 0 ≤ c) (hc : C ≤ c ^ n), f =O[l] g
⊢ f =O[l] g

Tactic:
obtain ⟨c : ℝ, hc₀ : 0 ≤ c, hc : C ≤ c ^ n⟩ :=
    ((eventually_ge_atTop _).and <| (tendsto_pow_atTop hn).eventually_ge_atTop C).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_ge_atTop, Filter.Tendsto.eventually_ge_atTop, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
c : ℝ
hc₀ : 0 ≤ c
hc : C ≤ c ^ n
⊢ f =O[l] g

Tactic:
(hC.of_pow hn hc hc₀).isBigO

Premises used: Asymptotics.IsBigOWith.of_pow, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
c : ℝ
hc₀ : 0 ≤ c
hc : C ≤ c ^ n
⊢ f =O[l] g

Tactic:
exact (hC.of_pow hn hc hc₀).isBigO

Premises used: Asymptotics.IsBigOWith.of_pow, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
rw : ∃ (c : ℝ), IsBigOWith c l (f ^ n) (f ^ m)
⊢ (f ^ n) =O[l] (f ^ m)

Tactic:
rw [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ ∃ (c : ℝ), IsBigOWith c l (f ^ n) (f ^ m)

Tactic:
⟨1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
refine : IsBigOWith 1 l (f ^ n) (f ^ m)
⊢ ∃ (c : ℝ), IsBigOWith c l (f ^ n) (f ^ m)

Tactic:
refine ⟨1, ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
rw : ∀ᶠ (x : α) in l, ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖
⊢ IsBigOWith 1 l (f ^ n) (f ^ m)

Tactic:
rw [IsBigOWith_def]

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
x : α
hx : 1 x ≤ f x
⊢ ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖

Tactic:
simp [abs_eq_self.mpr (zero_le_one.trans hx), pow_le_pow_right₀ hx h]

Premises used: Iff.mpr, pow_le_pow_right₀, zero_le_one, LE.le.trans, abs_eq_self
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ ∀ᶠ (x : α) in l, ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖

Tactic:
exact hf.mono fun x hx ↦ by simp [abs_eq_self.mpr (zero_le_one.trans hx), pow_le_pow_right₀ hx h]

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
R : Type u_13
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedRing R
f' : α → E'
l : Filter α
inst_2 : Module R E'
inst_3 : IsBoundedSMul R E'
c' : R
⊢ IsBigOWith (E := E') ‖c'‖ l (fun (x : α) ↦ c' • f' x) f'

Tactic:
isBigOWith_of_le' _ fun _ => norm_smul_le _ _

Premises used: norm_smul_le, Asymptotics.isBigOWith_of_le'
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
R : Type u_13
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedRing R
f' : α → E'
l : Filter α
inst_2 : Module R E'
inst_3 : IsBoundedSMul R E'
c' : R
⊢ IsBigO (E := E') l (fun (x : α) ↦ c' • f' x) f'

Tactic:
(IsBigOWith.const_smul_self _).isBigO

Premises used: Asymptotics.IsBigOWith.const_smul_self, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
R : Type u_13
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedRing R
c : ℝ
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module R E'
inst_4 : IsBoundedSMul R E'
h : IsBigOWith c l f' g
c' : R
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (‖c'‖ * c) l (fun (x : α) ↦ c' • f' x) g

Tactic:
.trans (.const_smul_self _) h (norm_nonneg _)

Premises used: Asymptotics.IsBigOWith.const_smul_self, Asymptotics.IsBigOWith.trans, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
R : Type u_13
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedRing R
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module R E'
inst_4 : IsBoundedSMul R E'
h : f' =O[l] g
c : R
⊢ (c • f') =O[l] g

Tactic:
let ⟨_b, hb⟩ := h.isBigOWith
  (hb.const_smul_left _).isBigO

Premises used: Asymptotics.IsBigO, Asymptotics.IsBigOWith.const_smul_left, _private.0.Asymptotics.IsBigO.const_smul_left.match_1, Asymptotics.IsBigOWith.isBigO, HSMul.hSMul, Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
R : Type u_13
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedRing R
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module R E'
inst_4 : IsBoundedSMul R E'
h : f' =o[l] g
c : R
⊢ (c • f') =o[l] g

Tactic:
(IsBigO.const_smul_self _).trans_isLittleO h

Premises used: Asymptotics.IsBigO.trans_isLittleO, Asymptotics.IsBigO.const_smul_self
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ ‖c‖ ≠ 0

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ c • f' x) g ↔ f' =O[l] g

Tactic:
rw [← isBigO_norm_left]

Premises used: Asymptotics.isBigO_norm_left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
simp : IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =O[l] g
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =O[l] g

Tactic:
simp only [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : IsBigO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =O[l] g
rw₁ rw₂ : f' =O[l] g ↔ f' =O[l] g
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =O[l] g

Tactic:
rw [isBigO_const_mul_left_iff cne0, isBigO_norm_left]

Premises used: Asymptotics.isBigO_const_mul_left_iff, Asymptotics.isBigO_norm_left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =o[l] g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ c • f' x) g ↔ f' =o[l] g

Tactic:
rw [← isLittleO_norm_left]

Premises used: Asymptotics.isLittleO_norm_left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
simp : IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =o[l] g
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =o[l] g

Tactic:
simp only [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =o[l] g
rw₁ rw₂ : f' =o[l] g ↔ f' =o[l] g
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =o[l] g

Tactic:
rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]

Premises used: Asymptotics.isLittleO_norm_left, Asymptotics.isLittleO_const_mul_left_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ ‖c‖ ≠ 0

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =O[l] f'
⊢ (IsBigO.{u_1, u_3, u_6} (F := E') l f fun (x : α) ↦ c • f' x) ↔ f =O[l] f'

Tactic:
rw [← isBigO_norm_right]

Premises used: Asymptotics.isBigO_norm_right
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
simp : (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =O[l] f'

Tactic:
simp only [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖f' x‖) ↔ f =O[l] f'
rw₁ rw₂ : f =O[l] f' ↔ f =O[l] f'
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'

Tactic:
rw [isBigO_const_mul_right_iff cne0, isBigO_norm_right]

Premises used: Asymptotics.isBigO_norm_right, Asymptotics.isBigO_const_mul_right_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =o[l] f'
⊢ (IsLittleO.{u_1, u_3, u_6} (F := E') l f fun (x : α) ↦ c • f' x) ↔ f =o[l] f'

Tactic:
rw [← isLittleO_norm_right]

Premises used: Asymptotics.isLittleO_norm_right
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
simp : (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =o[l] f'
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =o[l] f'

Tactic:
simp only [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖f' x‖) ↔ f =o[l] f'
rw₁ rw₂ : f =o[l] f' ↔ f =o[l] f'
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =o[l] f'

Tactic:
rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]

Premises used: Asymptotics.isLittleO_const_mul_right_iff, Asymptotics.isLittleO_norm_right
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : IsBigOWith c l k₁ k₂
h₂ : IsBigOWith c' l f' g'
simp :
  ∀ (h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖) (h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖),
    ∀ᶠ (x : α) in l, ‖k₁ x • f' x‖ ≤ c * c' * ‖k₂ x • g' x‖
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') (c * c') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

Tactic:
simp only [IsBigOWith_def] at *

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
h : ∀ (a : α) (hx₁ : ‖k₁ a‖ ≤ c * ‖k₂ a‖) (hx₂ : ‖f' a‖ ≤ c' * ‖g' a‖), ‖k₁ a • f' a‖ ≤ c * c' * ‖k₂ a • g' a‖
⊢ ∀ᶠ (x : α) in l, ‖k₁ x • f' x‖ ≤ c * c' * ‖k₂ x • g' x‖

Tactic:
filter_upwards [h₁, h₂] with _ hx₁ hx₂
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a : α
hx₁ : ‖k₁ a‖ ≤ c * ‖k₂ a‖
hx₂ : ‖f' a‖ ≤ c' * ‖g' a‖
h : ‖k₁ a‖ * ‖f' a‖ ≤ c * c' * ‖k₂ a • g' a‖
⊢ ‖k₁ a • f' a‖ ≤ c * c' * ‖k₂ a • g' a‖

Tactic:
apply le_trans (norm_smul_le _ _)

Premises used: norm_smul_le, le_trans
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a : α
hx₁ : ‖k₁ a‖ ≤ c * ‖k₂ a‖
hx₂ : ‖f' a‖ ≤ c' * ‖g' a‖
⊢ ‖k₁ a‖ * ‖f' a‖ ≤ c * ‖k₂ a‖ * (c' * ‖g' a‖)

Tactic:
mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁)

Premises used: mul_le_mul, norm_nonneg, le_trans
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a : α
hx₁ : ‖k₁ a‖ ≤ c * ‖k₂ a‖
hx₂ : ‖f' a‖ ≤ c' * ‖g' a‖
h : c * c' * ‖k₂ a • g' a‖ = c * ‖k₂ a‖ * (c' * ‖g' a‖)
⊢ ‖k₁ a‖ * ‖f' a‖ ≤ c * c' * ‖k₂ a • g' a‖

Tactic:
convert! mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1

Premises used: mul_le_mul, norm_nonneg, le_trans