-- Mathlib/Data/List/Scan.lean
theorem getElem_succ_scanl {i : ℕ} (h : i + 1 < (scanl f b l).length) :
    (scanl f b l)[i + 1] =
      f ((scanl f b l)[i]'(Nat.lt_of_succ_lt h))
        (l[i]'(Nat.lt_of_succ_lt_succ (h.trans_eq (length_scanl b l))))

Proof state:
case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ ([b] ++ scanl f (f b head✝) tail✝)[i + 1 + 1] = f ([b] ++ scanl f (f b head✝) tail✝)[i + 1] (head✝ :: tail✝)[i + 1]

Tactic:
rw [getElem_append_right]

Result:
case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f (f b head✝) tail✝)[i + 1 + 1 - [b].length] =
    f ([b] ++ scanl f (f b head✝) tail✝)[i + 1] (head✝ :: tail✝)[i + 1]

case succ.cons.h₁
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ [b].length ≤ i + 1 + 1

Proof state:
case succ
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
l : List α
h : i + 1 + 1 < (scanl f b l).length
⊢ (scanl f b l)[i + 1 + 1] = f (scanl f b l)[i + 1] l[i + 1]

Tactic:
cases l

Result:
case succ.nil
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
h : i + 1 + 1 < (scanl f b []).length
⊢ (scanl f b [])[i + 1 + 1] = f (scanl f b [])[i + 1] [][i + 1]

case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f b (head✝ :: tail✝))[i + 1 + 1] = f (scanl f b (head✝ :: tail✝))[i + 1] (head✝ :: tail✝)[i + 1]

Proof state:
case succ.nil
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
h : i + 1 + 1 < 0 + 1
⊢ (scanl f b [])[i + 1 + 1] = f (scanl f b [])[i + 1] [][i + 1]

Tactic:
exact absurd h (by omega)

Result:
no goals

Proof state:
case zero.cons
α : Type u_1
β : Type u_2
f : β → α → β
b : β
head✝ : α
tail✝ : List α
h : 0 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f b (head✝ :: tail✝))[0 + 1] = f (scanl f b (head✝ :: tail✝))[0] (head✝ :: tail✝)[0]

Tactic:
simp

Result:
no goals

Proof state:
case zero
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
h : 0 + 1 < (scanl f b l).length
⊢ (scanl f b l)[0 + 1] = f (scanl f b l)[0] l[0]

Tactic:
cases l

Result:
case zero.nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
h : 0 + 1 < (scanl f b []).length
⊢ (scanl f b [])[0 + 1] = f (scanl f b [])[0] [][0]

case zero.cons
α : Type u_1
β : Type u_2
f : β → α → β
b : β
head✝ : α
tail✝ : List α
h : 0 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f b (head✝ :: tail✝))[0 + 1] = f (scanl f b (head✝ :: tail✝))[0] (head✝ :: tail✝)[0]

Proof state:
case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ f (scanl f (f b head✝) tail✝)[i] tail✝[i] = f ([b] ++ scanl f (f b head✝) tail✝)[i + 1] (head✝ :: tail✝)[i + 1]

Tactic:
rfl

Result:
no goals

Proof state:
case zero.nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
h : 0 + 1 < (scanl f b []).length
⊢ (scanl f b [])[0 + 1] = f (scanl f b [])[0] [][0]

Tactic:
simp only [scanl, length, zero_eq, lt_self_iff_false] at h

Result:
no goals

Proof state:
case succ.cons.h₁
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ [b].length ≤ i + 1 + 1

Tactic:
simp only [length_singleton]

Result:
case succ.cons.h₁
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ 1 ≤ i + 1 + 1

Proof state:
case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f b (head✝ :: tail✝))[i + 1 + 1] = f (scanl f b (head✝ :: tail✝))[i + 1] (head✝ :: tail✝)[i + 1]

Tactic:
simp_rw [scanl_cons]

Result:
case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ ([b] ++ scanl f (f b head✝) tail✝)[i + 1 + 1] = f ([b] ++ scanl f (f b head✝) tail✝)[i + 1] (head✝ :: tail✝)[i + 1]

Proof state:
case succ.cons.h₁
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ 1 ≤ i + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
h : i + 1 + 1 < 0 + 1
⊢ ¬i + 1 + 1 < 0 + 1

Tactic:
omega

Result:
no goals

Proof state:
case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f (f b head✝) tail✝)[i + 1 + 1 - [b].length] =
    f ([b] ++ scanl f (f b head✝) tail✝)[i + 1] (head✝ :: tail✝)[i + 1]

Tactic:
simp only [length, Nat.zero_add 1, succ_add_sub_one, hi]

Result:
case succ.cons
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
head✝ : α
tail✝ : List α
h : i + 1 + 1 < (scanl f b (head✝ :: tail✝)).length
⊢ f (scanl f (f b head✝) tail✝)[i] tail✝[i] = f ([b] ++ scanl f (f b head✝) tail✝)[i + 1] (head✝ :: tail✝)[i + 1]

Proof state:
case succ.nil
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
h : i + 1 + 1 < (scanl f b []).length
⊢ (scanl f b [])[i + 1 + 1] = f (scanl f b [])[i + 1] [][i + 1]

Tactic:
simp only [scanl, length] at h

Result:
case succ.nil
α : Type u_1
β : Type u_2
f : β → α → β
i : ℕ
hi : ∀ {b : β} {l : List α} (h : i + 1 < (scanl f b l).length), (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
b : β
h : i + 1 + 1 < 0 + 1
⊢ (scanl f b [])[i + 1 + 1] = f (scanl f b [])[i + 1] [][i + 1]