-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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 ⋯)
⊢ (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
          ⋯)
have succ₁ : (a.gather b).sizeUpTo i +
    (sizeUpTo (n := (a.gather b).blocksFun (⟨i, sorry⟩ : Fin (a.gather b).length))
        {
          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, sorry⟩ : 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, sorry⟩ : Fin (a.gather b).length))
        {
          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, sorry⟩ : 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) sorry)
Tactic: rw [getElem_of_eq (getElem_splitWrtComposition _ _ _ _), getElem_drop, getElem_take]