Theorem: List.splitOnP_last (One.lean)

State before:
α : Type u_1
P : α → Bool
inst✝ : BEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P (front ++ sep :: tail) = splitOnP P front ++ [tail]
Tactic:
induction front with
| nil => 
  simp only [nil_append, splitOnP_cons, hsep, modifyHead, ite_true, splitOnP_nil, singleton_append, cons.injEq,
    true_and]
  rw [List.splitOnP_eq_single]
  apply h
| cons hd tl ih =>
  simp only [cons_append, splitOnP_cons]
  split
  . simp only [ih, cons_append]
  . rw [ih, List.modifyHead_append]
    apply List.splitOnP_ne_nil
State after:
no goals

State before:
case nil
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P ([] ++ sep :: tail) = splitOnP P [] ++ [tail]
Tactic:
simp only [nil_append, splitOnP_cons, hsep, modifyHead, ite_true, splitOnP_nil, singleton_append, cons.injEq,
  true_and]
State after:
case nil
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P tail = [tail]

State before:
case nil
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P tail = [tail]
Tactic:
rw [List.splitOnP_eq_single]
State after:
case nil.h
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ ∀ (x : α), x ∈ tail → ¬P x = true

State before:
case nil.h
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ ∀ (x : α), x ∈ tail → ¬P x = true
Tactic:
apply h
State after:
no goals

State before:
case cons
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
⊢ splitOnP P (hd :: tl ++ sep :: tail) = splitOnP P (hd :: tl) ++ [tail]
Tactic:
simp only [cons_append, splitOnP_cons]
State after:
case cons
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
⊢ (if P hd = true then [] :: splitOnP P (tl ++ sep :: tail)
    else modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail))) =
    (if P hd = true then [] :: splitOnP P tl else modifyHead (cons hd) (splitOnP P tl)) ++ [tail]

State before:
case cons
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
⊢ (if P hd = true then [] :: splitOnP P (tl ++ sep :: tail)
    else modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail))) =
    (if P hd = true then [] :: splitOnP P tl else modifyHead (cons hd) (splitOnP P tl)) ++ [tail]
Tactic:
split
State after:
case cons.inl
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : P hd = true
⊢ [] :: splitOnP P (tl ++ sep :: tail) = [] :: splitOnP P tl ++ [tail]

case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]

State before:
case cons.inl
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : P hd = true
⊢ [] :: splitOnP P (tl ++ sep :: tail) = [] :: splitOnP P tl ++ [tail]

case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]
Tactic:
. simp only [ih, cons_append]
State after:
case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]

State before:
case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]
Tactic:
. rw [ih, List.modifyHead_append]
  apply List.splitOnP_ne_nil
State after:
no goals