-- Module: Mathlib.Analysis.Analytic.Composition
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_1 :
  Membership.mem (γ := Finset ((a : Composition n) × Composition a.length)) Finset.univ
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
h :
  ∀ (i : ℕ) (him : i < b.length) (hin : i < (a.gather b).length),
    q.applyComposition
        (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))
        (p.applyComposition
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))
          v)
        (⟨i, him⟩ : Fin b.length) =
      (q
            (Composition.length (n :=
              (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, hin⟩)
              (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, hin⟩)) :
          (a : (i : Fin (⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hin⟩).length) → F) → G)
        (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, hin⟩)
          (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, hin⟩) :
              (a : Fin (⟨a.gather b, a.sigmaCompositionAux b⟩.fst.blocksFun ⟨i, hin⟩)) → Fin n)))
⊢ f (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b) =
    g
      (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) (a.gather b)
        (a.sigmaCompositionAux b))

Tactic:
apply r.congr (Composition.length_gather a b).symm

Premises used: FormalMultilinearSeries.congr, Composition.length_gather, Eq.symm