-- Mathlib/Data/List/ModifyLast.lean
theorem modifyLast.go_concat (f : α → α) (a : α) (tl : List α) (r : Array α) :
    modifyLast.go f (tl ++ [a]) r = (r.toListAppend <| modifyLast.go f (tl ++ [a]) #[])

Proof state:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

Tactic:
rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]

Result:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ (r.push hd).toListAppend (go f (tl ++ [a]) #[]) = r.toListAppend ((#[].push hd).toListAppend (go f (tl ++ [a]) #[]))

Proof state:
case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ r.toListAppend [f a] = r.toListAppend (#[].toListAppend [f a])

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
case x_3 | x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Result:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

Proof state:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ (r.push hd).toListAppend (go f (tl ++ [a]) #[]) = r.toListAppend ((#[].push hd).toListAppend (go f (tl ++ [a]) #[]))

Tactic:
simp only [Array.toListAppend_eq, Array.push_toList, Array.toList_toArray, nil_append,
  append_assoc]

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: (tl ++ [a])) r = r.toListAppend (go f (hd :: (tl ++ [a])) #[])

Tactic:
rw [modifyLast.go, modifyLast.go]

Result:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Proof state:
α : Type u_1
f : α → α
a : α
tl : List α
r : Array α
⊢ go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])

Tactic:
cases tl with
| nil =>
  simp only [nil_append, modifyLast.go]; rfl
| cons hd tl =>
  simp only [cons_append]
  rw [modifyLast.go, modifyLast.go]
  case x_3 | x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
  rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]
  simp only [Array.toListAppend_eq, Array.push_toList, Array.toList_toArray, nil_append,
    append_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ go f ([] ++ [a]) r = r.toListAppend (go f ([] ++ [a]) #[])

Tactic:
simp only [nil_append, modifyLast.go]

Result:
case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ r.toListAppend [f a] = r.toListAppend (#[].toListAppend [f a])

Proof state:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: tl ++ [a]) r = r.toListAppend (go f (hd :: tl ++ [a]) #[])

Tactic:
simp only [cons_append]

Result:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: (tl ++ [a])) r = r.toListAppend (go f (hd :: (tl ++ [a])) #[])