awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₁ x (c.partSize m)) 1
H₃ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₂ x (c.partSize m)) 1
⊢ ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) l
      (fun (a : α) ↦
        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

Tactic:
have H₄ : ∀ m, (fun a ↦ q₁ a (c.partSize m) - q₂ a (c.partSize m)) =O[l] f := fun m ↦
      hqf _ <| c.partSize_le _
-- 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₂ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₁ x (c.partSize m)) 1
H₃ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₂ x (c.partSize m)) 1
H₄ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) l
      (fun (a : α) ↦
        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 :=
    (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

Tactic:
rw [← Asymptotics.isBigO_pi] at H₂ H₃ H₄

Premises used: Asymptotics.isBigO_pi
-- 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₂ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₁ x (c.partSize m)) 1
H₃ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₂ x (c.partSize m)) 1
H₄ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) l
      (fun (a : α) ↦
        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 :=
    (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
⊢ 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

Tactic:
rw [← Asymptotics.isBigO_pi] at H₂ H₃ H₄

Premises used: Asymptotics.isBigO_pi
-- 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₂ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₁ x (c.partSize m)) 1
H₃ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₂ x (c.partSize m)) 1
H₄ :
  ∀ (m : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F) l
      (fun (a : α) ↦
        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 :=
    (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
⊢ 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

Tactic:
rw [← Asymptotics.isBigO_pi] at H₂ H₃ H₄

Premises used: Asymptotics.isBigO_pi
-- 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
⊢ 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
-- 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
⊢ Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) l
    (fun (a : α) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (p₁ a c.length)
        (p₂ a c.length))
    f

Tactic:
have H₁ : (fun a ↦ p₁ a c.length - p₂ a c.length) =O[l] f := hpf _ c.length_le
-- 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) l
    (fun (a : α) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (p₁ a c.length)
        (p₂ a c.length))
    f
⊢ ∀ (i : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₂ x (c.partSize i)) 1

Tactic:
have H₂ : ∀ i, (q₂ · (c.partSize i)) =O[l] (1 : α → ℝ) := fun i ↦
      (hq₂_bdd _ <| c.partSize_le i).isBigO_one ℝ
-- 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) l
    (fun (a : α) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (p₁ a c.length)
        (p₂ a c.length))
    f
H₂ :
  ∀ (i : Fin c.length),
    Asymptotics.IsBigO (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) (F :=
      ℝ) l (fun (x : α) ↦ q₂ x (c.partSize i)) 1
⊢ Asymptotics.IsBigO (E := ℝ) l
    (fun (x : α) ↦
      ‖HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (p₁ x c.length)
            (p₂ x c.length)‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
            (q₂ x (c.partSize i)))
    f

Tactic:
simpa using H₁.norm_norm.mul <| .finsetProd fun i _ ↦ (H₂ i).norm_left

Premises used: Asymptotics.IsBigO.norm_norm, Asymptotics.IsBigO.mul
-- 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.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
⊢ 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 : ℕ)))

Tactic:
taylorComp_sub_taylorComp_isBigO hp_bdd ?_ hq₁_bdd hq₂_bdd ?_

Premises used: FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO
-- 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.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 :
  Asymptotics.IsBigO (E :=
    (i : Fin n.succ) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑i : ℕ)) ↦ 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 (x : α) (i : Fin n.succ) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (↑i : ℕ)) ↦ F) G) (p₁ x (↑i : ℕ))
        (p₂ x (↑i : ℕ)))
    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 : ℕ)))
⊢ ∀ 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 : ℕ)))

Tactic:
simp only [← Nat.lt_succ_iff, Nat.forall_lt_iff_fin, ← Asymptotics.isBigO_pi]

Premises used: Asymptotics.isBigO_pi, Nat.lt_succ_iff, Nat.forall_lt_iff_fin