-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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.IsLittleO (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.IsLittleO (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
refine_1 :
  ∀ k ≤ n,
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin k) ↦ F) G) (F :=
      ((k : Fin (n + 1)) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ F) G) ×
        ((k : Fin (n + 1)) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ E) F))
      l (fun (a : α) ↦ p₁ a k - p₂ a k) fun (a : α) ↦
      (fun (k : Fin (n + 1)) ↦
        HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ F) G) (p₁ a (↑k : ℕ))
          (p₂ a (↑k : ℕ)),
        fun (k : Fin (n + 1)) ↦
        HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ E) F) (q₁ a (↑k : ℕ))
          (q₂ a (↑k : ℕ)))
⊢ Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) (F :=
    ((k : Fin (n + 1)) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ F) G) ×
      ((k : Fin (n + 1)) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ E) F))
    l (fun (a : α) ↦ (p₁ a).taylorComp (q₁ a) n - (p₂ a).taylorComp (q₂ a) n) fun (a : α) ↦
    (fun (k : Fin (n + 1)) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ F) G) (p₁ a (↑k : ℕ))
        (p₂ a (↑k : ℕ)),
      fun (k : Fin (n + 1)) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ E) F) (q₁ a (↑k : ℕ))
        (q₂ a (↑k : ℕ)))
have refine_2 : ∀ k ≤ n,
  Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F) (F :=
    ((k : Fin (n + 1)) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ F) G) ×
      ((k : Fin (n + 1)) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ E) F))
    l (fun (a : α) ↦ q₁ a k - q₂ a k) fun (a : α) ↦
    (fun (k : Fin (n + 1)) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ F) G) (p₁ a (↑k : ℕ))
        (p₂ a (↑k : ℕ)),
      fun (k : Fin (n + 1)) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑k : ℕ)) ↦ E) F) (q₁ a (↑k : ℕ))
        (q₂ a (↑k : ℕ)))
Tactic: refine taylorComp_sub_taylorComp_isBigO hp_bdd ?_ hq₁_bdd hq₂_bdd ?_