Theorem: List.getRest_delim_append (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ getRest (l₁ ++ l₂) l₁ = some l₂
Tactic:
induction l₁ with
| nil => simp only [nil_append, getRest_nil]
| cons head tail ih =>
  unfold getRest
  simp only [cons_append, ih, ite_true]
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ getRest ([] ++ l₂) [] = some l₂
Tactic:
simp only [nil_append, getRest_nil]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head : α
tail : List α
ih : getRest (tail ++ l₂) tail = some l₂
⊢ getRest (head :: tail ++ l₂) (head :: tail) = some l₂
Tactic:
unfold getRest
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head : α
tail : List α
ih : getRest (tail ++ l₂) tail = some l₂
⊢ (match head :: tail ++ l₂, head :: tail with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head : α
tail : List α
ih : getRest (tail ++ l₂) tail = some l₂
⊢ (match head :: tail ++ l₂, head :: tail with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
Tactic:
simp only [cons_append, ih, ite_true]
State after:
no goals