awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
⊢ i < (List.map sum (a.blocks.splitWrtComposition b)).length

Tactic:
have B : i < List.length (map List.sum (splitWrtComposition a.blocks b)) := by simp [A]
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
⊢ 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)

Tactic:
have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
zero :
  (take (take (i + 1) b.blocks).sum a.blocks).sum =
    (take (take i b.blocks).sum a.blocks).sum +
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map sum (a.blocks.splitWrtComposition b)) i B
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum

Tactic:
rw [sum_take_succ _ _ B, ← IH A C]

Premises used: List.sum_take_succ
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
rw : (take i b.blocks).sum ≤ (take (i + 1) b.blocks).sum
⊢ take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)

Tactic:
rw [take_take, min_eq_left]

Premises used: min_eq_left, List.take_take
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
⊢ (take i b.blocks).sum ≤ (take (i + 1) b.blocks).sum

Tactic:
apply monotone_sum_take _ (Nat.le_succ _)

Premises used: Nat.le_succ, List.monotone_sum_take
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
⊢ take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)

Tactic:
have :
        take (sum (take i b.blocks)) a.blocks =
          take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) := by
        rw [take_take, min_eq_left]
        apply monotone_sum_take _ (Nat.le_succ _)
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
this : take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)
zero :
  (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum +
      (drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum =
    (take (take i b.blocks).sum
          (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks) ++
            drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks))).sum +
      (drop (b.sizeUpTo i) (take (b.sizeUpTo (i + 1)) a.blocks)).sum
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum =
    (take (take i b.blocks).sum a.blocks).sum +
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map sum (a.blocks.splitWrtComposition b)) i B

Tactic:
rw [this, getElem_map, getElem_splitWrtComposition, ←
        take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks),
        sum_append]

Premises used: Composition.blocks, List.sum, List.take_append_drop, List.getElem_map, List.sum_append, Nat.succ, List.take, List.getElem_splitWrtComposition
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
this : take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)
zero :
  take (take i.succ b.blocks).sum a.blocks =
    take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks) ++
      drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)
⊢ (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum +
      (drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum =
    (take (take i b.blocks).sum
          (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks) ++
            drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks))).sum +
      (drop (b.sizeUpTo i) (take (b.sizeUpTo (i + 1)) a.blocks)).sum

Tactic:
congr
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
this : take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)
zero zero₁ : take (take i.succ b.blocks).sum a.blocks = take (take i.succ b.blocks).sum a.blocks
⊢ take (take i.succ b.blocks).sum a.blocks =
    take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks) ++
      drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)

Tactic:
rw [take_append_drop]

Premises used: List.take_append_drop
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)
zero :
  ∀ (hi : 0 < b.length) (hj : 0 < b.blocksFun (⟨0, hi⟩ : Fin b.length)),
    (take (take 0 b.blocks).sum a.blocks).sum = (take 0 (List.map sum (a.blocks.splitWrtComposition b))).sum
zero₁ :
  ∀ (i : ℕ)
    (IH :
      ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
        (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum)
    (hi : i + 1 < b.length) (hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)),
    (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum
⊢ (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum

Tactic:
induction i with
    | zero => rfl
    | succ i IH =>
      have A : i < b.length := Nat.lt_of_succ_lt hi
      have B : i < List.length (map List.sum (splitWrtComposition a.blocks b)) := by simp [A]
      have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
      rw [sum_take_succ _ _ B, ← IH A C]
      have :
        take (sum (take i b.blocks)) a.blocks =
          take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) := by
        rw [take_take, min_eq_left]
        apply monotone_sum_take _ (Nat.le_succ _)
      rw [this, getElem_map, getElem_splitWrtComposition, ←
        take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks),
        sum_append]
      congr
      rw [take_append_drop]

Premises used: Composition.blocks, List.sum, List.take_append_drop, List.getElem_map, List.sum_append, Nat.succ, List.take, List.getElem_splitWrtComposition
-- 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⟩
⊢ j < b.blocksFun ⟨i, hi⟩

Tactic:
have A : j < blocksFun b ⟨i, hi⟩ := lt_trans (lt_add_one j) hj
-- 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⟩
⊢ j < b.blocksFun ⟨i, hi⟩

Tactic:
A
-- 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⟩
h :
  length (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
      (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)) =
    b.blocksFun ⟨i, hi⟩
⊢ j < length (n := (a.gather b).blocksFun ⟨i, ⋯⟩) (a.sigmaCompositionAux b ⟨i, ⋯⟩)

Tactic:
convert! A
-- 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⟩
h h₁ :
  length (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
      (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)) =
    length (n := (a.gather b).blocksFun ⟨(↑(⟨i, hi⟩ : Fin b.length) : ℕ), ⋯⟩)
      (a.sigmaCompositionAux b ⟨(↑(⟨i, hi⟩ : Fin b.length) : ℕ), ⋯⟩)
⊢ length (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
      (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)) =
    b.blocksFun ⟨i, hi⟩

Tactic:
rw [← length_sigmaCompositionAux]

Premises used: Composition.length_sigmaCompositionAux
-- 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⟩
⊢ j < length (n := (a.gather b).blocksFun ⟨i, ⋯⟩) (a.sigmaCompositionAux b ⟨i, ⋯⟩)

Tactic:
have B : j < length (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ hi⟩) := by
      convert! A; rw [← length_sigmaCompositionAux]
-- 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, ⋯⟩)
simp : j < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks i hi
⊢ b.sizeUpTo i + j < b.sizeUpTo (i + 1)

Tactic:
simp only [sizeUpTo_succ b hi, add_lt_add_iff_left]

Premises used: Composition.sizeUpTo_succ, add_lt_add_iff_left
-- 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, ⋯⟩)
⊢ j < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks i hi

Tactic:
A

Premises used: Composition.blocksFun
-- 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, ⋯⟩)
⊢ j < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks i hi

Tactic:
exact A
-- 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, ⋯⟩)
⊢ b.sizeUpTo i + j < b.sizeUpTo (i + 1)

Tactic:
have C : sizeUpTo b i + j < sizeUpTo b (i + 1) := by
      simp only [sizeUpTo_succ b hi, add_lt_add_iff_left]
      exact A
-- 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)
⊢ b.sizeUpTo i + j < a.length

Tactic:
have D : sizeUpTo b i + j < length a := lt_of_lt_of_le C (b.sizeUpTo_le _)
-- 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
⊢ b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ

Tactic:
have : sizeUpTo b i + Nat.succ j = (sizeUpTo b i + j).succ := rfl
-- 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))
          (a.sigmaCompositionAux b (⟨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))
          (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)) j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length)
          (blocks (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
            (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)))
          j B)
⊢ a.sizeUpTo (b.sizeUpTo i + (j + 1)) =
    (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 + 1)

Tactic:
rw [this, sizeUpTo_succ _ D, IHj A, sizeUpTo_succ _ B]

Premises used: Composition.sizeUpTo_succ
-- 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)
          (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) 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 +
      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))
          (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)) j +
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length)
          (blocks (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
            (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)))
          j B)

Tactic:
simp only [sigmaCompositionAux, add_assoc]

Premises used: add_assoc, Composition.sigmaCompositionAux