awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
f'' : α → E''
l : Filter α
⊢ (IsLittleO.{u_1, u_9, u_7} (F := F') l f'' fun (_x : α) ↦ 0) ↔ f'' =ᶠ[l] 0

Tactic:
⟨fun h => isBigO_zero_right_iff.1 h.isBigO,
   fun h => IsLittleO.of_isBigOWith fun _c _hc => isBigOWith_zero_right_iff.2 h⟩

Premises used: Iff.mpr, Asymptotics.isBigO_zero_right_iff, Asymptotics.isBigOWith_zero_right_iff, Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsLittleO.isBigO, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
simp : ∀ᶠ (x : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖
⊢ IsBigOWith.{u_1, u_3, u_10} (E := E) (F := F'') (‖c‖ / ‖c'‖) l (fun (_x : α) ↦ c) fun (_x : α) ↦ c'

Tactic:
simp only [IsBigOWith_def]

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x} a
⊢ ∀ᶠ (x : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖

Tactic:
apply univ_mem'

Premises used: Filter.univ_mem'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
x : α
h : ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖
h₁ h₂ : ‖c‖ ≤ ‖c‖
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x} x

Tactic:
rw [mem_setOf, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hc')]

Premises used: Iff.mpr, div_mul_cancel₀, Set.mem_setOf, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ IsBigO.{u_1, u_3, u_10} (E := E) (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ c'

Tactic:
(isBigOWith_const_const c hc' l).isBigO

Premises used: Asymptotics.IsBigOWith.isBigO, Asymptotics.isBigOWith_const_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst_2 : l.NeBot
inl :
  (IsBigO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ 0) ↔
    Eq.{u_10 + 1} (α := F'') 0 0 → c = 0
inr :
  ∀ (hc' : c' ≠ 0),
    (IsBigO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ c') ↔ c' = 0 → c = 0
⊢ (IsBigO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ c') ↔ c' = 0 → c = 0

Tactic:
rcases eq_or_ne c' 0 with (rfl | hc')

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
c : E''
l : Filter α
inst_2 : l.NeBot
⊢ (IsBigO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ 0) ↔
    Eq.{u_10 + 1} (α := F'') 0 0 → c = 0

Tactic:
simp [EventuallyEq]

Premises used: Filter.EventuallyEq
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst_2 : l.NeBot
hc' : c' ≠ 0
⊢ (IsBigO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ c') ↔ c' = 0 → c = 0

Tactic:
simp [hc', isBigO_const_const _ hc']

Premises used: Asymptotics.isBigO_const_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
x : α
⊢ f'' =O[pure x] g'' ↔ g'' x = 0 → f'' x = 0

Tactic:
calc
    f'' =O[pure x] g'' ↔ (fun _y : α => f'' x) =O[pure x] fun _ => g'' x := isBigO_congr rfl rfl
    _ ↔ g'' x = 0 → f'' x = 0 := isBigO_const_const_iff _

Premises used: Asymptotics.isBigO_const_const_iff, Trans.trans, Asymptotics.isBigO_congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : R
f : α → R
l : Filter α
⊢ IsBigOWith (E := R) ‖c‖ l (fun (x : α) ↦ c * f x) f

Tactic:
isBigOWith_of_le' _ fun _x => norm_mul_le _ _

Premises used: Asymptotics.isBigOWith_of_le', norm_mul_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : R
f : α → R
l : Filter α
⊢ IsBigO (E := R) l (fun (x : α) ↦ c * f x) f

Tactic:
(isBigOWith_const_mul_self c f l).isBigO

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

Tactic:
(isBigOWith_const_mul_self c' f l).trans h (norm_nonneg c')

Premises used: Asymptotics.IsBigOWith.trans, Asymptotics.isBigOWith_const_mul_self, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
R : Type u_13
inst : Norm F
inst_1 : SeminormedRing R
g : α → F
l : Filter α
f : α → R
h : f =O[l] g
c' : R
⊢ IsBigO.{u_1, u_13, u_4} (E := R) l (fun (x : α) ↦ c' * f x) g

Tactic:
let ⟨_c, hc⟩ := h.isBigOWith
  (hc.const_mul_left c').isBigO

Premises used: HMul.hMul, Asymptotics.IsBigO, _private.0.Asymptotics.IsBigO.const_mul_left.match_1, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith, Asymptotics.IsBigOWith.const_mul_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
u : Rˣ
f : α → R
l : Filter α
⊢ IsBigOWith (F := R) ‖(↑u⁻¹ : R)‖ l f fun (x : α) ↦ (↑u : R) * f x

Tactic:
(isBigOWith_const_mul_self ↑u⁻¹ (fun x ↦ ↑u * f x) l).congr_left
    fun x ↦ u.inv_mul_cancel_left (f x)

Premises used: HMul.hMul, Asymptotics.IsBigOWith.congr_left, Asymptotics.isBigOWith_const_mul_self
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
S : Type u_17
inst : NormedRing S
inst_1 : NormMulClass S
c : S
hc : c ≠ 0
f : α → S
l : Filter α
⊢ IsBigOWith (F := S) ‖c‖⁻¹ l f fun (x : α) ↦ c * f x

Tactic:
simp [IsBigOWith, inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr hc)]

Premises used: Iff.mpr, Asymptotics.IsBigOWith, inv_mul_cancel_left₀, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : R
hc : IsUnit c
f : α → R
l : Filter α
⊢ IsBigO (F := R) l f fun (x : α) ↦ c * f x

Tactic:
let ⟨u, hu⟩ := hc
  hu ▸ (isBigOWith_self_const_mul' u f l).isBigO

Premises used: HMul.hMul, Asymptotics.isBigOWith_self_const_mul', Asymptotics.IsBigO, Eq.rec, _private.0.Asymptotics.isBigO_self_const_mul'.match_1, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
S : Type u_17
inst : NormedRing S
inst_1 : NormMulClass S
c : S
hc : c ≠ 0
f : α → S
l : Filter α
⊢ IsBigO (F := S) l f fun (x : α) ↦ c * f x

Tactic:
(isBigOWith_self_const_mul hc f l).isBigO

Premises used: Asymptotics.isBigOWith_self_const_mul, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
R : Type u_13
inst : Norm F
inst_1 : SeminormedRing R
g : α → F
l : Filter α
f : α → R
c : R
hc : IsUnit c
⊢ IsBigO.{u_1, u_13, u_4} (E := R) l (fun (x : α) ↦ c * f x) g ↔ f =O[l] g

Tactic:
⟨(isBigO_self_const_mul' hc f l).trans, fun h => h.const_mul_left c⟩

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.trans, Asymptotics.isBigO_self_const_mul', Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
inst : Norm F
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
g : α → F
l : Filter α
f : α → S
c : S
hc : c ≠ 0
⊢ IsBigO.{u_1, u_17, u_4} (E := S) l (fun (x : α) ↦ c * f x) g ↔ f =O[l] g

Tactic:
⟨(isBigO_self_const_mul hc f l).trans, (isBigO_const_mul_self c f l).trans⟩

Premises used: Asymptotics.IsBigO.trans, Iff.intro, Asymptotics.isBigO_const_mul_self, Asymptotics.isBigO_self_const_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
R : Type u_13
inst : Norm F
inst_1 : SeminormedRing R
g : α → F
l : Filter α
f : α → R
h : f =o[l] g
c : R
⊢ IsLittleO.{u_1, u_13, u_4} (E := R) l (fun (x : α) ↦ c * f x) g

Tactic:
(isBigO_const_mul_self c f l).trans_isLittleO h

Premises used: Asymptotics.isBigO_const_mul_self, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
R : Type u_13
inst : Norm F
inst_1 : SeminormedRing R
g : α → F
l : Filter α
f : α → R
c : R
hc : IsUnit c
⊢ IsLittleO.{u_1, u_13, u_4} (E := R) l (fun (x : α) ↦ c * f x) g ↔ f =o[l] g

Tactic:
⟨(isBigO_self_const_mul' hc f l).trans_isLittleO, fun h => h.const_mul_left c⟩

Premises used: Asymptotics.IsLittleO.const_mul_left, Asymptotics.isBigO_self_const_mul', Iff.intro, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
inst : Norm F
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
g : α → F
l : Filter α
f : α → S
c : S
hc : c ≠ 0
⊢ IsLittleO.{u_1, u_17, u_4} (E := S) l (fun (x : α) ↦ c * f x) g ↔ f =o[l] g

Tactic:
⟨(isBigO_self_const_mul hc f l).trans_isLittleO, (isBigO_const_mul_self c f l).trans_isLittleO⟩

Premises used: Iff.intro, Asymptotics.isBigO_const_mul_self, Asymptotics.isBigO_self_const_mul, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
c' : ℝ
f : α → E
l : Filter α
g : α → R
c : R
hc' : 0 ≤ c'
h : IsBigOWith.{u_1, u_3, u_13} (F := R) c' l f fun (x : α) ↦ c * g x
⊢ IsBigOWith (c' * ‖c‖) l f g

Tactic:
h.trans (isBigOWith_const_mul_self c g l) hc'

Premises used: Asymptotics.IsBigOWith.trans, Asymptotics.isBigOWith_const_mul_self
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
f : α → E
l : Filter α
g : α → R
c : R
h : IsBigO.{u_1, u_3, u_13} (F := R) l f fun (x : α) ↦ c * g x
⊢ f =O[l] g

Tactic:
let ⟨_c, cnonneg, hc⟩ := h.exists_nonneg
  (hc.of_const_mul_right cnonneg).isBigO

Premises used: Asymptotics.IsBigO, Asymptotics.IsBigO.exists_nonneg, Asymptotics.IsBigOWith.of_const_mul_right, Asymptotics.IsBigOWith.isBigO, _private.0.Asymptotics.IsBigO.of_const_mul_right.match_1
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
f : α → E
l : Filter α
g : α → R
u : Rˣ
c' : ℝ
hc' : 0 ≤ c'
h : IsBigOWith c' l f g
⊢ IsBigOWith.{u_1, u_3, u_13} (F := R) (c' * ‖(↑u⁻¹ : R)‖) l f fun (x : α) ↦ (↑u : R) * g x

Tactic:
h.trans (isBigOWith_self_const_mul' _ _ _) hc'

Premises used: Asymptotics.isBigOWith_self_const_mul', Asymptotics.IsBigOWith.trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
f : α → E
l : Filter α
g : α → S
c : S
hc : c ≠ 0
c' : ℝ
hc' : 0 ≤ c'
h : IsBigOWith c' l f g
⊢ IsBigOWith.{u_1, u_3, u_17} (F := S) (c' * ‖c‖⁻¹) l f fun (x : α) ↦ c * g x

Tactic:
h.trans (isBigOWith_self_const_mul hc g l) hc'

Premises used: Asymptotics.IsBigOWith.trans, Asymptotics.isBigOWith_self_const_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
f : α → E
l : Filter α
g : α → R
c : R
hc : IsUnit c
h : f =O[l] g
⊢ IsBigO.{u_1, u_3, u_13} (F := R) l f fun (x : α) ↦ c * g x

Tactic:
h.trans (isBigO_self_const_mul' hc g l)

Premises used: Asymptotics.IsBigO.trans, Asymptotics.isBigO_self_const_mul'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
f : α → E
l : Filter α
g : α → S
c : S
hc : c ≠ 0
h : f =O[l] g
⊢ IsBigO.{u_1, u_3, u_17} (F := S) l f fun (x : α) ↦ c * g x

Tactic:
match h.exists_nonneg with
  | ⟨_, hd, hd'⟩ => (hd'.const_mul_right hc hd).isBigO

Premises used: HMul.hMul, Asymptotics.IsBigO, Asymptotics.IsBigO.exists_nonneg, _private.0.Asymptotics.IsBigO.const_mul_right.match_1, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigOWith.const_mul_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
f : α → E
l : Filter α
g : α → R
c : R
hc : IsUnit c
⊢ (IsBigO.{u_1, u_3, u_13} (F := R) l f fun (x : α) ↦ c * g x) ↔ f =O[l] g

Tactic:
⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩

Premises used: Iff.intro, Asymptotics.IsBigO.const_mul_right', Asymptotics.IsBigO.of_const_mul_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
f : α → E
l : Filter α
g : α → S
c : S
hc : c ≠ 0
⊢ (IsBigO.{u_1, u_3, u_17} (F := S) l f fun (x : α) ↦ c * g x) ↔ f =O[l] g

Tactic:
⟨fun h ↦ h.of_const_mul_right, fun h ↦ h.const_mul_right hc⟩

Premises used: Asymptotics.IsBigO.const_mul_right, Iff.intro, Asymptotics.IsBigO.of_const_mul_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
f : α → E
l : Filter α
g : α → R
c : R
h : IsLittleO.{u_1, u_3, u_13} (F := R) l f fun (x : α) ↦ c * g x
⊢ f =o[l] g

Tactic:
h.trans_isBigO (isBigO_const_mul_self c g l)

Premises used: Asymptotics.isBigO_const_mul_self, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
f : α → E
l : Filter α
g : α → R
c : R
hc : IsUnit c
h : f =o[l] g
⊢ IsLittleO.{u_1, u_3, u_13} (F := R) l f fun (x : α) ↦ c * g x

Tactic:
h.trans_isBigO (isBigO_self_const_mul' hc g l)

Premises used: Asymptotics.isBigO_self_const_mul', Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
f : α → E
l : Filter α
g : α → S
c : S
hc : c ≠ 0
h : f =o[l] g
⊢ IsLittleO.{u_1, u_3, u_17} (F := S) l f fun (x : α) ↦ c * g x

Tactic:
h.trans_isBigO <| isBigO_self_const_mul hc g l

Premises used: Asymptotics.isBigO_self_const_mul, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
R : Type u_13
inst : Norm E
inst_1 : SeminormedRing R
f : α → E
l : Filter α
g : α → R
c : R
hc : IsUnit c
⊢ (IsLittleO.{u_1, u_3, u_13} (F := R) l f fun (x : α) ↦ c * g x) ↔ f =o[l] g

Tactic:
⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩

Premises used: Asymptotics.IsLittleO.of_const_mul_right, Asymptotics.IsLittleO.const_mul_right', Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
f : α → E
l : Filter α
g : α → S
c : S
hc : c ≠ 0
⊢ (IsLittleO.{u_1, u_3, u_17} (F := S) l f fun (x : α) ↦ c * g x) ↔ f =o[l] g

Tactic:
⟨fun h ↦ h.of_const_mul_right, fun h ↦ h.trans_isBigO (isBigO_self_const_mul hc g l)⟩

Premises used: Asymptotics.IsLittleO.of_const_mul_right, Iff.intro, Asymptotics.isBigO_self_const_mul, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : IsBigOWith c₁ l f₁ g₁
h₂ : IsBigOWith c₂ l f₂ g₂
simp :
  ∀ (h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) (h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖),
    ∀ᶠ (x : α) in l, ‖f₁ x * f₂ x‖ ≤ c₁ * c₂ * ‖g₁ x * g₂ x‖
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) (c₁ * c₂) l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
simp only [IsBigOWith_def] at *

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
h : ∀ (a : α) (hx₁ : ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖) (hx₂ : ‖f₂ a‖ ≤ c₂ * ‖g₂ a‖), ‖f₁ a * f₂ a‖ ≤ c₁ * c₂ * ‖g₁ a * g₂ a‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x * f₂ x‖ ≤ c₁ * c₂ * ‖g₁ x * g₂ x‖

Tactic:
filter_upwards [h₁, h₂] with _ hx₁ hx₂
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a : α
hx₁ : ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖
hx₂ : ‖f₂ a‖ ≤ c₂ * ‖g₂ a‖
h : ‖f₁ a‖ * ‖f₂ a‖ ≤ c₁ * c₂ * ‖g₁ a * g₂ a‖
⊢ ‖f₁ a * f₂ a‖ ≤ c₁ * c₂ * ‖g₁ a * g₂ a‖

Tactic:
apply le_trans (norm_mul_le _ _)

Premises used: norm_mul_le, le_trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a : α
hx₁ : ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖
hx₂ : ‖f₂ a‖ ≤ c₂ * ‖g₂ a‖
⊢ ‖f₁ a‖ * ‖f₂ a‖ ≤ c₁ * ‖g₁ 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.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a : α
hx₁ : ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖
hx₂ : ‖f₂ a‖ ≤ c₂ * ‖g₂ a‖
h : c₁ * c₂ * ‖g₁ a * g₂ a‖ = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
⊢ ‖f₁ a‖ * ‖f₂ a‖ ≤ c₁ * c₂ * ‖g₁ 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
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a : α
hx₁ : ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖
hx₂ : ‖f₂ a‖ ≤ c₂ * ‖g₂ a‖
h : c₁ * c₂ * (‖g₁ a‖ * ‖g₂ a‖) = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
h₃ h₄ : c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖) = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
⊢ c₁ * c₂ * ‖g₁ a * g₂ a‖ = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)

Tactic:
rw [norm_mul, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, norm_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
⊢ IsBigO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
let ⟨_c, hc⟩ := h₁.isBigOWith
  let ⟨_c', hc'⟩ := h₂.isBigOWith
  (hc.mul hc').isBigO

Premises used: HMul.hMul, _private.0.Asymptotics.IsBigO.mul.match_1, Asymptotics.IsBigO, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith, Asymptotics.IsBigOWith.mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : f₂ =o[l] g₂
simp :
  ∀ (h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂) ⦃c : ℝ⦄,
    0 < c → IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
simp only [IsLittleO_def] at *

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
rcases :
  ∀ (c' : ℝ) (c'pos : c' > 0) (hc' : IsBigOWith c' l f₁ g₁),
    IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₁ g₁
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
(hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

Premises used: ne_of_gt, mul_div_cancel₀, div_pos, Asymptotics.IsBigOWith.mul, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₁ g₁
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
exact (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

Premises used: ne_of_gt, mul_div_cancel₀, div_pos, Asymptotics.IsBigOWith.mul, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =o[l] g₁
h₂ : f₂ =O[l] g₂
simp :
  ∀ (h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ⦃c : ℝ⦄,
    0 < c → IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
simp only [IsLittleO_def] at *

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
rcases :
  ∀ (c' : ℝ) (c'pos : c' > 0) (hc' : IsBigOWith c' l f₂ g₂),
    IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₂ g₂
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

Premises used: div_mul_cancel₀, ne_of_gt, div_pos, Asymptotics.IsBigOWith.mul, Asymptotics.IsBigOWith.congr_const