-- Mathlib/Data/List/SplitLengths.lean
theorem length_splitLengths_getElem_le {i : ℕ} {hi : i < (sz.splitLengths l).length} :
    (sz.splitLengths l)[i].length ≤ sz[i]'(by simpa using hi)

Proof state:
case nil
α : Type u_1
l : List α
i : ℕ
hi : i < ([].splitLengths l).length
⊢ ([].splitLengths l)[i].length ≤ [][i]

Tactic:
simp at hi

Result:
no goals

Proof state:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using hi

Result:
no goals

Proof state:
case zero
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[0].length ≤ (head :: tail)[0]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[i].length ≤ (head :: tail)[i]

Tactic:
cases i

Result:
case zero
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[0].length ≤ (head :: tail)[0]

case succ
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
n✝ : ℕ
hi : n✝ + 1 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[n✝ + 1].length ≤ (head :: tail)[n✝ + 1]

Proof state:
case succ
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
n✝ : ℕ
hi : n✝ + 1 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[n✝ + 1].length ≤ (head :: tail)[n✝ + 1]

Tactic:
simp only [getElem_cons_succ, tail_ih]

Result:
no goals

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ ((head :: tail).splitLengths l)[i].length ≤ (head :: tail)[i]

Tactic:
simp only [splitLengths_cons]

Result:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[i].length ≤ (head :: tail)[i]

Proof state:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length ≤ sz[i]

Tactic:
induction sz generalizing l i

Result:
case nil
α : Type u_1
l : List α
i : ℕ
hi : i < ([].splitLengths l).length
⊢ ([].splitLengths l)[i].length ≤ [][i]

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α) {i : ℕ} {hi : i < (tail✝.splitLengths l).length}, (tail✝.splitLengths l)[i].length ≤ tail✝[i]
l : List α
i : ℕ
hi : i < ((head✝ :: tail✝).splitLengths l).length
⊢ ((head✝ :: tail✝).splitLengths l)[i].length ≤ (head✝ :: tail✝)[i]