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
s : Set E
t : Set F
q_1 : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
q q' : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
v : (i : Fin n) → E
⊢ Eq.{u_4 + 1} (α := G)
    (((fun
                (p :
                  (i : Fin c.length) →
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
              c.compAlongOrderedFinpartition f p)
            (update (β := fun (i : Fin c.length) ↦
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (q + q')) :
          (a : (i : Fin n) → E) → G)
        v :
      G)
    ((HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
            ((fun
                  (p :
                    (i : Fin c.length) →
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                c.compAlongOrderedFinpartition f p)
              (update (β := fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q))
            ((fun
                  (p :
                    (i : Fin c.length) →
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                c.compAlongOrderedFinpartition f p)
              (update (β := fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q')) :
          (a : (i : Fin n) → E) → G)
        v :
      G)

Tactic:
simp [applyOrderedFinpartition_update_left]

Premises used: OrderedFinpartition.applyOrderedFinpartition_update_left
-- 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
s : Set E
t : Set F
q_1 : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
a : 𝕜
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
H :
  ∀ (v : (i : Fin n) → E),
    Eq.{u_4 + 1} (α := G)
      (((fun
                  (p :
                    (i : Fin c.length) →
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                c.compAlongOrderedFinpartition f p)
              (update (β := fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (a • q)) :
            (a : (i : Fin n) → E) → G)
          v :
        G)
      ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) a
              ((fun
                    (p :
                      (i : Fin c.length) →
                        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                  c.compAlongOrderedFinpartition f p)
                (update (β := fun (i : Fin c.length) ↦
                  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)) :
            (a : (i : Fin n) → E) → G)
          v :
        G)
⊢ (fun (p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
        c.compAlongOrderedFinpartition f p)
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (a • q)) =
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) a
      ((fun
            (p :
              (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
          c.compAlongOrderedFinpartition f p)
        (update (β := fun (i : Fin c.length) ↦
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q))

Tactic:
ext v
-- 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
s : Set E
t : Set F
q_1 : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
a : 𝕜
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
v : (i : Fin n) → E
⊢ Eq.{u_4 + 1} (α := G)
    (((fun
                (p :
                  (i : Fin c.length) →
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
              c.compAlongOrderedFinpartition f p)
            (update (β := fun (i : Fin c.length) ↦
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (a • q)) :
          (a : (i : Fin n) → E) → G)
        v :
      G)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) a
            ((fun
                  (p :
                    (i : Fin c.length) →
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                c.compAlongOrderedFinpartition f p)
              (update (β := fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)) :
          (a : (i : Fin n) → E) → G)
        v :
      G)

Tactic:
simp [applyOrderedFinpartition_update_left]

Premises used: OrderedFinpartition.applyOrderedFinpartition_update_left
-- 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
refine :
  ∀ (f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
        ((((c.compAlongOrderedFinpartitionₗ :
                    (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G) →
                      MultilinearMap 𝕜
                        (fun (i : Fin c.length) ↦ ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                        (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) G))
                  f :
                MultilinearMap 𝕜
                  (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 :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) ≤
      1 * ‖f‖ * ∏ i : Fin c.length, ‖p i‖
⊢ 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)

Tactic:
refine MultilinearMap.mkContinuousLinear c.compAlongOrderedFinpartitionₗ 1 fun f p ↦ ?_

Premises used: OfNat.ofNat, MultilinearMap.mkContinuousLinear
-- 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
simp : ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
      ((((c.compAlongOrderedFinpartitionₗ :
                  (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G) →
                    MultilinearMap 𝕜
                      (fun (i : Fin c.length) ↦ ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) G))
                f :
              MultilinearMap 𝕜
                (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 :
        ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) ≤
    1 * ‖f‖ * ∏ i : Fin c.length, ‖p i‖

Tactic:
simp only [one_mul, compAlongOrderedFinpartitionₗ_apply_apply]

Premises used: OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply, one_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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
⊢ ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖

Tactic:
apply norm_compAlongOrderedFinpartition_le

Premises used: OrderedFinpartition.norm_compAlongOrderedFinpartition_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
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
⊢ (((compAlongOrderedFinpartitionL 𝕜 E F G c :
              (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))
            f :
          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 =
    c.compAlongOrderedFinpartition f p

Tactic:
rfl

Premises used: OrderedFinpartition.compAlongOrderedFinpartition, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
⊢ LE.le (α := ℕ) sorry 1

Tactic:
MultilinearMap.mkContinuousLinear_norm_le _ zero_le_one _

Premises used: MultilinearMap.mkContinuousLinear_norm_le, zero_le_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
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
⊢ norm (E :=
      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))
      ((compAlongOrderedFinpartitionL 𝕜 E F G c :
            (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))
          f :
        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)) ≤
    ‖f‖

Tactic:
(ContinuousLinearMap.le_of_opNorm_le _ c.norm_compAlongOrderedFinpartitionL_le f).trans_eq
    (one_mul _)

Premises used: Unit.unit, LE.le.trans_eq, sorryAx, Lean.Name.num, ContinuousLinearMap.le_of_opNorm_le, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat, one_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
n : ℕ
c : OrderedFinpartition n
f₁ f₂ : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
g₁ g₂ : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
h₁ :
  ‖c.compAlongOrderedFinpartition f₁ g₁ - c.compAlongOrderedFinpartition f₁ g₂‖ ≤
    ‖f₁‖ * (↑c.length : ℝ) * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖
h₂ :
  ‖c.compAlongOrderedFinpartition f₁ g₂ - c.compAlongOrderedFinpartition f₂ g₂‖ ≤ ‖f₁ - f₂‖ * ∏ i : Fin c.length, ‖g₂ i‖
⊢ ‖c.compAlongOrderedFinpartition f₁ g₁ - c.compAlongOrderedFinpartition f₁ g₂‖ +
      ‖c.compAlongOrderedFinpartition f₁ g₂ - c.compAlongOrderedFinpartition f₂ g₂‖ ≤
    ‖f₁‖ * (↑c.length : ℝ) * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖ + ‖f₁ - f₂‖ * ∏ i : Fin c.length, ‖g₂ i‖

Tactic:
gcongr ?_ + ?_
-- 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
n : ℕ
c : OrderedFinpartition n
f₁ f₂ : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
g₁ g₂ : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
⊢ ‖c.compAlongOrderedFinpartition f₁ g₁ - c.compAlongOrderedFinpartition f₁ g₂‖ ≤
    ‖f₁‖ * (↑c.length : ℝ) * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖

Tactic:
((c.compAlongOrderedFinpartitionL 𝕜 E F G f₁).norm_image_sub_le g₁ g₂).trans ?_

Premises used: ContinuousMultilinearMap.norm_image_sub_le, OrderedFinpartition.compAlongOrderedFinpartitionL, LE.le.trans, DFunLike.coe
-- 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
n : ℕ
c : OrderedFinpartition n
f₁ f₂ : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
g₁ g₂ : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
h₁ :
  norm (E :=
            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))
            ((compAlongOrderedFinpartitionL 𝕜 E F G c :
                  (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))
                f₁ :
              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)) *
          (↑(Fintype.card (Fin c.length)) : ℝ) *
        max ‖g₁‖ ‖g₂‖ ^ (Fintype.card (Fin c.length) - 1) *
      ‖g₁ - g₂‖ ≤
    ‖f₁‖ * (↑c.length : ℝ) * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖
⊢ ‖c.compAlongOrderedFinpartition f₁ g₁ - c.compAlongOrderedFinpartition f₁ g₂‖ ≤
    ‖f₁‖ * (↑c.length : ℝ) * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖

Tactic:
refine ((c.compAlongOrderedFinpartitionL 𝕜 E F G f₁).norm_image_sub_le g₁ g₂).trans ?_

Premises used: ContinuousMultilinearMap.norm_image_sub_le, OrderedFinpartition.compAlongOrderedFinpartitionL, LE.le.trans, DFunLike.coe
-- 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
n : ℕ
c : OrderedFinpartition n
f₁ f₂ : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
g₁ g₂ : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
h₁ :
  norm (E :=
            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))
            ((compAlongOrderedFinpartitionL 𝕜 E F G c :
                  (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))
                f₁ :
              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)) *
          (↑c.length : ℝ) *
        max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) *
      ‖g₁ - g₂‖ ≤
    ‖f₁‖ * (↑c.length : ℝ) * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖
⊢ norm (E :=
            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))
            ((compAlongOrderedFinpartitionL 𝕜 E F G c :
                  (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))
                f₁ :
              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)) *
          (↑(Fintype.card (Fin c.length)) : ℝ) *
        max ‖g₁‖ ‖g₂‖ ^ (Fintype.card (Fin c.length) - 1) *
      ‖g₁ - g₂‖ ≤
    ‖f₁‖ * (↑c.length : ℝ) * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖

Tactic:
simp only [Fintype.card_fin]

Premises used: Fintype.card_fin