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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
simp :
  (∃ (c : ℝ), ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x : α × β | ‖f x‖ ≤ c * ‖g x‖}) →
    {a : α | ∃ (c : ℝ), {x : β | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l
⊢ f =O[l ×ˢ l'] g →
    ∀ᶠ (a : α) in l, IsBigO.{u_2, u_3, u_4} (E := E) (F := F) l' (fun (x : β) ↦ f (a, x)) fun (x : β) ↦ g (a, x)

Tactic:
simp only [isBigO_iff, eventually_iff, mem_prod_iff]

Premises used: Filter.eventually_iff, Asymptotics.isBigO_iff, Filter.mem_prod_iff
-- 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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x : α × β | ‖f x‖ ≤ c * ‖g x‖}
⊢ {a : α | ∃ (c : ℝ), {x : β | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l

Tactic:
mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩

Premises used: And.intro, Exists.intro, Filter.mem_of_superset
-- 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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x : α × β | ‖f x‖ ≤ c * ‖g x‖}
⊢ {a : α | ∃ (c : ℝ), {x : β | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l

Tactic:
exact mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩
-- 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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
simp :
  (∃ (c : ℝ), ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x : α × β | ‖f x‖ ≤ c * ‖g x‖}) →
    {b : β | ∃ (c : ℝ), {x : α | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'
⊢ f =O[l ×ˢ l'] g →
    ∀ᶠ (b : β) in l', IsBigO.{u_1, u_3, u_4} (E := E) (F := F) l (fun (x : α) ↦ f (x, b)) fun (x : α) ↦ g (x, b)

Tactic:
simp only [isBigO_iff, eventually_iff, mem_prod_iff]

Premises used: Filter.eventually_iff, Asymptotics.isBigO_iff, Filter.mem_prod_iff
-- 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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x : α × β | ‖f x‖ ≤ c * ‖g x‖}
⊢ {b : β | ∃ (c : ℝ), {x : α | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'

Tactic:
mem_of_superset ht₂ fun _ hb ↦ ⟨c, mem_of_superset ht₁ fun _ ha ↦ ht ⟨ha, hb⟩⟩

Premises used: And.intro, Exists.intro, Filter.mem_of_superset
-- 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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x : α × β | ‖f x‖ ≤ c * ‖g x‖}
⊢ {b : β | ∃ (c : ℝ), {x : α | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'

Tactic:
exact mem_of_superset ht₂ fun _ hb ↦ ⟨c, mem_of_superset ht₁ fun _ ha ↦ ht ⟨ha, hb⟩⟩
-- 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
l : Filter α
l' : Filter β
simp :
  (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ (c : ℝ) (pa : α → Prop),
      (∀ᶠ (x : α) in l, pa x) ∧
        ∃ (pb : β → Prop),
          (∀ᶠ (y : β) in l', pb y) ∧
            ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖
⊢ f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [isBigO_iff, eventually_prod_iff]

Premises used: Asymptotics.isBigO_iff, Filter.eventually_prod_iff
-- 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
l : Filter α
l' : Filter β
⊢ (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ (c : ℝ) (pa : α → Prop),
      (∀ᶠ (x : α) in l, pa x) ∧
        ∃ (pb : β → Prop),
          (∀ᶠ (y : β) in l', pb y) ∧
            ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖

Tactic:
fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

Premises used: Norm.norm, HMul.hMul, Filter.Eventually, Exists, _private.0.Asymptotics.IsBigO.comp_fst.match_1, LE.le, Filter.eventually_true, And, And.intro, True, Exists.intro
-- 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
l : Filter α
l' : Filter β
⊢ (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ (c : ℝ) (pa : α → Prop),
      (∀ᶠ (x : α) in l, pa x) ∧
        ∃ (pb : β → Prop),
          (∀ᶠ (y : β) in l', pb y) ∧
            ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖

Tactic:
exact fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩
-- 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
l : Filter α
l' : Filter β
simp :
  (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ (c : ℝ) (pa : β → Prop),
      (∀ᶠ (x : β) in l', pa x) ∧
        ∃ (pb : α → Prop),
          (∀ᶠ (y : α) in l, pb y) ∧
            ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖
⊢ f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [isBigO_iff, eventually_prod_iff]

Premises used: Asymptotics.isBigO_iff, Filter.eventually_prod_iff
-- 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
l : Filter α
l' : Filter β
⊢ (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ (c : ℝ) (pa : β → Prop),
      (∀ᶠ (x : β) in l', pa x) ∧
        ∃ (pb : α → Prop),
          (∀ᶠ (y : α) in l, pb y) ∧
            ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Tactic:
fun ⟨c, hc⟩ ↦ ⟨c, fun _ ↦ True, eventually_true l', _, hc, fun _ ↦ id⟩

Premises used: Norm.norm, HMul.hMul, Filter.Eventually, Exists, id, _private.0.Asymptotics.IsBigO.comp_fst.match_1, LE.le, Filter.eventually_true, And, And.intro, True, Exists.intro
-- 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
l : Filter α
l' : Filter β
⊢ (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ (c : ℝ) (pa : β → Prop),
      (∀ᶠ (x : β) in l', pa x) ∧
        ∃ (pb : α → Prop),
          (∀ᶠ (y : α) in l, pb y) ∧
            ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Tactic:
exact fun ⟨c, hc⟩ ↦ ⟨c, fun _ ↦ True, eventually_true l', _, hc, fun _ ↦ id⟩
-- 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
l : Filter α
l' : Filter β
simp :
  (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ (pa : α → Prop),
          (∀ᶠ (x : α) in l, pa x) ∧
            ∃ (pb : β → Prop),
              (∀ᶠ (y : β) in l', pb y) ∧
                ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖
⊢ f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [isLittleO_iff, eventually_prod_iff]

Premises used: Filter.eventually_prod_iff, Asymptotics.isLittleO_iff
-- 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
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ (pa : α → Prop),
          (∀ᶠ (x : α) in l, pa x) ∧
            ∃ (pb : β → Prop),
              (∀ᶠ (y : β) in l', pb y) ∧
                ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖

Tactic:
fun h _ hc ↦ ⟨_, h hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

Premises used: Norm.norm, HMul.hMul, LE.le, Filter.eventually_true, And.intro, True, Exists.intro
-- 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
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ (pa : α → Prop),
          (∀ᶠ (x : α) in l, pa x) ∧
            ∃ (pb : β → Prop),
              (∀ᶠ (y : β) in l', pb y) ∧
                ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖

Tactic:
exact fun h _ hc ↦ ⟨_, h hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩
-- 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
l : Filter α
l' : Filter β
simp :
  (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ (pa : β → Prop),
          (∀ᶠ (x : β) in l', pa x) ∧
            ∃ (pb : α → Prop),
              (∀ᶠ (y : α) in l, pb y) ∧
                ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖
⊢ f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [isLittleO_iff, eventually_prod_iff]

Premises used: Filter.eventually_prod_iff, Asymptotics.isLittleO_iff
-- 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
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ (pa : β → Prop),
          (∀ᶠ (x : β) in l', pa x) ∧
            ∃ (pb : α → Prop),
              (∀ᶠ (y : α) in l, pb y) ∧
                ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Tactic:
fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩

Premises used: Norm.norm, HMul.hMul, id, LE.le, Filter.eventually_true, And.intro, True, Exists.intro
-- 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
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ (pa : β → Prop),
          (∀ᶠ (x : β) in l', pa x) ∧
            ∃ (pb : α → Prop),
              (∀ᶠ (y : α) in l, pb y) ∧
                ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Tactic:
exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : IsBigOWith c l f' k'
hg : IsBigOWith c l g' k'
rw :
  ∀ (hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖) (hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖),
    ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖
⊢ IsBigOWith (E := E' × F') c l (fun (x : α) ↦ (f' x, g' x)) k'

Tactic:
rw [isBigOWith_iff] at *

Premises used: Asymptotics.isBigOWith_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖
hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖
x : α
⊢ ‖f' x‖ ≤ c * ‖k' x‖ → ‖g' x‖ ≤ c * ‖k' x‖ → ‖(f' x, g' x)‖ ≤ c * ‖k' x‖

Tactic:
max_le

Premises used: max_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖
hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖f' x‖ ≤ c * ‖k' x‖) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖g' x‖ ≤ c * ‖k' x‖) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖(f' x, g' x)‖ ≤ c * ‖k' x‖) x} x}
            x}
      a
h₁ h₂ : ∀ (x : α), ‖f' x‖ ≤ c * ‖k' x‖ → ‖g' x‖ ≤ c * ‖k' x‖ → ‖(f' x, g' x)‖ ≤ c * ‖k' x‖
⊢ ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖

Tactic:
filter_upwards [hf, hg] with x using max_le

Premises used: max_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c c' : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : IsBigOWith c l f' k'
hg : IsBigOWith c' l g' k'
⊢ IsBigOWith (E := E' × F') (max c c') l (fun (x : α) ↦ (f' x, g' x)) k'

Tactic:
(hf.weaken <| le_max_left c c').prod_left_same (hg.weaken <| le_max_right c c')

Premises used: le_max_right, Asymptotics.IsBigOWith.weaken, le_max_left, Asymptotics.IsBigOWith.prod_left_same
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
h : IsBigOWith (E := E' × F') c l (fun (x : α) ↦ (f' x, g' x)) k'
⊢ IsBigOWith c l f' k'

Tactic:
(isBigOWith_fst_prod.trans h zero_le_one).congr_const <| one_mul c

Premises used: Asymptotics.IsBigOWith.trans, zero_le_one, one_mul, Asymptotics.isBigOWith_fst_prod, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
h : IsBigOWith (E := E' × F') c l (fun (x : α) ↦ (f' x, g' x)) k'
⊢ IsBigOWith c l g' k'

Tactic:
(isBigOWith_snd_prod.trans h zero_le_one).congr_const <| one_mul c

Premises used: Asymptotics.IsBigOWith.trans, zero_le_one, Asymptotics.isBigOWith_snd_prod, one_mul, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
⊢ IsBigOWith (E := E' × F') c l (fun (x : α) ↦ (f' x, g' x)) k' ↔ IsBigOWith c l f' k' ∧ IsBigOWith c l g' k'

Tactic:
⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left_same h.2⟩

Premises used: Asymptotics.IsBigOWith.prod_left_fst, Asymptotics.IsBigOWith.prod_left_snd, And.right, And.left, And.intro, Iff.intro, Asymptotics.IsBigOWith.prod_left_same
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : f' =O[l] k'
hg : g' =O[l] k'
⊢ IsBigO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k'

Tactic:
let ⟨_c, hf⟩ := hf.isBigOWith
  let ⟨_c', hg⟩ := hg.isBigOWith
  (hf.prod_left hg).isBigO

Premises used: Asymptotics.IsBigO, Prod.mk, _private.0.Asymptotics.IsBigO.prod_left.match_1, Asymptotics.IsBigOWith.prod_left, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
⊢ IsBigO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k' → f' =O[l] k'

Tactic:
IsBigO.trans isBigO_fst_prod

Premises used: Asymptotics.isBigO_fst_prod, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
⊢ IsBigO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k' → g' =O[l] k'

Tactic:
IsBigO.trans isBigO_snd_prod

Premises used: Asymptotics.IsBigO.trans, Asymptotics.isBigO_snd_prod
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
⊢ IsBigO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k' ↔ f' =O[l] k' ∧ g' =O[l] k'

Tactic:
⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left h.2⟩

Premises used: Asymptotics.IsBigO.prod_left_fst, Asymptotics.IsBigO.prod_left_snd, And.right, And.left, And.intro, Iff.intro, Asymptotics.IsBigO.prod_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : f' =o[l] k'
hg : g' =o[l] k'
⊢ IsLittleO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k'

Tactic:
IsLittleO.of_isBigOWith fun _c hc =>
    (hf.forall_isBigOWith hc).prod_left_same (hg.forall_isBigOWith hc)

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsBigOWith.prod_left_same
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
⊢ IsLittleO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k' → f' =o[l] k'

Tactic:
IsBigO.trans_isLittleO isBigO_fst_prod

Premises used: Asymptotics.isBigO_fst_prod, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
⊢ IsLittleO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k' → g' =o[l] k'

Tactic:
IsBigO.trans_isLittleO isBigO_snd_prod

Premises used: Asymptotics.isBigO_snd_prod, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
⊢ IsLittleO (E := E' × F') l (fun (x : α) ↦ (f' x, g' x)) k' ↔ f' =o[l] k' ∧ g' =o[l] k'

Tactic:
⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left h.2⟩

Premises used: Asymptotics.IsLittleO.prod_left_fst, Asymptotics.IsLittleO.prod_left, And.right, And.left, Asymptotics.IsLittleO.prod_left_snd, And.intro, Iff.intro
-- 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 : ℝ
f'' : α → E''
g'' : α → F''
l : Filter α
h : IsBigOWith c l f'' g''
x : α
hx : ‖f'' x‖ ≤ c * ‖g'' x‖
hg : g'' x = 0
⊢ ‖f'' x‖ ≤ 0

Tactic:
simpa [hg] using hx
-- 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''
l : Filter α
h : f'' =O[l] g''
⊢ ∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0

Tactic:
let ⟨_C, hC⟩ := h.isBigOWith
  hC.eq_zero_imp

Premises used: Filter.Eventually, _private.0.Asymptotics.IsBigO.eq_zero_imp.match_1, Asymptotics.IsBigOWith.eq_zero_imp, Asymptotics.IsBigO.isBigOWith
-- 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
rw :
  ∀ (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‖
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (c₁ + c₂) l (fun (x : α) ↦ f₁ x + f₂ x) g

Tactic:
rw [IsBigOWith_def] at *

Premises used: Asymptotics.IsBigOWith_def
-- 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₁ : ∀ᶠ (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₁ + c₂) * ‖g x‖

Tactic:
calc
      ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g x‖ + c₂ * ‖g x‖ := norm_add_le_of_le hx₁ hx₂
      _ = (c₁ + c₂) * ‖g x‖ := (add_mul _ _ _).symm

Premises used: add_mul, Trans.trans, norm_add_le_of_le, Eq.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'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g x‖
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖f₁ x‖ ≤ c₁ * ‖g x‖) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖f₂ x‖ ≤ c₂ * ‖g x‖) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖) x} x}
            x}
      a
h₃ h₄ : ∀ (x : α) (hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g x‖) (hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g x‖), ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖

Tactic:
filter_upwards [h₁, h₂] with x hx₁ hx₂ using
    calc
      ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g x‖ + c₂ * ‖g x‖ := norm_add_le_of_le hx₁ hx₂
      _ = (c₁ + c₂) * ‖g x‖ := (add_mul _ _ _).symm

Premises used: add_mul, HAdd.hAdd, Eq.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₁ : 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:
let ⟨_c₁, hc₁⟩ := h₁.isBigOWith
  let ⟨_c₂, hc₂⟩ := h₂.isBigOWith
  (hc₁.add hc₂).isBigO

Premises used: Asymptotics.IsBigO, _private.0.Asymptotics.IsBigO.add.match_1, Asymptotics.IsBigOWith.add, HAdd.hAdd, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith
-- 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:
IsLittleO.of_isBigOWith fun c cpos =>
    ((h₁.forall_isBigOWith <| half_pos cpos).add (h₂.forall_isBigOWith <|
      half_pos cpos)).congr_const (add_halves c)

Premises used: add_halves, half_pos, Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsBigOWith.add, Asymptotics.IsBigOWith.congr_const
-- 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₁ : IsBigOWith c₁ l f₁ g₁
h₂ : IsBigOWith c₂ l f₂ g₂
rw :
  ∀ (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‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (max c₁ c₂) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
rw [IsBigOWith_def] at *

Premises used: Asymptotics.IsBigOWith_def