awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
right :
  HEq (α := Fin (a.gather b).length → ℕ) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length (β :=
    Fin b.blocks.length → ℕ) fun (i : Fin b.blocks.length) ↦
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯
⊢ Eq (α := List ℕ)
    (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length)
    (ofFn (n := b.blocks.length) fun (i : Fin b.blocks.length) ↦
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯)

Tactic:
congr 1
-- 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 : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
⊢ HEq (α := Fin (a.gather b).length → ℕ) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length (β :=
    Fin b.blocks.length → ℕ) fun (i : Fin b.blocks.length) ↦
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯

Tactic:
(Fin.heq_fun_iff B).2 fun i => ?_

Premises used: Iff.mpr, Fin.heq_fun_iff
-- 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 : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
right :
  ∀ (i : Fin (a.gather b).length),
    (a.sigmaCompositionAux b i).length =
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ)
        ⋯
⊢ HEq (α := Fin (a.gather b).length → ℕ) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length (β :=
    Fin b.blocks.length → ℕ) fun (i : Fin b.blocks.length) ↦
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯

Tactic:
refine (Fin.heq_fun_iff B).2 fun i => ?_

Premises used: Iff.mpr, Fin.heq_fun_iff
-- 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 : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
i : Fin (a.gather b).length
right :
  {
        blocks :=
          getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
            ⋯,
        blocks_pos := ⋯, blocks_sum := ⋯ : Composition ((a.gather b).blocksFun i) }.length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯
right₁ :
  {
          blocks :=
            getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b)
              (↑i : ℕ) ⋯,
          blocks_pos := ⋯, blocks_sum := ⋯ : Composition ((a.gather b).blocksFun i) }.blocks.length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯
right₂ :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map List.length (a.blocks.splitWrtComposition b))
      (↑i : ℕ) ⋯ =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯
right₃ right₄ :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯ =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯
⊢ (a.sigmaCompositionAux b i).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯

Tactic:
rw [sigmaCompositionAux, Composition.length, List.getElem_map_rev List.length,
        List.getElem_of_eq (map_length_splitWrtComposition _ _)]

Premises used: Composition.length, List.getElem_map_rev, List.getElem_of_eq, List.map_length_splitWrtComposition, Composition.sigmaCompositionAux, List.length
-- 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)
⊢ List.map sum (ofFn (n := c.length) fun (i : Fin c.length) ↦ (d i).blocks) = c.blocks

Tactic:
simp [map_ofFn, Function.comp_def, Composition.blocks_sum, Composition.ofFn_blocksFun]

Premises used: Composition.ofFn_blocksFun, List.map_ofFn, Composition.blocks_sum, Function.comp_def
-- 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)
⊢ List.map sum (ofFn (n := c.length) fun (i : Fin c.length) ↦ (d i).blocks) = c.blocks

Tactic:
have : map List.sum (ofFn fun i : Fin (Composition.length c) => (d i).blocks) = c.blocks := by
      simp [map_ofFn, Function.comp_def, Composition.blocks_sum, Composition.ofFn_blocksFun]
-- 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) =
    c
⊢ ({ 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

Tactic:
congr
-- 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)).blocks =
    c.blocks
⊢ { 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) =
    c

Tactic:
ext1
-- 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 :
  List.map sum
      (splitWrtComposition (n :=
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.length)
        (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks))
        ({ 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)) =
    c.blocks
⊢ ({ 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)).blocks =
    c.blocks

Tactic:
dsimp [Composition.gather]

Premises used: Composition.gather
-- 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 :
  List.map (α := List ℕ) List.length (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) =
    blocks (n := List.length (α := ℕ) (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks)))
      ({ 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)
⊢ List.map sum
      (splitWrtComposition (n :=
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.length)
        (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks))
        ({ 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)) =
    c.blocks

Tactic:
rwa [splitWrtComposition_flatten]

Premises used: List.splitWrtComposition_flatten
-- 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
⊢ List.map (α := List ℕ) List.length (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) =
    blocks (n := List.length (α := ℕ) (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks)))
      ({ 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)

Tactic:
simp only [map_ofFn, Function.comp_def]

Premises used: List.map_ofFn, Function.comp_def
-- 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
e_2 :
  ({ 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
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
h :
  getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
      (splitWrtComposition (n :=
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.length)
        (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks))
        ({ 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 (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)
⊢ ({ 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 =
    blocks (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)

Tactic:
dsimp [Composition.sigmaCompositionAux]

Premises used: Composition.sigmaCompositionAux
-- 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
e_2 :
  ({ 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
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
h :
  getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
      (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) (↑i : ℕ) ⋯ =
    blocks (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)
rw :
  List.map (α := List ℕ) List.length (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) =
    blocks (n := List.length (α := ℕ) (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks)))
      ({ 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)
⊢ getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
      (splitWrtComposition (n :=
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.length)
        (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks))
        ({ 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 (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)

Tactic:
rw [getElem_of_eq (splitWrtComposition_flatten _ _ _)]

Premises used: List.splitWrtComposition_flatten, List.getElem_of_eq
-- 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
e_2 :
  ({ 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
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
⊢ getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
      (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) (↑i : ℕ) ⋯ =
    blocks (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)

Tactic:
simp only [List.getElem_ofFn]

Premises used: List.getElem_ofFn
-- 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
e_2 :
  ({ 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
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
⊢ List.map (α := List ℕ) List.length (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) =
    blocks (n := List.length (α := ℕ) (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks)))
      ({ 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)

Tactic:
simp only [map_ofFn, Function.comp_def]

Premises used: List.map_ofFn, Function.comp_def