-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource 0 M N
i : ℕ
him : i < Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
hin :
  i <
    (compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length
h :
  ((p
          ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                fun (n : ℕ) ↦ Composition n).blocksFun
            ⟨(↑(⟨i, him⟩ :
                    Fin
                      (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)
                        (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) :
                ℕ),
              ⋯⟩) :
        (a : (i : Fin ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨(↑⟨i, him⟩ : ℕ), ⋯⟩)) → E) → F)
      fun
        (_j :
          Fin
            ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              ⟨(↑(⟨i, him⟩ :
                      Fin
                        (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)
                          (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) :
                  ℕ),
                ⋯⟩)) ↦
      z) =
    p.applyComposition
      ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n))
      (fun
          (_j :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).fst (β :=
                fun (n : ℕ) ↦ Composition n))) ↦
        z)
      (⟨i, hin⟩ :
        Fin
          (compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
              Composition n).length)
h₁ :
  Eq.{u_3 + 1} (α := F)
    ((p
            ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              ⟨(↑(⟨i, him⟩ :
                      Fin
                        (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)
                          (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) :
                  ℕ),
                ⋯⟩) :
          (a : (i : Fin ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨(↑⟨i, him⟩ : ℕ), ⋯⟩)) → E) → F)
        fun
          (_j :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                    fun (n : ℕ) ↦ Composition n).blocksFun
                ⟨(↑(⟨i, him⟩ :
                        Fin
                          (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)
                            (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) :
                    ℕ),
                  ⋯⟩)) ↦
        z :
      F)
    ((p
            ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              ⟨i, hin⟩) :
          (a : (i : Fin ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨i, hin⟩)) → E) → F)
        ((fun
              (_j :
                Fin
                  ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).fst (β :=
                    fun (n : ℕ) ↦ Composition n))) ↦
            z) ∘
          (⇑((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                    fun (n : ℕ) ↦ Composition n).embedding
                ⟨i, hin⟩) :
            (a : Fin ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨i, hin⟩)) →
              Fin (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).fst)) :
      F)
h₂ h₃ :
  Eq.{u_3 + 1} (α := F)
    ((p
            ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              ⟨(↑(⟨i, him⟩ :
                      Fin
                        (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)
                          (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) :
                  ℕ),
                ⋯⟩) :
          (a : (i : Fin ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨(↑⟨i, him⟩ : ℕ), ⋯⟩)) → E) → F)
        fun
          (_j :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                    fun (n : ℕ) ↦ Composition n).blocksFun
                ⟨(↑(⟨i, him⟩ :
                        Fin
                          (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)
                            (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) :
                    ℕ),
                  ⋯⟩)) ↦
        z :
      F)
    ((p
            ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              ⟨i, hin⟩) :
          (a : (i : Fin ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨i, hin⟩)) → E) → F)
        fun
          (x :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
                    fun (n : ℕ) ↦ Composition n).blocksFun
                ⟨i, hin⟩)) ↦
        z :
      F)
⊢ ((p (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) ⟨i, him⟩) :
        (a : (i : Fin (⟨k, blocks_fun⟩.snd ⟨i, him⟩)) → E) → F)
      fun
        (_j :
          Fin
            (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
              ⟨i, him⟩)) ↦
      z) =
    p.applyComposition
      ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n))
      (fun
          (_j :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).fst (β :=
                fun (n : ℕ) ↦ Composition n))) ↦
        z)
      (⟨i, hin⟩ :
        Fin
          (compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
              Composition n).length)

Tactic:
rw [← compChangeOfVariables_blocksFun 0 M N H, applyComposition, Function.comp_def]

Premises used: FormalMultilinearSeries.compChangeOfVariables_blocksFun, FormalMultilinearSeries.applyComposition, Function.comp_def, OfNat.ofNat