-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  ∀ (hj : j < b.blocksFun ⟨i, hi⟩),
    a.sizeUpTo (b.sizeUpTo i + j) =
      (a.gather b).sizeUpTo i +
        sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)) j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < length (n := (a.gather b).blocksFun ⟨i, ⋯⟩) (a.sigmaCompositionAux b ⟨i, ⋯⟩)
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
succ :
  (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks (b.sizeUpTo i + j) D) =
    (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length)
          (drop (b.sizeUpTo i) (take (b.sizeUpTo (i + 1)) a.blocks)) j ⋯)
succ₁ :
  (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks (b.sizeUpTo i + j) D) =
    (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (take (b.sizeUpTo (i + 1)) a.blocks)
          (b.sizeUpTo i + j) ⋯)
succ₂ succ₃ :
  (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks (b.sizeUpTo i + j) D) =
    (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks (b.sizeUpTo i + j) ⋯)
⊢ (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks (b.sizeUpTo i + j) D) =
    (a.gather b).sizeUpTo i +
      (sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
          {
            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, ⋯⟩ : Fin (a.gather b).length)) }
          j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length)
          (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) i ⋯) j
          ⋯)

Tactic:
rw [getElem_of_eq (getElem_splitWrtComposition _ _ _ _), getElem_drop, getElem_take]

Premises used: List.getElem_of_eq, List.getElem_take, List.getElem_drop, List.getElem_splitWrtComposition