Theorem: List.modifyHead_append (One.lean)

State before:
α✝ : Type u_1
l₁ : List α✝
f : α✝ → α✝
l₂ : List α✝
h : l₁ ≠ []
⊢ modifyHead f (l₁ ++ l₂) = modifyHead f l₁ ++ l₂
Tactic:
cases l₁ with
| nil => simp only [ne_eq, not_true] at h
| cons head tail => simp only [modifyHead, cons_append]
State after:
no goals

State before:
case nil
α✝ : Type u_1
f : α✝ → α✝
l₂ : List α✝
h : [] ≠ []
⊢ modifyHead f ([] ++ l₂) = modifyHead f [] ++ l₂
Tactic:
simp only [ne_eq, not_true] at h
State after:
no goals

State before:
case cons
α✝ : Type u_1
f : α✝ → α✝
l₂ : List α✝
head : α✝
tail : List α✝
h : head :: tail ≠ []
⊢ modifyHead f (head :: tail ++ l₂) = modifyHead f (head :: tail) ++ l₂
Tactic:
simp only [modifyHead, cons_append]
State after:
no goals