awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
h : ∀ (x : α) (hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) (hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖), ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
filter_upwards [h₁, h₂] with x hx₁ hx₂
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖

Tactic:
norm_add_le_of_le hx₁ hx₂

Premises used: norm_add_le_of_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
h₃ : c₁ ≤ max c₁ c₂
h₄ : c₂ ≤ max c₁ c₂
⊢ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₁ ≤ max c₁ c₂

Tactic:
simp [le_max_left _ _, le_max_right _ _]

Premises used: le_max_right, le_max_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₂ ≤ max c₁ c₂

Tactic:
simp [le_max_left _ _, le_max_right _ _]

Premises used: le_max_right, le_max_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
rw : max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * (‖g₁ x‖ + ‖g₂ x‖)
rw₁ rw₂ : max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖
⊢ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
rw [Real.norm_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)), mul_add]

Premises used: add_nonneg, mul_add, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x₁ : c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖
x₂ : max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
calc
    ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ := norm_add_le_of_le hx₁ hx₂
    _ ≤ (max c₁ c₂) * ‖g₁ x‖ + (max c₁ c₂) * ‖g₂ x‖ := by
        gcongr <;> simp [le_max_left _ _, le_max_right _ _]
    _ = (max c₁ c₂) * ‖‖g₁ x‖ + ‖g₂ x‖‖ := by
        rw [Real.norm_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)), mul_add]

Premises used: Max.max, norm_add_le_of_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
obtain :
  ∀ (c₁ : ℝ) (hc₁ : IsBigOWith c₁ l f₁ g₁),
    IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
obtain ⟨c₁, hc₁⟩ := h₁.isBigOWith

Premises used: Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
c₁ : ℝ
hc₁ : IsBigOWith c₁ l f₁ g₁
obtain :
  ∀ (c₂ : ℝ) (hc₂ : IsBigOWith c₂ l f₂ g₂),
    IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
obtain ⟨c₂, hc₂⟩ := h₂.isBigOWith

Premises used: Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
c₁ : ℝ
hc₁ : IsBigOWith c₁ l f₁ g₁
c₂ : ℝ
hc₂ : IsBigOWith c₂ l f₂ g₂
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
(hc₁.add_add hc₂).isBigO

Premises used: Asymptotics.IsBigOWith.add_add, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
c₁ : ℝ
hc₁ : IsBigOWith c₁ l f₁ g₁
c₂ : ℝ
hc₂ : IsBigOWith c₂ l f₂ g₂
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
exact (hc₁.add_add hc₂).isBigO

Premises used: Asymptotics.IsBigOWith.add_add, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
(h₁.trans_le fun x => ?_).add (h₂.trans_le ?_)

Premises used: Asymptotics.IsLittleO.add, Asymptotics.IsLittleO.trans_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
refine_1 : ∀ (x : α), ‖g₁ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
refine_2 : ∀ (x : α), ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
refine (h₁.trans_le fun x => ?_).add (h₂.trans_le ?_)

Premises used: Asymptotics.IsLittleO.add, Asymptotics.IsLittleO.trans_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
x : α
⊢ ‖g₁ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
simp [abs_of_nonneg, add_nonneg]

Premises used: add_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ ∀ (x : α), ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
simp [abs_of_nonneg, add_nonneg]

Premises used: add_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =O[l] g
h₂ : f₂ =o[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x + f₂ x) g

Tactic:
h₁.add h₂.isBigO

Premises used: Asymptotics.IsBigO.add, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
h₂ : f₂ =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x + f₂ x) g

Tactic:
h₁.isBigO.add h₂

Premises used: Asymptotics.IsBigO.add, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : f₂ =o[l] g
hc : c₁ < c₂
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') c₂ l (fun (x : α) ↦ f₁ x + f₂ x) g

Tactic:
(h₁.add (h₂.forall_isBigOWith (sub_pos.2 hc))).congr_const (add_sub_cancel _ _)

Premises used: Iff.mpr, sub_pos, Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsBigOWith.add, add_sub_cancel, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
h₂ : IsBigOWith c₁ l f₂ g
hc : c₁ < c₂
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') c₂ l (fun (x : α) ↦ f₁ x + f₂ x) g

Tactic:
(h₂.add_isLittleO h₁ hc).congr_left fun _ => add_comm _ _

Premises used: Asymptotics.IsBigOWith.add_isLittleO, Asymptotics.IsBigOWith.congr_left, add_comm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (c₁ + c₂) l (fun (x : α) ↦ f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Premises used: sub_eq_add_neg, Asymptotics.IsBigOWith.add, Asymptotics.IsBigOWith.neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : f₂ =o[l] g
hc : c₁ < c₂
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') c₂ l (fun (x : α) ↦ f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add_isLittleO h₂.neg_left hc

Premises used: sub_eq_add_neg, Asymptotics.IsBigOWith.add_isLittleO, Asymptotics.IsLittleO.neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =O[l] g
h₂ : f₂ =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Premises used: sub_eq_add_neg, Asymptotics.IsBigO.neg_left, Asymptotics.IsBigO.add
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
h₂ : f₂ =o[l] g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Premises used: sub_eq_add_neg, Asymptotics.IsLittleO.neg_left, Asymptotics.IsLittleO.add
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₂ : f₂ =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x + f₂ x) g ↔ f₁ =O[l] g

Tactic:
⟨fun h ↦ h.sub h₂ |>.congr (fun _ ↦ add_sub_cancel_right _ _) (fun _ ↦ rfl), fun h ↦ h.add h₂⟩

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.add, Iff.intro, add_sub_cancel_right, Asymptotics.IsBigO.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x + f₂ x) g ↔ f₂ =O[l] g

Tactic:
⟨fun h ↦ h.sub h₁ |>.congr (fun _ ↦ (eq_sub_of_add_eq' rfl).symm) (fun _ ↦ rfl), fun h ↦ h₁.add h⟩

Premises used: Asymptotics.IsBigO.sub, eq_sub_of_add_eq', Asymptotics.IsBigO.add, Iff.intro, Eq.symm, Asymptotics.IsBigO.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₂ : f₂ =o[l] g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x + f₂ x) g ↔ f₁ =o[l] g

Tactic:
⟨fun h ↦ h.sub h₂ |>.congr (fun _ ↦ add_sub_cancel_right _ _) (fun _ ↦ rfl), fun h ↦ h.add h₂⟩

Premises used: Asymptotics.IsLittleO.add, Iff.intro, Asymptotics.IsLittleO.congr, add_sub_cancel_right, Asymptotics.IsLittleO.sub, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x + f₂ x) g ↔ f₂ =o[l] g

Tactic:
⟨fun h ↦ h.sub h₁ |>.congr (fun _ ↦ (eq_sub_of_add_eq' rfl).symm) (fun _ ↦ rfl), fun h ↦ h₁.add h⟩

Premises used: eq_sub_of_add_eq', Asymptotics.IsLittleO.add, Iff.intro, Asymptotics.IsLittleO.congr, Eq.symm, Asymptotics.IsLittleO.sub, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₂ : f₂ =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g ↔ f₁ =O[l] g

Tactic:
⟨fun h ↦ h.add h₂ |>.congr (fun _ ↦ sub_add_cancel ..) (fun _ ↦ rfl), fun h ↦ h.sub h₂⟩

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.add, Iff.intro, sub_add_cancel, Asymptotics.IsBigO.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =O[l] g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g ↔ f₂ =O[l] g

Tactic:
⟨fun h ↦ h₁.sub h |>.congr (fun _ ↦ sub_sub_self ..) (fun _ ↦ rfl), fun h ↦ h₁.sub h⟩

Premises used: Asymptotics.IsBigO.sub, Iff.intro, sub_sub_self, Asymptotics.IsBigO.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₂ : f₂ =o[l] g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g ↔ f₁ =o[l] g

Tactic:
⟨fun h ↦ h.add h₂ |>.congr (fun _ ↦ sub_add_cancel ..) (fun _ ↦ rfl), fun h ↦ h.sub h₂⟩

Premises used: Asymptotics.IsLittleO.add, Iff.intro, Asymptotics.IsLittleO.congr, sub_add_cancel, Asymptotics.IsLittleO.sub, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g ↔ f₂ =o[l] g

Tactic:
⟨fun h ↦ h₁.sub h |>.congr (fun _ ↦ sub_sub_self ..) (fun _ ↦ rfl), fun h ↦ h₁.sub h⟩

Premises used: Iff.intro, Asymptotics.IsLittleO.congr, sub_sub_self, Asymptotics.IsLittleO.sub, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ f₁ x - f₂ x) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ f₂ x - f₁ x) g

Tactic:
h.neg_left.congr_left fun _x => neg_sub _ _

Premises used: neg_sub, Asymptotics.IsBigOWith.congr_left, Asymptotics.IsBigOWith.neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ f₁ x - f₂ x) g ↔
    IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ f₂ x - f₁ x) g

Tactic:
⟨IsBigOWith.symm, IsBigOWith.symm⟩

Premises used: Asymptotics.IsBigOWith.symm, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h : IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₂ x - f₁ x) g

Tactic:
h.neg_left.congr_left fun _x => neg_sub _ _

Premises used: neg_sub, Asymptotics.IsBigO.neg_left, Asymptotics.IsBigO.congr_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g ↔
    IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₂ x - f₁ x) g

Tactic:
⟨IsBigO.symm, IsBigO.symm⟩

Premises used: Iff.intro, Asymptotics.IsBigO.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h : IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₂ x - f₁ x) g

Tactic:
simpa only [neg_sub] using h.neg_left

Premises used: neg_sub, Asymptotics.IsLittleO.neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g ↔
    IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₂ x - f₁ x) g

Tactic:
⟨IsLittleO.symm, IsLittleO.symm⟩

Premises used: Asymptotics.IsLittleO.symm, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c c' : ℝ
g : α → F
l : Filter α
f₁ f₂ f₃ : α → E'
h₁ : IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ f₁ x - f₂ x) g
h₂ : IsBigOWith.{u_1, u_6, u_4} (E := E') c' l (fun (x : α) ↦ f₂ x - f₃ x) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (c + c') l (fun (x : α) ↦ f₁ x - f₃ x) g

Tactic:
(h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

Premises used: sub_add_sub_cancel, Asymptotics.IsBigOWith.congr_left, Asymptotics.IsBigOWith.add
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ f₃ : α → E'
h₁ : IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g
h₂ : IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₂ x - f₃ x) g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₃ x) g

Tactic:
(h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

Premises used: sub_add_sub_cancel, Asymptotics.IsBigO.congr_left, Asymptotics.IsBigO.add
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ f₃ : α → E'
h₁ : IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g
h₂ : IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₂ x - f₃ x) g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₃ x) g

Tactic:
(h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

Premises used: sub_add_sub_cancel, Asymptotics.IsLittleO.congr_left, Asymptotics.IsLittleO.add
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h : IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g
⊢ f₁ =O[l] g ↔ f₂ =O[l] g

Tactic:
⟨fun h' => (h'.sub h).congr_left fun _x => sub_sub_cancel _ _, fun h' =>
    (h.add h').congr_left fun _x => sub_add_cancel _ _⟩

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.congr_left, Asymptotics.IsBigO.add, sub_sub_cancel, Iff.intro, sub_add_cancel
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h : IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ f₁ x - f₂ x) g
⊢ f₁ =o[l] g ↔ f₂ =o[l] g

Tactic:
⟨fun h' => (h'.sub h).congr_left fun _x => sub_sub_cancel _ _, fun h' =>
    (h.add h').congr_left fun _x => sub_add_cancel _ _⟩

Premises used: Asymptotics.IsLittleO.congr_left, sub_sub_cancel, Asymptotics.IsLittleO.add, Iff.intro, sub_add_cancel, Asymptotics.IsLittleO.sub
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
c : ℝ
hc : 0 < c
x : α
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ norm.{u_6} (E := E') 0 ≤ c * ‖g' x‖) x} x

Tactic:
simpa using mul_nonneg hc.le (norm_nonneg <| g' x)

Premises used: mul_nonneg, LT.lt.le, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
c : ℝ
g' : α → F'
l : Filter α
hc : 0 ≤ c
x : α
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ norm.{u_6} (E := E') 0 ≤ c * ‖g' x‖) x} x

Tactic:
simpa using mul_nonneg hc (norm_nonneg <| g' x)

Premises used: mul_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
x : α
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ norm.{u_6} (E := E') 0 ≤ 0 * ‖g x‖) x} x

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (_x : α) ↦ 0) g

Tactic:
isBigO_iff_isBigOWith.2 ⟨0, isBigOWith_zero' _ _⟩

Premises used: Iff.mpr, Asymptotics.isBigOWith_zero', Exists.intro, Asymptotics.isBigO_iff_isBigOWith, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ IsBigO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ f' x - f' x) g'

Tactic:
(isBigO_zero g' l).congr_left fun _x => (sub_self _).symm

Premises used: Asymptotics.isBigO_zero, sub_self, Asymptotics.IsBigO.congr_left, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ f' x - f' x) g'

Tactic:
(isLittleO_zero g' l).congr_left fun _x => (sub_self _).symm

Premises used: sub_self, Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.congr_left, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
c : ℝ
f'' : α → E''
l : Filter α
⊢ (IsBigOWith.{u_1, u_9, u_7} (F := F') c l f'' fun (_x : α) ↦ 0) ↔ f'' =ᶠ[l] 0

Tactic:
simp only [IsBigOWith_def, norm_zero, mul_zero, norm_le_zero_iff, EventuallyEq, Pi.zero_apply]

Premises used: Asymptotics.IsBigOWith_def, norm_zero, Pi.zero_apply, Filter.EventuallyEq, MulZeroClass.mul_zero, norm_le_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''
f'' : α → E''
l : Filter α
⊢ (IsBigO.{u_1, u_9, u_7} (F := F') l f'' fun (_x : α) ↦ 0) ↔ f'' =ᶠ[l] 0

Tactic:
⟨fun h =>
    let ⟨_c, hc⟩ := h.isBigOWith
    isBigOWith_zero_right_iff.1 hc,
    fun h => (isBigOWith_zero_right_iff.2 h : IsBigOWith 1 _ _ _).isBigO⟩

Premises used: Iff.mpr, Asymptotics.isBigOWith_zero_right_iff, _private.0.Asymptotics.isBigO_zero_right_iff.match_1, Filter.EventuallyEq, Iff.intro, Iff.mp, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith, OfNat.ofNat