Theorem: List.modifyLast_cons (One.lean)

State before:
α : Type u_1
f : α → α
head : α
tail : List α
h : tail ≠ []
⊢ modifyLast f (head :: tail) = head :: modifyLast f tail
Tactic:
rw [← List.dropLast_append_getLast (List.cons_ne_nil head tail),← List.dropLast_append_getLast h,
 List.modifyLast_append_one, List.modifyLast_append_one]
State after:
α : Type u_1
f : α → α
head : α
tail : List α
h : tail ≠ []
⊢ dropLast (head :: (dropLast tail ++ [getLast tail h])) ++
      [f
          (getLast (head :: (dropLast tail ++ [getLast tail h]))
            (_ : head :: (dropLast tail ++ [getLast tail h]) ≠ []))] =
    head :: (dropLast tail ++ [f (getLast tail h)])

State before:
α : Type u_1
f : α → α
head : α
tail : List α
h : tail ≠ []
⊢ dropLast (head :: (dropLast tail ++ [getLast tail h])) ++
      [f
          (getLast (head :: (dropLast tail ++ [getLast tail h]))
            (_ : head :: (dropLast tail ++ [getLast tail h]) ≠ []))] =
    head :: (dropLast tail ++ [f (getLast tail h)])
Tactic:
simp only [append_eq_nil, and_false, IsEmpty.forall_iff, dropLast_concat, ne_eq, not_false_iff, getLast_cons,
  getLast_append, cons_append, dropLast]
State after:
no goals