-- 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
h :
  ∀ (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),
    ((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)
⊢ Eq.{u_4 + 1} (α := G)
    ((q (Sigma.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)) :
          (a : (i : Fin ⟨k, blocks_fun⟩.fst) → F) → G)
        fun
          (i :
            Fin
              (Sigma.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) ↦
        (p (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) i) :
            (a : (i : Fin (⟨k, blocks_fun⟩.snd i)) → E) → F)
          fun
            (_j :
              Fin
                (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
                  i)) ↦
          z :
      G)
    ((q.compAlongComposition p
            ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
              fun (n : ℕ) ↦ Composition n)) :
          (a : (i : Fin (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).fst) → E) → G)
        fun
          (_j :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).fst (β :=
                fun (n : ℕ) ↦ Composition n))) ↦
        z :
      G)

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

Premises used: FormalMultilinearSeries.congr, FormalMultilinearSeries.compChangeOfVariables_length, OfNat.ofNat, Eq.symm