-- 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
rw :
  Eq (α := List (List ℕ))
    (ofFn (n :=
      length (n := n)
        (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
          ((fun (i : (a : Composition n) × Composition a.length) ↦
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                  (i.fst (β := fun (a : Composition n) ↦ Composition a.length).gather
                    (i.snd (β := fun (a : Composition n) ↦ Composition a.length)))
                  (i.fst (β := fun (a : Composition n) ↦ Composition a.length).sigmaCompositionAux
                    (i.snd (β := fun (a : Composition n) ↦ Composition a.length))) :
                (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))))
            ((fun (i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
                (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length)
                    {
                      blocks :=
                        flatten
                          (ofFn (n :=
                            i.fst (β := fun (c : Composition n) ↦
                                (i : Fin c.length) → Composition (c.blocksFun i)).length)
                            fun
                              (j :
                                Fin
                                  i.fst (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                            (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                j).blocks),
                      blocks_pos := ⋯, blocks_sum := ⋯ }
                    {
                      blocks :=
                        ofFn (n :=
                          i.fst (β := fun (c : Composition n) ↦
                              (i : Fin c.length) → Composition (c.blocksFun i)).length)
                          fun
                            (j :
                              Fin
                                i.fst (β := fun (c : Composition n) ↦
                                    (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                          (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                              j).length,
                      blocks_pos := ⋯, blocks_sum := ⋯ :
                      Composition
                        {
                            blocks :=
                              flatten
                                (ofFn (n :=
                                  i.fst (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                  fun
                                    (j :
                                      Fin
                                        i.fst (β := fun (c : Composition n) ↦
                                            (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                  (i.snd (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
                            blocks_pos := ⋯, blocks_sum := ⋯ : Composition n }.length } :
                  (a : Composition n) × Composition a.length))
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) c d)))))
      fun
        (i :
          Fin
            (length (n := n)
              (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                ((fun (i : (a : Composition n) × Composition a.length) ↦
                    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                        (i.fst (β := fun (a : Composition n) ↦ Composition a.length).gather
                          (i.snd (β := fun (a : Composition n) ↦ Composition a.length)))
                        (i.fst (β := fun (a : Composition n) ↦ Composition a.length).sigmaCompositionAux
                          (i.snd (β := fun (a : Composition n) ↦ Composition a.length))) :
                      (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))))
                  ((fun (i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
                      (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length)
                          {
                            blocks :=
                              flatten
                                (ofFn (n :=
                                  i.fst (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                  fun
                                    (j :
                                      Fin
                                        i.fst (β := fun (c : Composition n) ↦
                                            (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                  (i.snd (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
                            blocks_pos := ⋯, blocks_sum := ⋯ }
                          {
                            blocks :=
                              ofFn (n :=
                                i.fst (β := fun (c : Composition n) ↦
                                    (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                fun
                                  (j :
                                    Fin
                                      i.fst (β := fun (c : Composition n) ↦
                                          (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                    j).length,
                            blocks_pos := ⋯, blocks_sum := ⋯ :
                            Composition
                              {
                                  blocks :=
                                    flatten
                                      (ofFn (n :=
                                        i.fst (β := fun (c : Composition n) ↦
                                            (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                        fun
                                          (j :
                                            Fin
                                              i.fst (β := fun (c : Composition n) ↦
                                                  (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                        (i.snd (β := fun (c : Composition n) ↦
                                            (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
                                  blocks_pos := ⋯, blocks_sum := ⋯ : Composition n }.length } :
                        (a : Composition n) × Composition a.length))
                    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) c
                      d)))))) ↦
      blocks (n :=
        blocksFun
          (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
            ((fun (i : (a : Composition n) × Composition a.length) ↦
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                    (i.fst (β := fun (a : Composition n) ↦ Composition a.length).gather
                      (i.snd (β := fun (a : Composition n) ↦ Composition a.length)))
                    (i.fst (β := fun (a : Composition n) ↦ Composition a.length).sigmaCompositionAux
                      (i.snd (β := fun (a : Composition n) ↦ Composition a.length))) :
                  (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))))
              ((fun (i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
                  (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length)
                      {
                        blocks :=
                          flatten
                            (ofFn (n :=
                              i.fst (β := fun (c : Composition n) ↦
                                  (i : Fin c.length) → Composition (c.blocksFun i)).length)
                              fun
                                (j :
                                  Fin
                                    i.fst (β := fun (c : Composition n) ↦
                                        (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                              (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                  j).blocks),
                        blocks_pos := ⋯, blocks_sum := ⋯ }
                      {
                        blocks :=
                          ofFn (n :=
                            i.fst (β := fun (c : Composition n) ↦
                                (i : Fin c.length) → Composition (c.blocksFun i)).length)
                            fun
                              (j :
                                Fin
                                  i.fst (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                            (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                j).length,
                        blocks_pos := ⋯, blocks_sum := ⋯ :
                        Composition
                          {
                              blocks :=
                                flatten
                                  (ofFn (n :=
                                    i.fst (β := fun (c : Composition n) ↦
                                        (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                    fun
                                      (j :
                                        Fin
                                          i.fst (β := fun (c : Composition n) ↦
                                              (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                    (i.snd (β := fun (c : Composition n) ↦
                                        (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
                              blocks_pos := ⋯, blocks_sum := ⋯ : Composition n }.length } :
                    (a : Composition n) × Composition a.length))
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) c d))))
          i)
        (Sigma.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
            ((fun (i : (a : Composition n) × Composition a.length) ↦
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                    (i.fst (β := fun (a : Composition n) ↦ Composition a.length).gather
                      (i.snd (β := fun (a : Composition n) ↦ Composition a.length)))
                    (i.fst (β := fun (a : Composition n) ↦ Composition a.length).sigmaCompositionAux
                      (i.snd (β := fun (a : Composition n) ↦ Composition a.length))) :
                  (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))))
              ((fun (i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
                  (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length)
                      {
                        blocks :=
                          flatten
                            (ofFn (n :=
                              i.fst (β := fun (c : Composition n) ↦
                                  (i : Fin c.length) → Composition (c.blocksFun i)).length)
                              fun
                                (j :
                                  Fin
                                    i.fst (β := fun (c : Composition n) ↦
                                        (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                              (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                  j).blocks),
                        blocks_pos := ⋯, blocks_sum := ⋯ }
                      {
                        blocks :=
                          ofFn (n :=
                            i.fst (β := fun (c : Composition n) ↦
                                (i : Fin c.length) → Composition (c.blocksFun i)).length)
                            fun
                              (j :
                                Fin
                                  i.fst (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                            (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                j).length,
                        blocks_pos := ⋯, blocks_sum := ⋯ :
                        Composition
                          {
                              blocks :=
                                flatten
                                  (ofFn (n :=
                                    i.fst (β := fun (c : Composition n) ↦
                                        (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                    fun
                                      (j :
                                        Fin
                                          i.fst (β := fun (c : Composition n) ↦
                                              (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                    (i.snd (β := fun (c : Composition n) ↦
                                        (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
                              blocks_pos := ⋯, blocks_sum := ⋯ : Composition n }.length } :
                    (a : Composition n) × Composition a.length))
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) c d)))
            i :
          Composition
            (blocksFun
              (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                ((fun (i : (a : Composition n) × Composition a.length) ↦
                    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                        (i.fst (β := fun (a : Composition n) ↦ Composition a.length).gather
                          (i.snd (β := fun (a : Composition n) ↦ Composition a.length)))
                        (i.fst (β := fun (a : Composition n) ↦ Composition a.length).sigmaCompositionAux
                          (i.snd (β := fun (a : Composition n) ↦ Composition a.length))) :
                      (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))))
                  ((fun (i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
                      (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length)
                          {
                            blocks :=
                              flatten
                                (ofFn (n :=
                                  i.fst (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                  fun
                                    (j :
                                      Fin
                                        i.fst (β := fun (c : Composition n) ↦
                                            (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                  (i.snd (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
                            blocks_pos := ⋯, blocks_sum := ⋯ }
                          {
                            blocks :=
                              ofFn (n :=
                                i.fst (β := fun (c : Composition n) ↦
                                    (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                fun
                                  (j :
                                    Fin
                                      i.fst (β := fun (c : Composition n) ↦
                                          (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                    j).length,
                            blocks_pos := ⋯, blocks_sum := ⋯ :
                            Composition
                              {
                                  blocks :=
                                    flatten
                                      (ofFn (n :=
                                        i.fst (β := fun (c : Composition n) ↦
                                            (i : Fin c.length) → Composition (c.blocksFun i)).length)
                                        fun
                                          (j :
                                            Fin
                                              i.fst (β := fun (c : Composition n) ↦
                                                  (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                                        (i.snd (β := fun (c : Composition n) ↦
                                            (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
                                  blocks_pos := ⋯, blocks_sum := ⋯ : Composition n }.length } :
                        (a : Composition n) × Composition a.length))
                    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) c d))))
              i)))
    (ofFn (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)) c d)).length)
      fun
        (i :
          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)) c
                  d)).length) ↦
      blocks (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)) c
                d)).blocksFun
          i)
        (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)) c d) i))
⊢ Eq (α := (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
    ((fun (i : (a : Composition n) × Composition a.length) ↦
        (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
            (i.fst (β := fun (a : Composition n) ↦ Composition a.length).gather
              (i.snd (β := fun (a : Composition n) ↦ Composition a.length)))
            (i.fst (β := fun (a : Composition n) ↦ Composition a.length).sigmaCompositionAux
              (i.snd (β := fun (a : Composition n) ↦ Composition a.length))) :
          (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))))
      ((fun (i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length)
              {
                blocks :=
                  flatten
                    (ofFn (n :=
                      i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
                      fun
                        (j :
                          Fin
                            i.fst (β := fun (c : Composition n) ↦
                                (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                      (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                          j).blocks),
                blocks_pos := ⋯, blocks_sum := ⋯ }
              {
                blocks :=
                  ofFn (n :=
                    i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
                    fun
                      (j :
                        Fin
                          i.fst (β := fun (c : Composition n) ↦
                              (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                    (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length,
                blocks_pos := ⋯, blocks_sum := ⋯ :
                Composition
                  {
                      blocks :=
                        flatten
                          (ofFn (n :=
                            i.fst (β := fun (c : Composition n) ↦
                                (i : Fin c.length) → Composition (c.blocksFun i)).length)
                            fun
                              (j :
                                Fin
                                  i.fst (β := fun (c : Composition n) ↦
                                      (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
                            (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                                j).blocks),
                      blocks_pos := ⋯, blocks_sum := ⋯ : Composition n }.length } :
            (a : Composition n) × Composition a.length))
        (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) c d)))
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) c d)

Tactic:
rw [sigma_pi_composition_eq_iff]

Premises used: Composition.sigma_pi_composition_eq_iff