-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
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
⊢ 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
have 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‖
Tactic: have H₅ := ((H₂.prod_left H₃).norm_left.pow (c.length - 1)).mul H₄.norm_norm