awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
simp : (∀ᶠ (x : α) in map k l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : β) in l, ‖(f ∘ k) x‖ ≤ c * ‖(g ∘ k) x‖
⊢ IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)

Tactic:
simp only [IsBigOWith_def]

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ (∀ᶠ (x : α) in map k l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : β) in l, ‖(f ∘ k) x‖ ≤ c * ‖(g ∘ k) x‖

Tactic:
eventually_map

Premises used: Filter.eventually_map
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ (∀ᶠ (x : α) in map k l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : β) in l, ‖(f ∘ k) x‖ ≤ c * ‖(g ∘ k) x‖

Tactic:
exact eventually_map

Premises used: Filter.eventually_map
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)

Tactic:
simp only [IsBigO_def, isBigOWith_map]

Premises used: Asymptotics.isBigOWith_map, Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)

Tactic:
simp only [IsLittleO_def, isBigOWith_map]

Premises used: Asymptotics.isBigOWith_map, Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l l' : Filter α
h : IsBigOWith c l' f g
hl : l ≤ l'
⊢ IsBigOWith c l f g

Tactic:
IsBigOWith.of_bound <| hl h.bound

Premises used: Asymptotics.IsBigOWith.bound, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l l' : Filter α
h : f =O[l'] g
hl : l ≤ l'
⊢ f =O[l] g

Tactic:
isBigO_iff_isBigOWith.2 <| h.isBigOWith.imp fun _c h => h.mono hl

Premises used: Iff.mpr, Exists.imp, Asymptotics.IsBigO.isBigOWith, Asymptotics.isBigO_iff_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l l' : Filter α
h : f =o[l'] g
hl : l ≤ l'
⊢ f =o[l] g

Tactic:
IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).mono hl

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsBigOWith.mono
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : IsBigOWith c' l g k
hc : 0 ≤ c
simp :
  ∀ (hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) (hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖),
    ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖
⊢ IsBigOWith (c * c') l f k

Tactic:
simp only [IsBigOWith_def] at *

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
h : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖) (hx' : ‖g x‖ ≤ c' * ‖k x‖), ‖f x‖ ≤ c * c' * ‖k x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖

Tactic:
filter_upwards [hfg, hgk] with x hx hx'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
hx
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
ha : 0 ≤ c
⊢ c * ‖g x‖ ≤ c * (c' * ‖k x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ c * (c' * ‖k x‖) = c * c' * ‖k x‖

Tactic:
(mul_assoc _ _ _).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
c₁ : c * ‖g x‖ ≤ c * (c' * ‖k x‖)
⊢ ‖f x‖ ≤ c * c' * ‖k x‖

Tactic:
calc
    ‖f x‖ ≤ c * ‖g x‖ := hx
    _ ≤ c * (c' * ‖k x‖) := by gcongr
    _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm

Premises used: Norm.norm, HMul.hMul, mul_assoc, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
l : Filter α
f : α → E
g : α → F'
k : α → G
hfg : f =O[l] g
hgk : g =O[l] k
⊢ f =O[l] k

Tactic:
let ⟨_c, cnonneg, hc⟩ := hfg.exists_nonneg
  let ⟨_c', hc'⟩ := hgk.isBigOWith
  (hc.trans hc' cnonneg).isBigO

Premises used: Asymptotics.IsBigO, Asymptotics.IsBigOWith.trans, _private.0.Asymptotics.IsBigO.trans.match_2, _private.0.Asymptotics.IsBigO.trans.match_1, Asymptotics.IsBigO.exists_nonneg, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : f =o[l] g
hgk : IsBigOWith c l g k
hc : 0 < c
simp : ∀ (hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
⊢ f =o[l] k

Tactic:
simp only [IsLittleO_def] at *

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
⊢ 0 < c' / c

Tactic:
have : 0 < c' / c := div_pos c'pos hc
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Tactic:
((hfg this).trans hgk this.le).congr_const (div_mul_cancel₀ _ hc.ne')

Premises used: div_mul_cancel₀, Asymptotics.IsBigOWith.trans, LT.lt.le, LT.lt.ne', Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Tactic:
exact ((hfg this).trans hgk this.le).congr_const (div_mul_cancel₀ _ hc.ne')

Premises used: div_mul_cancel₀, Asymptotics.IsBigOWith.trans, LT.lt.le, LT.lt.ne', Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G' : Type u_8
inst : Norm E
inst_1 : Norm F
inst_2 : SeminormedAddCommGroup G'
l : Filter α
f : α → E
g : α → F
k : α → G'
hfg : f =o[l] g
hgk : g =O[l] k
⊢ f =o[l] k

Tactic:
let ⟨_c, cpos, hc⟩ := hgk.exists_pos
  hfg.trans_isBigOWith hc cpos

Premises used: Asymptotics.IsLittleO.trans_isBigOWith, Asymptotics.IsLittleO, _private.0.Asymptotics.IsLittleO.trans_isBigO.match_1, Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : g =o[l] k
hc : 0 < c
simp : ∀ (hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
⊢ f =o[l] k

Tactic:
simp only [IsLittleO_def] at *

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
⊢ 0 < c' / c

Tactic:
have : 0 < c' / c := div_pos c'pos hc
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Tactic:
(hfg.trans (hgk this) hc.le).congr_const (mul_div_cancel₀ _ hc.ne')

Premises used: Asymptotics.IsBigOWith.trans, LT.lt.le, mul_div_cancel₀, LT.lt.ne', Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Tactic:
exact (hfg.trans (hgk this) hc.le).congr_const (mul_div_cancel₀ _ hc.ne')

Premises used: Asymptotics.IsBigOWith.trans, LT.lt.le, mul_div_cancel₀, LT.lt.ne', Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
l : Filter α
f : α → E
g : α → F'
k : α → G
hfg : f =O[l] g
hgk : g =o[l] k
⊢ f =o[l] k

Tactic:
let ⟨_c, cpos, hc⟩ := hfg.exists_pos
  hc.trans_isLittleO hgk cpos

Premises used: Asymptotics.IsBigOWith.trans_isLittleO, Asymptotics.IsLittleO, _private.0.Asymptotics.IsLittleO.trans_isBigO.match_1, Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[l] g
hgk : g =o[l] k
⊢ f =o[l] k

Tactic:
hfg.trans_isBigOWith hgk.isBigOWith one_pos

Premises used: Asymptotics.IsLittleO.trans_isBigOWith, Asymptotics.IsLittleO.isBigOWith, one_pos
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
l : Filter α
f : α → E
g : α → F'
k : α → G
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖
hgk : g =O[l] k
⊢ f =O[l] k

Tactic:
(IsBigO.of_bound' hfg).trans hgk

Premises used: Asymptotics.IsBigO.trans, Asymptotics.IsBigO.of_bound'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
g : α → ℝ
l : Filter α
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ g x
⊢ f =O[l] g

Tactic:
.of_norm_eventuallyLE hfg

Premises used: Asymptotics.IsBigO.of_norm_eventuallyLE
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
⊢ IsBigOWith c l f g

Tactic:
IsBigOWith.of_bound <| univ_mem' hfg

Premises used: Asymptotics.IsBigOWith.of_bound, Filter.univ_mem'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
rw : ‖f x‖ ≤ ‖g x‖
⊢ ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ ‖g x‖

Tactic:
hfg x
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ ‖g x‖

Tactic:
exact hfg x
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
(isBigOWith_of_le' l hfg).isBigO

Premises used: Asymptotics.isBigOWith_of_le', Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
⊢ f =O[l] g

Tactic:
(isBigOWith_of_le l hfg).isBigO

Premises used: Asymptotics.isBigOWith_of_le, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
⊢ IsBigOWith 1 l f f

Tactic:
isBigOWith_of_le l fun _ => le_rfl

Premises used: le_rfl, Asymptotics.isBigOWith_of_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
⊢ f =O[l] f

Tactic:
(isBigOWith_refl f l).isBigO

Premises used: Asymptotics.isBigOWith_refl, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
l : Filter α
f₁ f₂ : α → E
hf : f₁ =ᶠ[l] f₂
⊢ f₁ =O[l] f₂

Tactic:
hf.trans_isBigO (isBigO_refl _ _)

Premises used: Filter.EventuallyEq.trans_isBigO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖
hc : 0 ≤ c
⊢ IsBigOWith c l f k

Tactic:
(hfg.trans (isBigOWith_of_le l hgk) hc).congr_const <| mul_one c

Premises used: Asymptotics.IsBigOWith.trans, Asymptotics.isBigOWith_of_le, mul_one, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
f : α → E
k : α → G
g' : α → F'
l : Filter α
hfg : f =O[l] g'
hgk : ∀ (x : α), ‖g' x‖ ≤ ‖k x‖
⊢ f =O[l] k

Tactic:
hfg.trans (isBigO_of_le l hgk)

Premises used: Asymptotics.IsBigO.trans, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : f =o[l] g
hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖
⊢ f =o[l] k

Tactic:
hfg.trans_isBigOWith (isBigOWith_of_le _ hgk) zero_lt_one

Premises used: Asymptotics.IsLittleO.trans_isBigOWith, Asymptotics.isBigOWith_of_le, zero_lt_one
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
rcases : ∀ (x : α) (hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖) (hne : ‖f' x‖ ≠ 0), False
⊢ False

Tactic:
rcases ((ho.bound one_half_pos).and_frequently h).exists with ⟨x, hle, hne⟩

Premises used: Asymptotics.IsLittleO.bound, Filter.Frequently.exists, one_half_pos, Filter.Eventually.and_frequently
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖
hne : ‖f' x‖ ≠ 0
⊢ ‖f' x‖ ≤ ‖f' x‖ / 2

Tactic:
rw [one_div, ← div_eq_inv_mul] at hle

Premises used: one_div, div_eq_inv_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖
hne : ‖f' x‖ ≠ 0
hle₁ : ‖f' x‖ ≤ ‖f' x‖ / 2
⊢ ‖f' x‖ ≠ 0

Tactic:
rw [one_div, ← div_eq_inv_mul] at hle

Premises used: one_div, div_eq_inv_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ ‖f' x‖ / 2
hne : ‖f' x‖ ≠ 0
⊢ False

Tactic:
(half_lt_self (lt_of_le_of_ne (norm_nonneg _) hne.symm)).not_ge hle

Premises used: half_lt_self, Ne.symm, LT.lt.not_ge, norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ ‖f' x‖ / 2
hne : ‖f' x‖ ≠ 0
⊢ False

Tactic:
exact (half_lt_self (lt_of_le_of_ne (norm_nonneg _) hne.symm)).not_ge hle

Premises used: half_lt_self, Ne.symm, LT.lt.not_ge, norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E'' : Type u_9
inst : NormedAddCommGroup E''
f'' : α → E''
l : Filter α
h : ∃ᶠ (x : α) in l, f'' x ≠ 0
⊢ ¬f'' =o[l] f''

Tactic:
isLittleO_irrefl' <| h.mono fun _x => norm_ne_zero_iff.mpr

Premises used: Iff.mpr, Asymptotics.isLittleO_irrefl', Filter.Frequently.mono, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
l : Filter α
h : f'' =O[l] g'
hf : ∃ᶠ (x : α) in l, f'' x ≠ 0
⊢ ¬g' =o[l] f''

Tactic:
fun h' =>
  isLittleO_irrefl hf (h.trans_isLittleO h')

Premises used: Asymptotics.isLittleO_irrefl, Asymptotics.IsBigO.trans_isLittleO, Not
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
l : Filter α
h : f'' =o[l] g'
hf : ∃ᶠ (x : α) in l, f'' x ≠ 0
⊢ ¬g' =O[l] f''

Tactic:
fun h' =>
  isLittleO_irrefl hf (h.trans_isBigO h')

Premises used: Asymptotics.isLittleO_irrefl, Not, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
⊢ IsBigOWith c ⊥ f g

Tactic:
IsBigOWith.of_bound <| trivial

Premises used: trivial, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
⊢ f =O[⊥] g

Tactic:
(isBigOWith_bot 1 f g).isBigO

Premises used: Asymptotics.isBigOWith_bot, Asymptotics.IsBigOWith.isBigO, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
⊢ f =o[⊥] g

Tactic:
IsLittleO.of_isBigOWith fun c _ => isBigOWith_bot c f g

Premises used: Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.isBigOWith_bot
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
x : α
⊢ IsBigOWith c (pure x) f g ↔ ‖f x‖ ≤ c * ‖g x‖

Tactic:
isBigOWith_iff

Premises used: Set.Mem, Filter.Eventually, setOf, Asymptotics.isBigOWith_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l l' : Filter α
h : IsBigOWith c l f g
h' : IsBigOWith c l' f g
⊢ IsBigOWith c (l ⊔ l') f g

Tactic:
IsBigOWith.of_bound <| mem_sup.2 ⟨h.bound, h'.bound⟩

Premises used: Iff.mpr, Filter.mem_sup, And.intro, Asymptotics.IsBigOWith.bound, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
c c' : ℝ
f : α → E
g' : α → F'
l l' : Filter α
h : IsBigOWith c l f g'
h' : IsBigOWith c' l' f g'
⊢ IsBigOWith (max c c') (l ⊔ l') f g'

Tactic:
IsBigOWith.of_bound <|
    mem_sup.2 ⟨(h.weaken <| le_max_left c c').bound, (h'.weaken <| le_max_right c c').bound⟩

Premises used: le_max_right, Iff.mpr, Filter.mem_sup, And.intro, Asymptotics.IsBigOWith.bound, Asymptotics.IsBigOWith.weaken, le_max_left, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l l' : Filter α
h : f =O[l] g'
h' : f =O[l'] g'
⊢ f =O[l ⊔ l'] g'

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

Premises used: _private.0.Asymptotics.IsBigO.exists_pos.match_1, Asymptotics.IsBigO, Max.max, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith, Asymptotics.IsBigOWith.sup'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l l' : Filter α
h : f =o[l] g
h' : f =o[l'] g
⊢ f =o[l ⊔ l'] g

Tactic:
IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).sup (h'.forall_isBigOWith cpos)

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsBigOWith.sup
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l l' : Filter α
⊢ f =O[l ⊔ l'] g' ↔ f =O[l] g' ∧ f =O[l'] g'

Tactic:
⟨fun h => ⟨h.mono le_sup_left, h.mono le_sup_right⟩, fun h => h.1.sup h.2⟩

Premises used: le_sup_left, le_sup_right, And.right, And.left, Asymptotics.IsBigO.mono, And.intro, Iff.intro, Asymptotics.IsBigO.sup
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l l' : Filter α
⊢ f =o[l ⊔ l'] g ↔ f =o[l] g ∧ f =o[l'] g

Tactic:
⟨fun h => ⟨h.mono le_sup_left, h.mono le_sup_right⟩, fun h => h.1.sup h.2⟩

Premises used: le_sup_left, le_sup_right, And.right, And.left, And.intro, Iff.intro, Asymptotics.IsLittleO.sup, Asymptotics.IsLittleO.mono
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
simp_rw : (∀ᶠ (x : α) in 𝓝[insert x s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₁ : (∀ᶠ (x : α) in pure x ⊔ 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₂ :
  ((∀ᶠ (x : α) in pure x, ‖g x‖ ≤ C * ‖g' x‖) ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔
    ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₃ : (‖g x‖ ≤ C * ‖g' x‖ ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₄ : (True ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'

Tactic:
simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]

Premises used: nhdsWithin_insert, Asymptotics.IsBigOWith_def, Filter.eventually_pure, Filter.eventually_sup, true_and
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h1 : IsBigOWith C (𝓝[s] x) g g'
h2 : ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g'

Tactic:
(isBigOWith_insert h2).mpr h1

Premises used: Iff.mpr, Asymptotics.isBigOWith_insert