-- Mathlib/Analysis/Analytic/Composition.lean
theorem comp_partialSum (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
    (M N : ℕ) (z : E) :
    q.partialSum M (∑ i ∈ Finset.Ico 1 N, p i fun _j => z) =
      ∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z

Proof state:
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
⊢ ∀ (i : ℕ) (him : i < ⟨k, blocks_fun⟩.fst) (hin : i < (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.length),
    ((p (⟨k, blocks_fun⟩.snd ⟨i, him⟩)) fun _j => z) =
      p.applyComposition (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd (fun _j => z) ⟨i, hin⟩

Tactic:
intros

Result:
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
i✝ : ℕ
him✝ : i✝ < ⟨k, blocks_fun⟩.fst
hin✝ : i✝ < (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.length
⊢ ((p (⟨k, blocks_fun⟩.snd ⟨i✝, him✝⟩)) fun _j => z) =
    p.applyComposition (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd (fun _j => z) ⟨i✝, hin✝⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
H :
  (∑ n ∈ Finset.range M, ∑ r ∈ Fintype.piFinset fun i => Finset.Ico 1 N, (q n) fun i => (p (r i)) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z
⊢ q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z

Tactic:
simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using H

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ (∑ x ∈ (Finset.Ico 0 M).sigma fun n => Fintype.piFinset fun i => Finset.Ico 1 N,
      (q x.fst) fun i => (p (x.snd i)) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z

Tactic:
apply compChangeOfVariables_sum 0 M N

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 0 M N),
    ((q e.fst) fun i => (p (e.snd i)) fun _j => z) =
      (q.compAlongComposition p (compChangeOfVariables 0 M N e he).snd) fun _j => z

Proof state:
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
⊢ ((q ⟨k, blocks_fun⟩.fst) fun i => (p (⟨k, blocks_fun⟩.snd i)) fun _j => z) =
    (q.compAlongComposition p (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd) fun _j => z

Tactic:
apply congr _ (compChangeOfVariables_length 0 M N H).symm

Result:
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
⊢ ∀ (i : ℕ) (him : i < ⟨k, blocks_fun⟩.fst) (hin : i < (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.length),
    ((p (⟨k, blocks_fun⟩.snd ⟨i, him⟩)) fun _j => z) =
      p.applyComposition (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd (fun _j => z) ⟨i, hin⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z

Tactic:
suffices H :
  (∑ n ∈ Finset.range M,
      ∑ r ∈ Fintype.piFinset fun i : Fin n => Finset.Ico 1 N,
        q n fun i : Fin n => p (r i) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z by
  simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using H

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ (∑ n ∈ Finset.range M, ∑ r ∈ Fintype.piFinset fun i => Finset.Ico 1 N, (q n) fun i => (p (r i)) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 0 M N),
    ((q e.fst) fun i => (p (e.snd i)) fun _j => z) =
      (q.compAlongComposition p (compChangeOfVariables 0 M N e he).snd) fun _j => z

Tactic:
rintro ⟨k, blocks_fun⟩ H

Result:
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
⊢ ((q ⟨k, blocks_fun⟩.fst) fun i => (p (⟨k, blocks_fun⟩.snd i)) fun _j => z) =
    (q.compAlongComposition p (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd) fun _j => z