-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
theorem norm_compAlongOrderedFinpartition_le (f : F [×c.length]→L[𝕜] G)
    (p : ∀ i, E [×c.partSize i]→L[𝕜] F) :
    ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i, ‖p i‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap 𝕜 (fun i => F) G
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
v : Fin n → E
⊢ ‖f (c.applyOrderedFinpartition p v)‖ ≤ ‖f‖ * ∏ x : Fin c.length, ‖p x‖ * ∏ r : Fin (c.partSize x), ‖v (c.emb x r)‖

Tactic:
exact f.le_opNorm_mul_prod_of_le <| c.norm_applyOrderedFinpartition_le _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap 𝕜 (fun i => F) G
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
v : Fin n → E
⊢ ‖(c.compAlongOrderedFinpartition f p) v‖ ≤ (‖f‖ * ∏ i : Fin c.length, ‖p i‖) * ∏ i : Fin n, ‖v i‖

Tactic:
rw [compAlongOrderFinpartition_apply, mul_assoc, ← c.prod_sigma_eq_prod,
  ← Finset.prod_mul_distrib]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap 𝕜 (fun i => F) G
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
v : Fin n → E
⊢ ‖f (c.applyOrderedFinpartition p v)‖ ≤ ‖f‖ * ∏ x : Fin c.length, ‖p x‖ * ∏ r : Fin (c.partSize x), ‖v (c.emb x r)‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap 𝕜 (fun i => F) G
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
⊢ ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖

Tactic:
refine ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun v ↦ ?_

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap 𝕜 (fun i => F) G
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
v : Fin n → E
⊢ ‖(c.compAlongOrderedFinpartition f p) v‖ ≤ (‖f‖ * ∏ i : Fin c.length, ‖p i‖) * ∏ i : Fin n, ‖v i‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap 𝕜 (fun i => F) G
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
⊢ 0 ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖

Tactic:
positivity

Result:
no goals