no goals
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
tl : List α
r : Array α
⊢ go f (tl ++ [a]) r = Array.toListAppend r (go f (tl ++ [a]) #[])
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_ne_nil_right tl [a] (cons_ne_nil a [])
  rw [modifyLast.go_append_one _ _ tl _, modifyLast.go_append_one _ _ tl (Array.push #[] hd)]
  simp only [Array.toListAppend_eq, Array.push_data, Array.data_toArray, nil_append, append_assoc]
case nil
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
⊢ Array.toListAppend r [f a] = Array.toListAppend r (Array.toListAppend #[] [f a])
case nil
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
⊢ go f ([] ++ [a]) r = Array.toListAppend r (go f ([] ++ [a]) #[])
simp only [nil_append, modifyLast.go]
no goals
case nil
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
⊢ Array.toListAppend r [f a] = Array.toListAppend r (Array.toListAppend #[] [f a])
rfl
case cons
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: (tl ++ [a])) r = Array.toListAppend r (go f (hd :: (tl ++ [a])) #[])
case cons
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: tl ++ [a]) r = Array.toListAppend r (go f (hd :: tl ++ [a]) #[])
simp only [cons_append]
case cons
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (Array.push r hd) = Array.toListAppend r (go f (tl ++ [a]) (Array.push #[] hd))

case cons.x_3
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

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

case cons.x_3
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

case cons.x_3
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False
case x_3 | x_3 => exact append_ne_nil_of_ne_nil_right tl [a] (cons_ne_nil a [])
case cons
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ Array.toListAppend (Array.push r hd) (go f (tl ++ [a]) #[]) =
    Array.toListAppend r (Array.toListAppend (Array.push #[] hd) (go f (tl ++ [a]) #[]))
case cons
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (Array.push r hd) = Array.toListAppend r (go f (tl ++ [a]) (Array.push #[] hd))
rw [modifyLast.go_append_one _ _ tl _, modifyLast.go_append_one _ _ tl (Array.push #[] hd)]
no goals
case cons
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ Array.toListAppend (Array.push r hd) (go f (tl ++ [a]) #[]) =
    Array.toListAppend r (Array.toListAppend (Array.push #[] hd) (go f (tl ++ [a]) #[]))
simp only [Array.toListAppend_eq, Array.push_data, Array.data_toArray, nil_append, append_assoc]
no goals
ι : Type ?u.316975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False
exact append_ne_nil_of_ne_nil_right tl [a] (cons_ne_nil a [])