-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsLittleO.listProd {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜}
    (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i) :
    (fun x ↦ (L.map (f · x)).prod) =o[l] (fun x ↦ (L.map (g · x)).prod)

Proof state:
case cons.inl
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hi : f i =o[l] g i
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x =>
    g i x * (List.map (fun x_1 => g x_1 x) L).prod

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

Result:
no goals

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : 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
⊢ (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod

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

Result:
no goals

Proof state:
case nil
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ [], f i =O[l] g i
h₂ : ∃ i ∈ [], f i =o[l] g i
⊢ (fun x => (List.map (fun x_1 => f x_1 x) []).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) []).prod

Tactic:
simp at h₂

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hL : ∃ x ∈ L, f x =o[l] g x
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x =>
    g i x * (List.map (fun x_1 => g x_1 x) L).prod

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

Result:
no goals

Proof state:
case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
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
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x =>
    g i x * (List.map (fun x_1 => g x_1 x) L).prod

Tactic:
cases h₂ with
| inl hi => exact hi.mul_isBigO <| .listProd h₁.2
| inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL

Result:
no goals

Proof state:
case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
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
⊢ (fun x => (List.map (fun x_1 => f x_1 x) (i :: L)).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) (i :: L)).prod

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

Result:
case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
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
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x =>
    g i x * (List.map (fun x_1 => g x_1 x) L).prod