-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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
⊢ ((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)
have 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))) :
              ℕ),
            sorry⟩) :
      (a : (i : Fin ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨(↑⟨i, him⟩ : ℕ), sorry⟩)) → 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))) :
                ℕ),
              sorry⟩)) ↦
    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]