no goals
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
l : List α
⊢ modifyLast f (l ++ [a]) = l ++ [f a]
cases l with
| nil =>
  simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq, Array.data_toArray]
| cons _ tl =>
  simp only [cons_append, modifyLast]
  rw [modifyLast.go]
  case x_3 => exact append_ne_nil_of_ne_nil_right tl [a] (cons_ne_nil a [])
  rw [modifyLast.go_append_one, Array.toListAppend_eq, Array.push_data, Array.data_toArray,
    nil_append, cons_append, nil_append, cons_inj]
  exact modifyLast_append_one _ _ tl
no goals
case nil
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
⊢ modifyLast f ([] ++ [a]) = [] ++ [f a]
simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq, Array.data_toArray]
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (head✝ :: (tl ++ [a])) #[] = head✝ :: (tl ++ [f a])
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast f (head✝ :: tl ++ [a]) = head✝ :: tl ++ [f a]
simp only [cons_append, modifyLast]
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (Array.push #[] head✝) = head✝ :: (tl ++ [f a])

case cons.x_3
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (head✝ :: (tl ++ [a])) #[] = head✝ :: (tl ++ [f a])
rw [modifyLast.go]
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (Array.push #[] head✝) = head✝ :: (tl ++ [f a])
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (Array.push #[] head✝) = head✝ :: (tl ++ [f a])

case cons.x_3
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False
case x_3 => exact append_ne_nil_of_ne_nil_right tl [a] (cons_ne_nil a [])
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (Array.push #[] head✝) = head✝ :: (tl ++ [f a])
rw [modifyLast.go_append_one, Array.toListAppend_eq, Array.push_data, Array.data_toArray,
  nil_append, cons_append, nil_append, cons_inj]
no goals
case cons
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]
exact modifyLast_append_one _ _ tl
no goals
ι : Type ?u.319092
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False
exact append_ne_nil_of_ne_nil_right tl [a] (cons_ne_nil a [])