Theorem: List.eq_append_of_getRest (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
l l₁ l₂ : List α
P : getRest l l₁ = some l₂
⊢ l = l₁ ++ l₂
Tactic:
induction l₁ generalizing l l₂ with
| nil =>
  unfold getRest at P
  simp only [Option.some.injEq] at P
  simp only [P, nil_append]
| cons head tail ih =>
  unfold getRest at P
  split at P
  case h_1 heq => simp only at heq
  case h_2 => simp only at P
  case h_3 hd tl y l₁ heq =>
    split at P
    case inr heq₂ => contradiction
    case inl heq₂ =>
      injection heq
      subst hd y l₁
      simp only [cons_append, cons.injEq, true_and]
      apply ih
      apply P
State after:
no goals

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

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l₂ : List α
P :
  (match l, [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ l = [] ++ l₂
Tactic:
simp only [Option.some.injEq] at P
State after:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l₂ : List α
P : l = l₂
⊢ l = [] ++ l₂

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

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

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l l₂ : List α
P :
  (match l, head :: tail with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ l = head :: tail ++ l₂
Tactic:
split at P
State after:
case cons.h_1
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ x✝ : List α
heq✝ : head :: tail = []
P : some x✝² = some l₂
⊢ x✝² = head :: tail ++ l₂

case cons.h_2
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : head :: tail = [] → False
P : none = some l₂
⊢ [] = head :: tail ++ l₂

case cons.h_3
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq✝ : head :: tail = y✝ :: l₁✝
P : (if x✝ = y✝ then getRest l✝ l₁✝ else none) = some l₂
⊢ x✝ :: l✝ = head :: tail ++ l₂

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ x✝ : List α
heq : head :: tail = []
P : some x✝² = some l₂
⊢ x✝² = head :: tail ++ l₂
Tactic:
case h_1 heq => simp only at heq
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : head :: tail = [] → False
P : none = some l₂
⊢ [] = head :: tail ++ l₂
Tactic:
case h_2 => simp only at P
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
P : (if hd = y then getRest tl l₁ else none) = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
case h_3 hd tl y l₁ heq =>
  split at P
  case inr heq₂ => contradiction
  case inl heq₂ =>
    injection heq
    subst hd y l₁
    simp only [cons_append, cons.injEq, true_and]
    apply ih
    apply P
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ x✝ : List α
heq : head :: tail = []
P : some x✝² = some l₂
⊢ x✝² = head :: tail ++ l₂
Tactic:
simp only at heq
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : head :: tail = [] → False
P : none = some l₂
⊢ [] = head :: tail ++ l₂
Tactic:
simp only at P
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
P : (if hd = y then getRest tl l₁ else none) = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
split at P
State after:
case inl
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
h✝ : hd = y
P : getRest tl l₁ = some l₂
⊢ hd :: tl = head :: tail ++ l₂

case inr
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
h✝ : ¬hd = y
P : False
⊢ hd :: tl = head :: tail ++ l₂

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : ¬hd = y
P : False
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
case inr heq₂ => contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : hd = y
P : getRest tl l₁ = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
case inl heq₂ =>
  injection heq
  subst hd y l₁
  simp only [cons_append, cons.injEq, true_and]
  apply ih
  apply P
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : ¬hd = y
P : False
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : hd = y
P : getRest tl l₁ = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
injection heq
State after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq₂ : hd = y
P : getRest tl l₁ = some l₂
head_eq✝ : head = y
tail_eq✝ : tail = l₁
⊢ hd :: tl = head :: tail ++ l₂

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq₂ : hd = y
P : getRest tl l₁ = some l₂
head_eq✝ : head = y
tail_eq✝ : tail = l₁
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
subst hd y l₁
State after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ head :: tl = head :: tail ++ l₂

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ head :: tl = head :: tail ++ l₂
Tactic:
simp only [cons_append, cons.injEq, true_and]
State after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ tl = tail ++ l₂

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ tl = tail ++ l₂
Tactic:
apply ih
State after:
case P
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ getRest tl tail = some l₂

State before:
case P
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ getRest tl tail = some l₂
Tactic:
apply P
State after:
no goals