awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ :
  ∀ (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
⊢ 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₃ : ∀ (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
Tactic: have H₃ : ∀ m, (q₂ · (c.partSize m)) =O[l] (1 : α → ℝ) := fun m ↦
      (hq₂_bdd _ <| c.partSize_le _).isBigO_one ℝ
-- 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₂ :
  ∀ (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
⊢ 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₄ : ∀ (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 _
-- 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
⊢ 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
have 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
Tactic: have H₁ : (fun a ↦ p₁ a c.length - p₂ a c.length) =O[l] f := hpf _ c.length_le
-- 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) 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
⊢ 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
have 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
Tactic: have H₂ : ∀ i, (q₂ · (c.partSize i)) =O[l] (1 : α → ℝ) := fun i ↦
      (hq₂_bdd _ <| c.partSize_le i).isBigO_one ℝ
-- 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
⊢ 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_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 : ℕ)))
Tactic: refine taylorComp_sub_taylorComp_isBigO hp_bdd ?_ hq₁_bdd hq₂_bdd ?_
-- 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
⊢ ∀ 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 : ℕ)))
have 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 : ℕ)))
Tactic: simp only [← Nat.lt_succ_iff, Nat.forall_lt_iff_fin, ← Asymptotics.isBigO_pi]
-- 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
⊢ ∀ 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 : ℕ)))
have refine_2 : Asymptotics.IsBigO (E :=
  (i : Fin n.succ) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑i : ℕ)) ↦ 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 (x : α) (i : Fin n.succ) ↦
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (↑i : ℕ)) ↦ E) F) (q₁ x (↑i : ℕ))
      (q₂ 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 : ℕ)))
Tactic: simp only [← Nat.lt_succ_iff, Nat.forall_lt_iff_fin, ← Asymptotics.isBigO_pi]
-- 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq :
  ∀ (n : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ F) G) (fun (x : F) ↦ q x n) t
hp :
  ∀ (n : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (x : E) ↦ p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
    (fun (x : E) ↦ (q (f x)).taylorComp (p x) n) s
have apply : ∀ (c : OrderedFinpartition n),
  Membership.mem (γ := Finset (OrderedFinpartition n)) Finset.univ c →
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
      (fun (a : E) ↦ (q (f a)).compAlongOrderedFinpartition (p a) c) s
Tactic: apply Finset.analyticOn_fun_sum _ (fun c _ ↦ ?_)
-- 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq :
  ∀ (n : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ F) G) (fun (x : F) ↦ q x n) t
hp :
  ∀ (n : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (x : E) ↦ p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
h_1 : Membership.mem (γ := Finset (OrderedFinpartition n)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
    (fun (a : E) ↦ (q (f a)).compAlongOrderedFinpartition (p a) c) s
have change : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
  ((fun
        (p :
          ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G ×
            ((m : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F)) ↦
      (((B :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G) →
                  ContinuousMultilinearMap 𝕜
                    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                    (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) G))
              p.1 :
            ContinuousMultilinearMap 𝕜
              (fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
              (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)) :
          (a : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) G)
        p.2) ∘
    fun (x : E) ↦ (q (f x) c.length, fun (m : Fin c.length) ↦ p x (c.partSize m)))
  s
Tactic: change AnalyticOn 𝕜
    ((fun p ↦ B p.1 p.2) ∘ (fun x ↦ (q (f x) c.length, fun m ↦ p x (c.partSize m)))) s