awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (IsLittleO.{u_1, u_3, u_6} (F := E') l f fun (x : α) ↦ c • f' x) ↔ f =o[l] f'
have rw : (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =o[l] f'
Tactic: rw [← isLittleO_norm_right]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =o[l] f'
have simp : (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =o[l] f'
Tactic: simp only [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =o[l] f'
have rw : (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖f' x‖) ↔ f =o[l] f'
Tactic: rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖f' x‖) ↔ f =o[l] f'
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =o[l] f'
have rw₁ : f =o[l] f' ↔ f =o[l] f'
Tactic: rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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₁ : IsBigOWith c l k₁ k₂
h₂ : IsBigOWith c' l f' g'
⊢ IsBigOWith.{u_1, u_6, u_7} (E := E') (F := F') (c * c') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
have simp : ∀ (h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖) (h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖),
  ∀ᶠ (x : α) in l, ‖k₁ x • f' x‖ ≤ c * c' * ‖k₂ x • g' x‖
Tactic: simp only [IsBigOWith_def] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ∀ᶠ (x : α) in l, ‖k₁ x • f' x‖ ≤ c * c' * ‖k₂ x • g' x‖
have h : ∀ (a : α) (hx₁ : ‖k₁ a‖ ≤ c * ‖k₂ a‖) (hx₂ : ‖f' a‖ ≤ c' * ‖g' a‖), ‖k₁ a • f' a‖ ≤ c * c' * ‖k₂ a • g' a‖
Tactic: filter_upwards [h₁, h₂] with _ hx₁ hx₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ‖k₁ a • f' a‖ ≤ c * c' * ‖k₂ a • g' a‖
have h : ‖k₁ a‖ * ‖f' a‖ ≤ c * c' * ‖k₂ a • g' a‖
Tactic: apply le_trans (norm_smul_le _ _)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ‖k₁ a‖ * ‖f' a‖ ≤ c * c' * ‖k₂ a • g' a‖
have h : c * c' * ‖k₂ a • g' a‖ = c * ‖k₂ 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.Lemmas (goal)
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‖
⊢ c * c' * ‖k₂ a • g' a‖ = c * ‖k₂ a‖ * (c' * ‖g' a‖)
have h : c * c' * (‖k₂ a‖ * ‖g' a‖) = c * ‖k₂ a‖ * (c' * ‖g' a‖)
Tactic: rw [norm_smul, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖)
⊢ c * c' * ‖k₂ a • g' a‖ = c * ‖k₂ a‖ * (c' * ‖g' a‖)
have h₃ : c * ‖k₂ a‖ * (c' * ‖g' a‖) = c * ‖k₂ a‖ * (c' * ‖g' a‖)
Tactic: rw [norm_smul, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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'
⊢ IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
have 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
Tactic: obtain ⟨c₁, h₁⟩ := h₁.isBigOWith
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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₂
⊢ IsBigO.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ k₁ x • f' x) fun (x : α) ↦ k₂ x • g' x
have 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
Tactic: obtain ⟨c₂, h₂⟩ := h₂.isBigOWith
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
have 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
Tactic: simp only [IsLittleO_def] at *
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ 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
have 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
Tactic: rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
have 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
Tactic: simp only [IsLittleO_def] at *
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ 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
have 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
Tactic: rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ 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))
have 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)
Tactic: simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ 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)
have 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) [])
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)
Cleared hypotheses: L, hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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) [])
⊢ 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)
have 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))
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)
Cleared hypotheses: L, hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ 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)
have 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 ι))
Tactic: obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ 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))
have 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)
Tactic: simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
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)
have cons : ∀ (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: cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
h₂ : f i =o[l] g i ∨ ∃ x ∈ L, f x =o[l] g x
cons :
  ∀ (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)
⊢ 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)
have cons₁ : ∀ (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: cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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 : ι → α → 𝕜
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)
have nil : ∀ (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: induction L with
  | nil => simp at h₂
  | cons i L ihL =>
    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢
    cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL
Cleared hypotheses: L, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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 : ι → α → 𝕜
h₁ : ∀ i ∈ L, f i =O[l] g i
h₂ : ∃ i ∈ L, f i =o[l] g i
nil :
  ∀ (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) [])
⊢ 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)
have cons : ∀ (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),
  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: induction L with
  | nil => simp at h₂
  | cons i L ihL =>
    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢
    cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL
Cleared hypotheses: L, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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 : ι → α → 𝕜
h₁ : ∀ i ∈ s, f i =O[l] g i
h₂ : ∃ i ∈ s, f i =o[l] g i
⊢ IsLittleO.{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)
have obtain : ∀ (l_1 : List ι) (h₁ : ∀ i ∈ (↑l_1 : Multiset ι), f i =O[l] g i) (h₂ : ∃ i ∈ (↑l_1 : Multiset ι), f i =o[l] g i),
  IsLittleO.{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 ι))
Tactic: obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
Cleared hypotheses: s, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
⊢ IsLittleO.{u_1, u_15, u_15} (E := 𝕜) (F := 𝕜) l (fun (x : α) ↦ f x / g x) fun (_x : α) ↦ 1
have x : IsLittleO.{u_1, u_15, u_15} (E := 𝕜) (F := 𝕜) l (fun (x : α) ↦ f x / g x) fun (x : α) ↦ g x / g x
Tactic: calc
      (fun x => f x / g x) =o[l] fun x => g x / g x := by
        simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)
      _ =O[l] fun _x => (1 : 𝕜) := isBigO_of_le _ fun x => by simp [div_self_le_one]