awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a : α
hx₁ : ‖k₁ a‖ ≤ c * ‖k₂ a‖
hx₂ : ‖f' a‖ ≤ c' * ‖g' a‖
h : c * c' * (‖k₂ a‖ * ‖g' a‖) = c * ‖k₂ a‖ * (c' * ‖g' a‖)
h₃ h₄ : c * ‖k₂ a‖ * (c' * ‖g' a‖) = c * ‖k₂ a‖ * (c' * ‖g' a‖)
⊢ c * c' * ‖k₂ a • g' a‖ = c * ‖k₂ a‖ * (c' * ‖g' a‖)

Tactic:
rw [norm_smul, mul_mul_mul_comm]

Premises used: norm_smul, mul_mul_mul_comm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : f' =O[l] g'
obtain :
  ∀ (c₁ : ℝ) (h₁ : IsBigOWith c₁ l k₁ k₂),
    IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
⊢ IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁_1 : k₁ =O[l] k₂
h₂ : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
obtain :
  ∀ (c₂ : ℝ) (h₂ : IsBigOWith c₂ l f' g'),
    IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
⊢ IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁_1 : k₁ =O[l] k₂
h₂_1 : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
c₂ : ℝ
h₂ : IsBigOWith c₂ l f' g'
⊢ IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

Tactic:
(h₁.smul h₂).isBigO

Premises used: Asymptotics.IsBigOWith.smul, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁_1 : k₁ =O[l] k₂
h₂_1 : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
c₂ : ℝ
h₂ : IsBigOWith c₂ l f' g'
⊢ IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

Tactic:
exact (h₁.smul h₂).isBigO

Premises used: Asymptotics.IsBigOWith.smul, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : f' =o[l] g'
simp :
  ∀ (h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g') ⦃c : ℝ⦄,
    0 < c → IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

Tactic:
simp only [IsLittleO_def] at *

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
rcases :
  ∀ (c' : ℝ) (c'pos : c' > 0) (hc' : IsBigOWith c' l k₁ k₂),
    IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l k₁ k₂
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: ne_of_gt, Asymptotics.IsBigOWith.smul, mul_div_cancel₀, div_pos, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l k₁ k₂
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: ne_of_gt, Asymptotics.IsBigOWith.smul, mul_div_cancel₀, div_pos, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =o[l] k₂
h₂ : f' =O[l] g'
simp :
  ∀ (h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂) ⦃c : ℝ⦄,
    0 < c → IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

Tactic:
simp only [IsLittleO_def] at *

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
rcases :
  ∀ (c' : ℝ) (c'pos : c' > 0) (hc' : IsBigOWith c' l f' g'),
    IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f' g'
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: div_mul_cancel₀, ne_of_gt, Asymptotics.IsBigOWith.smul, div_pos, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f' g'
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') c l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

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

Premises used: div_mul_cancel₀, ne_of_gt, Asymptotics.IsBigOWith.smul, div_pos, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedRing R
inst_3 : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst_4 : Module R E'
inst_5 : IsBoundedSMul R E'
inst_6 : Module 𝕜' F'
inst_7 : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =o[l] k₂
h₂ : f' =o[l] g'
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x

Tactic:
h₁.smul_isBigO h₂.isBigO

Premises used: Asymptotics.IsLittleO.smul_isBigO, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i =O[l] g i
⊢ IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) []))
    fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) [])

Tactic:
simp [isBoundedUnder_const]

Premises used: Filter.isBoundedUnder_const
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (hf : ∀ i ∈ L, f i =O[l] g i),
    IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
hf : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1
cons :
  ∀ (hf : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x),
    IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
      (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
      g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
⊢ IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (i :: L)))
    fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) (i :: L))

Tactic:
simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢

Premises used: List.map_cons, List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (hf : ∀ i ∈ L, f i =O[l] g i),
    IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
hf : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
⊢ IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
    fun (x : α) ↦ g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
hf.1.mul (ihL hf.2)

Premises used: Asymptotics.IsBigO.mul, And.right, And.left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (hf : ∀ i ∈ L, f i =O[l] g i),
    IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
hf : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
⊢ IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
    fun (x : α) ↦ g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
exact hf.1.mul (ihL hf.2)

Premises used: Asymptotics.IsBigO.mul, And.right, And.left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
L : List ι
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ L, f i =O[l] g i
nil :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i =O[l] g i),
    IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) []))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) [])
cons :
  ∀ (i : ι) (L : List ι)
    (ihL :
      ∀ (hf : ∀ i ∈ L, f i =O[l] g i),
        IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
          fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L))
    (hf : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1),
    IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (i :: L)))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) (i :: L))
⊢ IsBigO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
    fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
induction L with
  | nil => simp [isBoundedUnder_const]
  | cons i L ihL =>
    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢
    exact hf.1.mul (ihL hf.2)

Premises used: List.map_cons, List.forall_mem_cons, Filter.isBoundedUnder_const, List.prod_cons
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ s, f i =O[l] g i
⊢ ∃ (l : List ι), (↑l : Multiset ι) = s

Tactic:
Quotient.mk_surjective s

Premises used: Multiset, Multiset.ofList, Quotient.mk_surjective
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ s, f i =O[l] g i
obtain :
  ∀ (l_1 : List ι) (hf : ∀ i ∈ (↑l_1 : Multiset ι), f i =O[l] g i),
    IsBigO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l
      (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l_1 : Multiset ι))) fun (x : α) ↦
      Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l_1 : Multiset ι))
⊢ IsBigO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) s))
    fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) s)

Tactic:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s

Premises used: List, Quotient.mk_surjective, rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l_1 : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
hf : ∀ i ∈ (↑l : Multiset ι), f i =O[l_1] g i
⊢ IsBigO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l_1
    (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l : Multiset ι))) fun (x : α) ↦
    Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l : Multiset ι))

Tactic:
mod_cast IsBigO.listProd hf

Premises used: Multiset.map, Asymptotics.IsBigO.listProd, Multiset.prod, Asymptotics.IsBigO, cast, Multiset.ofList, Eq.refl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l_1 : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
hf : ∀ i ∈ (↑l : Multiset ι), f i =O[l_1] g i
⊢ IsBigO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l_1
    (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l : Multiset ι))) fun (x : α) ↦
    Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l : Multiset ι))

Tactic:
exact mod_cast IsBigO.listProd hf

Premises used: Asymptotics.IsBigO.listProd
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
s : Finset ι
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ s, f i =O[l] g i
⊢ IsBigO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l (fun (x : α) ↦ ∏ i ∈ s, f i x) fun (x : α) ↦ ∏ i ∈ s, g i x

Tactic:
.multisetProd hf

Premises used: Finset.prod, Asymptotics.IsBigO.multisetProd
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i =O[l] g i
h₂ : ∃ (i : ι), Membership.mem (γ := List ι) [] i ∧ f i =o[l] g i
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) []))
    fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) [])

Tactic:
simp at h₂
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h₁ : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1
h₂ : ∃ i_1 ∈ i :: L, f i_1 =o[l] g i_1
cons :
  ∀ (h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x) (h₂ : f i =o[l] g i ∨ ∃ x ∈ L, f x =o[l] g x),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
      (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
      g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
    (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (i :: L))) fun (x : α) ↦
    List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) (i :: L))

Tactic:
simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢

Premises used: List.map_cons, List.forall_mem_cons, List.prod_cons, List.exists_mem_cons_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hi : f i =o[l] g i
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
    (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
    g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
hi.mul_isBigO <| .listProd h₁.2

Premises used: Asymptotics.IsBigO.listProd, And.right, Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hi : f i =o[l] g i
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
    (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
    g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
exact hi.mul_isBigO <| .listProd h₁.2

Premises used: Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hL : ∃ x ∈ L, f x =o[l] g x
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
    (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
    g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
h₁.1.mul_isLittleO <| ihL h₁.2 hL

Premises used: Asymptotics.IsBigO.mul_isLittleO, And.right, And.left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hL : ∃ x ∈ L, f x =o[l] g x
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
    (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
    g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
exact h₁.1.mul_isLittleO <| ihL h₁.2 hL

Premises used: Asymptotics.IsBigO.mul_isLittleO, And.right, And.left