Theorem: List.getRest_none (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ getRest l₁ l₂ = none ↔ ¬l₂ <+: l₁
Tactic:
apply iff_not_comm.1
State after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ¬getRest l₁ l₂ = none

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ¬getRest l₁ l₂ = none
Tactic:
rw [← ne_eq, Option.ne_none_iff_exists]
State after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ∃ x, some x = getRest l₁ l₂

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ∃ x, some x = getRest l₁ l₂
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ → ∃ x, some x = getRest l₁ l₂

case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ → ∃ x, some x = getRest l₁ l₂

case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁
Tactic:
. intro ⟨l₃, h⟩
  subst h
  exists l₃
  exact Eq.symm getRest_delim_append
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁
Tactic:
. intro ⟨l₃, h⟩
  exists l₃
  exact Eq.symm (eq_append_of_getRest (Eq.symm h))
State after:
no goals