-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
α : Type u_5
H : Type u_6
inst_7 : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖p₁ x k‖
hpf :
  ∀ k ≤ n,
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin k) ↦ F) G) l
      (fun (a : α) ↦ p₁ a k - p₂ a k) f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖q₂ x k‖
hqf :
  ∀ k ≤ n,
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F) l
      (fun (a : α) ↦ q₁ a k - q₂ a k) f
c : OrderedFinpartition n
h : Membership.mem (γ := Finset (OrderedFinpartition n)) Finset.univ c
H₁ :
  Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (F := ℝ) l
    (fun (x : α) ↦ p₁ x c.length) 1
H₂ :
  Asymptotics.IsBigO (E :=
    (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) (F := ℝ) l
    (fun (x : α) (m : Fin c.length) ↦ q₁ x (c.partSize m)) 1
H₃ :
  Asymptotics.IsBigO (E :=
    (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) (F := ℝ) l
    (fun (x : α) (m : Fin c.length) ↦ q₂ x (c.partSize m)) 1
H₄ :
  Asymptotics.IsBigO (E :=
    (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) l
    (fun (a : α) (m : Fin c.length) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F)
        (q₁ a (c.partSize m)) (q₂ a (c.partSize m)))
    f
H₅ :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) l
    (fun (x : α) ↦
      norm (E :=
            ((i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ×
              ((i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F))
            (fun (m : Fin c.length) ↦ q₁ x (c.partSize m), fun (m : Fin c.length) ↦ q₂ x (c.partSize m)) ^
          (c.length - 1) *
        norm (E :=
          (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
          fun (m : Fin c.length) ↦
          HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F)
            (q₁ x (c.partSize m)) (q₂ x (c.partSize m)))
    fun (x : α) ↦ HPow.hPow (α := ℝ) (1 x) (c.length - 1) * ‖f x‖
⊢ Asymptotics.IsBigO (E := ℝ) l
    (fun (x : α) ↦
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (p₁ x c.length) *
            (↑c.length : ℝ) *
          max
              (norm (E :=
                (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                fun (m : Fin c.length) ↦ q₁ x (c.partSize m))
              (norm (E :=
                (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                fun (m : Fin c.length) ↦ q₂ x (c.partSize m)) ^
            (c.length - 1) *
        ‖HSub.hSub (α :=
            (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
            (fun (m : Fin c.length) ↦ q₁ x (c.partSize m)) fun (m : Fin c.length) ↦ q₂ x (c.partSize m)‖)
    f

Tactic:
simpa [mul_assoc] using H₁.norm_left.mul <| H₅.const_mul_left c.length

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.const_mul_left, mul_assoc, Asymptotics.IsBigO.mul, Nat.cast, OrderedFinpartition.length