-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : (i : Fin n) → E
f : (a : Composition n) × Composition a.length → H :=
  fun (c : (a : Composition n) × Composition a.length) ↦
    (r c.snd (β := fun (a : Composition n) ↦ Composition a.length).length : (a : (i : Fin c.snd.length) → G) → H)
      (q.applyComposition (c.snd (β := fun (a : Composition n) ↦ Composition a.length))
        (p.applyComposition (c.fst (β := fun (a : Composition n) ↦ Composition a.length)) v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun (c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
    (r c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length :
        (a : (i : Fin c.fst.length) → G) → H)
      fun (i : Fin c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (q (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).length :
          (a : (i : Fin (c.snd i).length) → F) → G)
        (p.applyComposition (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i)
          (v ∘
            (⇑(c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).embedding i) :
              (a : Fin (c.fst.blocksFun i)) → Fin n)))
a : Composition n
b : Composition a.length
h :
  Membership.mem (γ := Finset ((a : Composition n) × Composition a.length)) Finset.univ
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
i : ℕ
hi1 : i < b.length
hi2 : i < (a.gather b).length
j : ℕ
hj1 : j < b.blocksFun ⟨i, hi1⟩
hj2 :
  j <
    Composition.length (n := (a.gather b).blocksFun ⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), ⋯⟩)
      (a.sigmaCompositionAux b ⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), ⋯⟩)
⊢ (p.applyComposition
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))
          v ∘
        (⇑(embedding
              (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
                (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))
              (⟨i, hi1⟩ : Fin b.length)) :
          (a_1 : Fin (⟨a, b⟩.snd.blocksFun ⟨i, hi1⟩)) → Fin ⟨a, b⟩.fst.length))
      (⟨j, hj1⟩ : Fin (b.blocksFun (⟨i, hi1⟩ : Fin b.length))) =
    p.applyComposition
      (Sigma.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
        (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) (a.gather b)
          (a.sigmaCompositionAux b))
        ⟨i, hi2⟩)
      (v ∘
        (⇑((Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                  (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                    (a.gather b) (a.sigmaCompositionAux b))).embedding
              ⟨i, hi2⟩) :
          (a : Fin (⟨a.gather b, a.sigmaCompositionAux b⟩.fst.blocksFun ⟨i, hi2⟩)) → Fin n))
      (⟨j, hj2⟩ :
        Fin
          (Composition.length (n :=
            (a.gather b).blocksFun (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), ⋯⟩ : Fin (a.gather b).length))
            (a.sigmaCompositionAux b (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), ⋯⟩ : Fin (a.gather b).length))))
have h : ∀ (i_1 : ℕ)
  (him : i_1 < a.blocksFun ((b.embedding ⟨i, hi1⟩ : (a_1 : Fin (b.blocksFun ⟨i, hi1⟩)) → Fin a.length) ⟨j, hj1⟩))
  (hin :
    i_1 <
      blocksFun (n := (a.gather b).blocksFun ⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩)
        (a.sigmaCompositionAux b ⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩)
        ⟨(↑(⟨j, hj1⟩ : Fin (b.blocksFun (⟨i, hi1⟩ : Fin b.length))) : ℕ), sorry⟩),
  (v ∘
        (⇑((Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
                  (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).embedding
              ((embedding
                    (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
                      (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))
                    (⟨i, hi1⟩ : Fin b.length) :
                  (a_1 : Fin (⟨a, b⟩.snd.blocksFun ⟨i, hi1⟩)) → Fin ⟨a, b⟩.fst.length)
                (⟨j, hj1⟩ : Fin (b.blocksFun (⟨i, hi1⟩ : Fin b.length))))) :
          (a :
              Fin
                (⟨a, b⟩.fst.blocksFun
                  ((⟨a, b⟩.snd.embedding ⟨i, hi1⟩ : (a_1 : Fin (⟨a, b⟩.snd.blocksFun ⟨i, hi1⟩)) → Fin ⟨a, b⟩.fst.length)
                    ⟨j, hj1⟩))) →
            Fin n))
      (⟨i_1, him⟩ :
        Fin
          (a.blocksFun
            ((b.embedding (⟨i, hi1⟩ : Fin b.length) : (a_1 : Fin (b.blocksFun ⟨i, hi1⟩)) → Fin a.length)
              (⟨j, hj1⟩ : Fin (b.blocksFun (⟨i, hi1⟩ : Fin b.length)))))) =
    Function.comp (β :=
      Fin
        ((Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) (a.gather b)
                (a.sigmaCompositionAux b))).blocksFun
          ⟨i, hi2⟩))
      (v ∘
        (⇑((Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                  (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                    (a.gather b) (a.sigmaCompositionAux b))).embedding
              ⟨i, hi2⟩) :
          (a : Fin (⟨a.gather b, a.sigmaCompositionAux b⟩.fst.blocksFun ⟨i, hi2⟩)) → Fin n))
      (⇑(embedding
            (Sigma.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) (a.gather b)
                (a.sigmaCompositionAux b))
              (⟨i, hi2⟩ : Fin (a.gather b).length))
            (⟨j, hj2⟩ :
              Fin
                (Composition.length (n :=
                  (a.gather b).blocksFun (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩ : Fin (a.gather b).length))
                  (a.sigmaCompositionAux b (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩ : Fin (a.gather b).length))))) :
        (a_1 : Fin ((⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hi2⟩).blocksFun ⟨j, hj2⟩)) →
          Fin (⟨a.gather b, a.sigmaCompositionAux b⟩.fst.blocksFun ⟨i, hi2⟩))
      (⟨i_1, hin⟩ :
        Fin
          (blocksFun (n := (a.gather b).blocksFun (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩ : Fin (a.gather b).length))
            (a.sigmaCompositionAux b (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩ : Fin (a.gather b).length))
            (⟨(↑(⟨j, hj1⟩ : Fin (b.blocksFun (⟨i, hi1⟩ : Fin b.length))) : ℕ), sorry⟩ :
              Fin
                (Composition.length (n :=
                  (a.gather b).blocksFun (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩ : Fin (a.gather b).length))
                  (a.sigmaCompositionAux b (⟨(↑(⟨i, hi1⟩ : Fin b.length) : ℕ), sorry⟩ : Fin (a.gather b).length))))))
Tactic: apply p.congr (blocksFun_sigmaCompositionAux a b _ _).symm