awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n_1 n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
⊢ (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length) = b.blocks
have right : 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 : ℕ) sorry)
Tactic: conv_rhs => rw [← ofFn_getElem (xs := b.blocks)]
-- 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
n_1 n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
⊢ 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 : ℕ) ⋯)
have 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 : ℕ) sorry
Tactic: congr 1
-- 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
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 : ℕ) ⋯
have right : ∀ (i : Fin (a.gather b).length),
  (a.sigmaCompositionAux b i).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), sorry⟩ : Fin b.blocks.length) : ℕ) sorry
Tactic: refine (Fin.heq_fun_iff B).2 fun i => ?_
-- 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
n_1 n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
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) : ℕ) ⋯
have right : {
      blocks :=
        getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ) sorry,
      blocks_pos := sorry, blocks_sum := sorry : Composition ((a.gather b).blocksFun i) }.length =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), sorry⟩ : Fin b.blocks.length) : ℕ) sorry
Tactic: rw [sigmaCompositionAux, Composition.length, List.getElem_map_rev List.length,
        List.getElem_of_eq (map_length_splitWrtComposition _ _)]
-- 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
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) : ℕ) ⋯
⊢ (a.sigmaCompositionAux b i).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯
have right₁ : {
        blocks :=
          getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
            sorry,
        blocks_pos := sorry, blocks_sum := sorry : Composition ((a.gather b).blocksFun i) }.blocks.length =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), sorry⟩ : Fin b.blocks.length) : ℕ) sorry
Tactic: rw [sigmaCompositionAux, Composition.length, List.getElem_map_rev List.length,
        List.getElem_of_eq (map_length_splitWrtComposition _ _)]
-- 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
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) : ℕ) ⋯
⊢ (a.sigmaCompositionAux b i).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯
have right₂ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map List.length (a.blocks.splitWrtComposition b))
    (↑i : ℕ) sorry =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), sorry⟩ : Fin b.blocks.length) : ℕ) sorry
Tactic: rw [sigmaCompositionAux, Composition.length, List.getElem_map_rev List.length,
        List.getElem_of_eq (map_length_splitWrtComposition _ _)]
-- 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
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) : ℕ) ⋯
⊢ (a.sigmaCompositionAux b i).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), ⋯⟩ : Fin b.blocks.length) : ℕ) ⋯
have right₃ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) sorry =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑(⟨(↑i : ℕ), sorry⟩ : Fin b.blocks.length) : ℕ) sorry
Tactic: rw [sigmaCompositionAux, Composition.length, List.getElem_map_rev List.length,
        List.getElem_of_eq (map_length_splitWrtComposition _ _)]
-- 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
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
⊢ 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)
have h : ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry, blocks_sum := sorry :
          Composition n }.gather
      ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := sorry, blocks_sum := sorry } :
        Composition
          { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
              blocks_sum := sorry : Composition n }.length)).length =
  c.length
Tactic: congr! 1
-- 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
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
⊢ ({ 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
have h : { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry, blocks_sum := sorry :
        Composition n }.gather
    ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := sorry, blocks_sum := sorry } :
      Composition
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
            blocks_sum := sorry : Composition n }.length) =
  c
Tactic: congr
-- 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
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
⊢ { 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
have h : ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry, blocks_sum := sorry :
          Composition n }.gather
      ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := sorry, blocks_sum := sorry } :
        Composition
          { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
              blocks_sum := sorry : Composition n }.length)).blocks =
  c.blocks
Tactic: ext1
-- 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
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
⊢ ({ 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
have h : List.map sum
    (splitWrtComposition (n :=
      { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
          blocks_sum := sorry : 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 := sorry, blocks_sum := sorry } :
        Composition
          { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
              blocks_sum := sorry : Composition n }.length)) =
  c.blocks
Tactic: dsimp [Composition.gather]
-- 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
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 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
have 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 := sorry, blocks_sum := sorry } :
      Composition
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
            blocks_sum := sorry : Composition n }.length)
Tactic: rwa [splitWrtComposition_flatten]
-- 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
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
⊢ ({ 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 : ℕ), ⋯⟩)
have 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 := sorry,
          blocks_sum := sorry : 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 := sorry, blocks_sum := sorry } :
        Composition
          { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
              blocks_sum := sorry : Composition n }.length))
    (↑i : ℕ) sorry =
  blocks (n := c.blocksFun ⟨(↑i : ℕ), sorry⟩) (d ⟨(↑i : ℕ), sorry⟩)
Tactic: dsimp [Composition.sigmaCompositionAux]