Theorem: List.splitOn_last (One.lean)

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ splitOn sep (front ++ sep :: tail) = splitOn sep front ++ [tail]
Tactic:
unfold splitOn
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ splitOnP (fun x => x == sep) (front ++ sep :: tail) = splitOnP (fun x => x == sep) front ++ [tail]

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ splitOnP (fun x => x == sep) (front ++ sep :: tail) = splitOnP (fun x => x == sep) front ++ [tail]
Tactic:
apply List.splitOnP_last
State after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ ∀ (e : α), e ∈ tail → ¬(e == sep) = true

case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true

State before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ ∀ (e : α), e ∈ tail → ¬(e == sep) = true

case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true
Tactic:
. exact h
State after:
case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true

State before:
case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true
Tactic:
. simp only [beq_self_eq_true]
State after:
no goals