awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =O[l] g
have simp : (∃ (c : ℝ), IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =o[l] g
have simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
Tactic: simp only [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigO.{u_1, u_3, u_7} (F := F') l f fun (x : α) ↦ -g' x) ↔ f =O[l] g'
have simp : (∃ (c : ℝ), IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔ ∃ (c : ℝ), IsBigOWith c l f g'
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (IsLittleO.{u_1, u_3, u_7} (F := F') l f fun (x : α) ↦ -g' x) ↔ f =o[l] g'
have simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔
  ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'
Tactic: simp only [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ -f' x) g ↔ f' =O[l] g
have simp : (∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ -f' x) g ↔ f' =o[l] g
have simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔
  ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
Tactic: simp only [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 β
⊢ 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)
have 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
Tactic: simp only [isBigO_iff, eventually_iff, mem_prod_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 β
⊢ 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)
have 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'
Tactic: simp only [isBigO_iff, eventually_iff, mem_prod_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 β
⊢ f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)
have 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)‖
Tactic: simp only [isBigO_iff, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 β
⊢ f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)
have 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)‖
Tactic: simp only [isBigO_iff, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 β
⊢ f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)
have 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)‖
Tactic: simp only [isLittleO_iff, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 β
⊢ f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)
have 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)‖
Tactic: simp only [isLittleO_iff, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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'
⊢ IsBigOWith (E := E' × F') c l (fun (x : α) ↦ (f' x, g' x)) k'
have 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‖
Tactic: rw [isBigOWith_iff] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖
have 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
Tactic: filter_upwards [hf, hg] with x using max_le
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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
⊢ ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖
have h₁ : ∀ (a : α), ‖f' a‖ ≤ c * ‖k' a‖ → ‖g' a‖ ≤ c * ‖k' a‖ → ‖(f' a, g' a)‖ ≤ c * ‖k' a‖
Tactic: filter_upwards [hf, hg] with x using max_le
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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
have 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‖
Tactic: rw [IsBigOWith_def] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 : α) in l, ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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
⊢ ∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖
have h₃ : ∀ (a : α), ‖f₁ a‖ ≤ c₁ * ‖g a‖ → ‖f₂ a‖ ≤ c₂ * ‖g a‖ → ‖f₁ a + f₂ a‖ ≤ (c₁ + c₂) * ‖g a‖
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
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₂
⊢ 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‖
have 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‖‖
Tactic: rw [IsBigOWith_def] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 : α) in l, ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
have 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‖‖
Tactic: filter_upwards [h₁, h₂] with x hx₁ hx₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖
have h₃ : c₁ ≤ max c₁ c₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₂
⊢ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖
have h₄ : c₂ ≤ max c₁ c₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖
⊢ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
have rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖)
⊢ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
have rw₁ : max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖
Tactic: rw [Real.norm_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)), mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
have x₁ : c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖
⊢ ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
have x₂ : max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₂
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖
have 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‖
Tactic: obtain ⟨c₁, hc₁⟩ := h₁.isBigOWith
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₁
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖
have 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‖
Tactic: obtain ⟨c₂, hc₂⟩ := h₂.isBigOWith
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖
have refine_1 : ∀ (x : α), ‖g₁ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
Tactic: refine (h₁.trans_le fun x => ?_).add (h₂.trans_le ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖‖
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (x : α) ↦ f₁ x + f₂ x) fun (x : α) ↦ ‖g₁ x‖ + ‖g₂ x‖
have refine_2 : ∀ (x : α), ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
Tactic: refine (h₁.trans_le fun x => ?_).add (h₂.trans_le ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 α
⊢ IsBigOWith.{u_1, u_3, u_10} (E := E) (F := F'') (‖c‖ / ‖c'‖) l (fun (_x : α) ↦ c) fun (_x : α) ↦ c'
have simp : ∀ᶠ (x : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖
Tactic: simp only [IsBigOWith_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖
have h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x} a
Tactic: apply univ_mem'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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 : α
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x} x
have h : ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖
Tactic: rw [mem_setOf, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hc')]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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'‖
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x} x
have h₁ : ‖c‖ ≤ ‖c‖
Tactic: rw [mem_setOf, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hc')]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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
⊢ (IsBigO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ c') ↔ c' = 0 → c = 0
have 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
Tactic: rcases eq_or_ne c' 0 with (rfl | hc')
Cleared hypotheses: c'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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
⊢ (IsBigO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ c) fun (_x : α) ↦ c') ↔ c' = 0 → c = 0
have 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
Tactic: rcases eq_or_ne c' 0 with (rfl | hc')
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₂
⊢ 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
have 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‖
Tactic: simp only [IsBigOWith_def] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x * f₂ x‖ ≤ c₁ * c₂ * ‖g₁ x * g₂ x‖
have h : ∀ (a : α) (hx₁ : ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖) (hx₂ : ‖f₂ a‖ ≤ c₂ * ‖g₂ a‖), ‖f₁ a * f₂ a‖ ≤ c₁ * c₂ * ‖g₁ a * g₂ a‖
Tactic: filter_upwards [h₁, h₂] with _ hx₁ hx₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₁ * c₂ * ‖g₁ a * g₂ a‖
have h : ‖f₁ a‖ * ‖f₂ a‖ ≤ c₁ * c₂ * ‖g₁ a * g₂ a‖
Tactic: apply le_trans (norm_mul_le _ _)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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₁ * c₂ * ‖g₁ a * g₂ a‖
have h : c₁ * c₂ * ‖g₁ a * g₂ a‖ = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
Tactic: convert! mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖
⊢ c₁ * c₂ * ‖g₁ a * g₂ a‖ = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
have h : c₁ * c₂ * (‖g₁ a‖ * ‖g₂ a‖) = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
Tactic: rw [norm_mul, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
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‖)
⊢ c₁ * c₂ * ‖g₁ a * g₂ a‖ = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
have h₃ : c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖) = c₁ * ‖g₁ a‖ * (c₂ * ‖g₂ a‖)
Tactic: rw [norm_mul, mul_mul_mul_comm]