no goals
ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
f : α → α
l₁ l₂ : List α
x✝ : l₂ ≠ []
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂
cases l₂ with
| nil => contradiction
| cons hd tl =>
  cases tl with
  | nil => exact modifyLast_append_one _ hd _
  | cons hd' tl' =>
    rw [append_cons, ←nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
      modifyLast_append _ (l₁ ++ [hd]) (hd' :: tl') _, modifyLast_append _ [hd] (hd' :: tl') _,
      append_assoc]
    all_goals { exact cons_ne_nil _ _ }
no goals
case nil
ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
x✝ : [] ≠ []
⊢ modifyLast f (l₁ ++ []) = l₁ ++ modifyLast f []
contradiction
no goals
case cons
ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
hd : α
tl : List α
x✝ : hd :: tl ≠ []
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)
cases tl with
| nil => exact modifyLast_append_one _ hd _
| cons hd' tl' =>
  rw [append_cons, ←nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
    modifyLast_append _ (l₁ ++ [hd]) (hd' :: tl') _, modifyLast_append _ [hd] (hd' :: tl') _,
    append_assoc]
  all_goals { exact cons_ne_nil _ _ }
no goals
case cons.nil
ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
hd : α
x✝ : [hd] ≠ []
⊢ modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]
exact modifyLast_append_one _ hd _
ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []
case cons.cons
ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ modifyLast f (l₁ ++ hd :: hd' :: tl') = l₁ ++ modifyLast f (hd :: hd' :: tl')
rw [append_cons, ←nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
  modifyLast_append _ (l₁ ++ [hd]) (hd' :: tl') _, modifyLast_append _ [hd] (hd' :: tl') _,
  append_assoc]
no goals
ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

ι : Type ?u.319860
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ : List α
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []
all_goals { exact cons_ne_nil _ _ }