-- Mathlib/Analysis/Analytic/Composition.lean
theorem comp_assoc (r : FormalMultilinearSeries 𝕜 G H) (q : FormalMultilinearSeries 𝕜 F G)
    (p : FormalMultilinearSeries 𝕜 E F) : (r.comp q).comp p = r.comp (q.comp p)

Proof state:
case h.H.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c => (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c => (r c.fst.length) fun i => (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
a : Composition n
b : Composition a.length
a✝ : ⟨a, b⟩ ∈ Finset.univ
⊢ f ⟨a, b⟩ = g ⟨a.gather b, a.sigmaCompositionAux b⟩

Tactic:
apply r.congr (Composition.length_gather a b).symm

Result:
case h.H.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c => (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c => (r c.fst.length) fun i => (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
a : Composition n
b : Composition a.length
a✝ : ⟨a, b⟩ ∈ Finset.univ
⊢ ∀ (i : ℕ) (him : i < b.length) (hin : i < (a.gather b).length),
    q.applyComposition ⟨a, b⟩.snd (p.applyComposition ⟨a, b⟩.fst v) ⟨i, him⟩ =
      (q (⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hin⟩).length)
        (p.applyComposition (⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hin⟩)
          (v ∘ ⇑(⟨a.gather b, a.sigmaCompositionAux b⟩.fst.embedding ⟨i, hin⟩)))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c => (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c => (r c.fst.length) fun i => (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
this :
  ∑ c : (a : Composition n) × Composition a.length, f c =
    ∑ c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)), g c
⊢ ((r.comp q).comp p n) v = (r.comp (q.comp p) n) v

Tactic:
simpa (config := { unfoldPartialApp := true }) only [FormalMultilinearSeries.comp,
  ContinuousMultilinearMap.sum_apply, compAlongComposition_apply, Finset.sum_sigma',
  applyComposition, ContinuousMultilinearMap.map_sum]

Result:
no goals

Proof state:
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c => (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
⊢ ((r.comp q).comp p n) v = (r.comp (q.comp p) n) v

Tactic:
let g : (Σ c : Composition n, ∀ i : Fin c.length, Composition (c.blocksFun i)) → H := fun c =>
  r c.1.length fun i : Fin c.1.length =>
    q (c.2 i).length (applyComposition p (c.2 i) (v ∘ c.1.embedding i))

Result:
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c => (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c => (r c.fst.length) fun i => (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
⊢ ((r.comp q).comp p n) v = (r.comp (q.comp p) n) v

Proof state:
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c => (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c => (r c.fst.length) fun i => (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
⊢ ((r.comp q).comp p n) v = (r.comp (q.comp p) n) v

Tactic:
suffices ∑ c, f c = ∑ c, g c by
  simpa (config := { unfoldPartialApp := true }) only [FormalMultilinearSeries.comp,
    ContinuousMultilinearMap.sum_apply, compAlongComposition_apply, Finset.sum_sigma',
    applyComposition, ContinuousMultilinearMap.map_sum]

Result:
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c => (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c => (r c.fst.length) fun i => (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
⊢ ∑ c : (a : Composition n) × Composition a.length, f c =
    ∑ c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)), g c