-- 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
n_1 n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn (n := c.length) fun (i : Fin c.length) ↦ (d i).blocks) = c.blocks
h :
  ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯, blocks_sum := ⋯ :
            Composition n }.gather
        ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
          Composition
            { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                blocks_sum := ⋯ : Composition n }.length)).length =
    c.length
h₁ :
  ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯, blocks_sum := ⋯ :
              Composition n }.gather
          ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
            Composition
              { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                  blocks_sum := ⋯ : Composition n }.length)).length =
      c.length →
    HEq (α :=
      Fin
          ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                  blocks_sum := ⋯ : Composition n }.gather
              ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯,
                  blocks_sum := ⋯ } :
                Composition
                  { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                      blocks_sum := ⋯ : Composition n }.length)).length →
        List ℕ)
      fun
        (i :
          Fin
            ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                    blocks_sum := ⋯ : Composition n }.gather
                ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯,
                    blocks_sum := ⋯ } :
                  Composition
                    { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                        blocks_sum := ⋯ : Composition n }.length)).length) ↦
      ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
              blocks_sum := ⋯ : Composition n }.sigmaCompositionAux
          { blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ :
            Composition
              { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                  blocks_sum := ⋯ : Composition n }.length }
          i).blocks
      (β := Fin c.length → List ℕ) fun (i : Fin c.length) ↦ (d i).blocks
⊢ Eq (α := List (List ℕ))
    (ofFn (n :=
      ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
              blocks_sum := ⋯ : Composition n }.gather
          ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
            Composition
              { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                  blocks_sum := ⋯ : Composition n }.length)).length)
      fun
        (i :
          Fin
            ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                    blocks_sum := ⋯ : Composition n }.gather
                ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯,
                    blocks_sum := ⋯ } :
                  Composition
                    { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                        blocks_sum := ⋯ : Composition n }.length)).length) ↦
      ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
              blocks_sum := ⋯ : Composition n }.sigmaCompositionAux
          { blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ :
            Composition
              { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                  blocks_sum := ⋯ : Composition n }.length }
          i).blocks)
    (ofFn (n := c.length) fun (i : Fin c.length) ↦ (d i).blocks)

Tactic:
congr! 1