awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
rw :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map List.length (a.blocks.splitWrtComposition b))
      (↑i : ℕ) ⋯ =
    b.blocksFun i
rw₁ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯ = b.blocksFun i
⊢ (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
        ⋯).length =
    b.blocksFun i
have rw₂ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) sorry = b.blocks.get i
Tactic: rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
      get_eq_getElem]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
rw :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map List.length (a.blocks.splitWrtComposition b))
      (↑i : ℕ) ⋯ =
    b.blocksFun i
rw₁ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯ = b.blocksFun i
rw₂ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯ = b.blocks.get i
⊢ (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
        ⋯).length =
    b.blocksFun i
have rw₃ : 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
Tactic: rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
      get_eq_getElem]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ blocksFun (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 : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) ⋯,
        blocks_pos := ⋯, blocks_sum := ⋯ :
        Composition ((a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length)) }
      (⟨(↑j : ℕ), ⋯⟩ :
        Fin
          (length (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 : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) ⋯,
              blocks_pos := ⋯, blocks_sum := ⋯ :
              Composition ((a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length)) })) =
    a.blocksFun ((b.embedding i : (a_1 : Fin (b.blocksFun i)) → Fin a.length) j)
have rw : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks
    (b.sizeUpTo (↑(⟨(↑i : ℕ), sorry⟩ : Fin (a.gather b).length) : ℕ) +
      (↑(⟨(↑j : ℕ), sorry⟩ :
            Fin
              (length (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⟩ : Fin (a.gather b).length) : ℕ) sorry,
                  blocks_pos := sorry, blocks_sum := sorry :
                  Composition ((a.gather b).blocksFun (⟨(↑i : ℕ), sorry⟩ : Fin (a.gather b).length)) })) :
        ℕ))
    sorry =
  a.blocksFun ((b.embedding i : (a_1 : Fin (b.blocksFun i)) → Fin a.length) j)
Tactic: rw [blocksFun, get_eq_getElem, getElem_of_eq (getElem_splitWrtComposition _ _ _ _),
    getElem_drop, getElem_take]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)
⊢ a.sizeUpTo (b.sizeUpTo i + 0) =
    (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)) 0
have zero : (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
Tactic: change
      sum (take (b.blocks.take i).sum a.blocks) =
        sum (take i (map sum (splitWrtComposition a.blocks b)))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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)
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum
have A : i < b.length
Tactic: have A : i < b.length := Nat.lt_of_succ_lt hi
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum
have B : 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum
have C : 0 < b.blocksFun (⟨i, A⟩ : Fin b.length)
Tactic: have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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 + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum
have 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
Tactic: rw [sum_take_succ _ _ B, ← IH A C]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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)
have rw : (take i b.blocks).sum ≤ (take (i + 1) b.blocks).sum
Tactic: rw [take_take, min_eq_left]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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 + 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
have this : 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 _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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)
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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)
⊢ (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
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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)
⊢ 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)
have zero : take (take i.succ b.blocks).sum a.blocks = take (take i.succ b.blocks).sum a.blocks
Tactic: rw [take_append_drop]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
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
have 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
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]
Cleared hypotheses: i, hi, hj
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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
⊢ (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
have 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
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]
Cleared hypotheses: i, hi, hj
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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.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)
have A : j < b.blocksFun ⟨i, hi⟩
Tactic: have A : j < blocksFun b ⟨i, hi⟩ := lt_trans (lt_add_one j) hj
-- 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⟩
⊢ j < length (n := (a.gather b).blocksFun ⟨i, ⋯⟩) (a.sigmaCompositionAux b ⟨i, ⋯⟩)
have h : length (n := (a.gather b).blocksFun (⟨i, sorry⟩ : Fin (a.gather b).length))
    (a.sigmaCompositionAux b (⟨i, sorry⟩ : Fin (a.gather b).length)) =
  b.blocksFun ⟨i, hi⟩
Tactic: convert! A
-- 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⟩
⊢ 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⟩
have h : length (n := (a.gather b).blocksFun (⟨i, sorry⟩ : Fin (a.gather b).length))
    (a.sigmaCompositionAux b (⟨i, sorry⟩ : Fin (a.gather b).length)) =
  length (n := (a.gather b).blocksFun ⟨(↑(⟨i, hi⟩ : Fin b.length) : ℕ), sorry⟩)
    (a.sigmaCompositionAux b ⟨(↑(⟨i, hi⟩ : Fin b.length) : ℕ), sorry⟩)
Tactic: rw [← length_sigmaCompositionAux]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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⟩
⊢ 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)
have B : j < length (n := (a.gather b).blocksFun ⟨i, sorry⟩) (a.sigmaCompositionAux b ⟨i, sorry⟩)
Tactic: have B : j < length (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ hi⟩) := by
      convert! A; rw [← length_sigmaCompositionAux]
-- 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, ⋯⟩)
⊢ b.sizeUpTo i + j < b.sizeUpTo (i + 1)
have simp : j < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks i hi
Tactic: simp only [sizeUpTo_succ b hi, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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, ⋯⟩)
⊢ 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)
have C : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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)
⊢ 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)
have D : b.sizeUpTo i + j < a.length
Tactic: have D : sizeUpTo b i + j < length a := lt_of_lt_of_le C (b.sizeUpTo_le _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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
⊢ 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)
have this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
Tactic: have : sizeUpTo b i + Nat.succ j = (sizeUpTo b i + j).succ := rfl