Theorem: List.splitOnP_append (One.lean)

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
l₁ : List α✝
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P l₁)
Tactic:
induction l₁ with
| nil => 
  simp only [nil_append, List.append_eq, splitOnP_nil, modifyLast_singleton]
  apply List.splitOnP_eq_single
  apply h
| cons head tail ih =>
  rw [cons_append, splitOnP_cons, splitOnP_cons]
  split
  case inl heq =>
    rw [ih,modifyLast_cons]
    apply List.splitOnP_ne_nil
  case inr heq =>
    rw [ih, modifyLast_eq_modifyNth, modifyLast_eq_modifyNth,
      modifyHead_eq_modifyNth, modifyHead_eq_modifyNth,
      modifyNth_comm_of_comm]
    simp only [List.append_eq, tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, modify_get?_length]
    simp only [Function.Commute, Function.Semiconj, List.append_eq, cons_append, forall_const]
State after:
no goals

State before:
case nil
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P ([] ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P [])
Tactic:
simp only [nil_append, List.append_eq, splitOnP_nil, modifyLast_singleton]
State after:
case nil
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P l₂ = [l₂]

State before:
case nil
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P l₂ = [l₂]
Tactic:
apply List.splitOnP_eq_single
State after:
case nil.h
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ ∀ (x : α✝), x ∈ l₂ → ¬P x = true

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

State before:
case cons
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
⊢ splitOnP P (head :: tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P (head :: tail))
Tactic:
rw [cons_append, splitOnP_cons, splitOnP_cons]
State after:
case cons
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
⊢ (if P head = true then [] :: splitOnP P (tail ++ l₂) else modifyHead (cons head) (splitOnP P (tail ++ l₂))) =
    modifyLast (fun x => List.append x l₂)
      (if P head = true then [] :: splitOnP P tail else modifyHead (cons head) (splitOnP P tail))

State before:
case cons
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
⊢ (if P head = true then [] :: splitOnP P (tail ++ l₂) else modifyHead (cons head) (splitOnP P (tail ++ l₂))) =
    modifyLast (fun x => List.append x l₂)
      (if P head = true then [] :: splitOnP P tail else modifyHead (cons head) (splitOnP P tail))
Tactic:
split
State after:
case cons.inl
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
h✝ : P head = true
⊢ [] :: splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) ([] :: splitOnP P tail)

case cons.inr
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
h✝ : ¬P head = true
⊢ modifyHead (cons head) (splitOnP P (tail ++ l₂)) =
    modifyLast (fun x => List.append x l₂) (modifyHead (cons head) (splitOnP P tail))

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ [] :: splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) ([] :: splitOnP P tail)
Tactic:
case inl heq =>
  rw [ih,modifyLast_cons]
  apply List.splitOnP_ne_nil
State after:
no goals

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyHead (cons head) (splitOnP P (tail ++ l₂)) =
    modifyLast (fun x => List.append x l₂) (modifyHead (cons head) (splitOnP P tail))
Tactic:
case inr heq =>
  rw [ih, modifyLast_eq_modifyNth, modifyLast_eq_modifyNth,
    modifyHead_eq_modifyNth, modifyHead_eq_modifyNth,
    modifyNth_comm_of_comm]
  simp only [List.append_eq, tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, modify_get?_length]
  simp only [Function.Commute, Function.Semiconj, List.append_eq, cons_append, forall_const]
State after:
no goals

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ [] :: splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) ([] :: splitOnP P tail)
Tactic:
rw [ih,modifyLast_cons]
State after:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ splitOnP P tail ≠ []

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ splitOnP P tail ≠ []
Tactic:
apply List.splitOnP_ne_nil
State after:
no goals

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyHead (cons head) (splitOnP P (tail ++ l₂)) =
    modifyLast (fun x => List.append x l₂) (modifyHead (cons head) (splitOnP P tail))
Tactic:
rw [ih, modifyLast_eq_modifyNth, modifyLast_eq_modifyNth,
  modifyHead_eq_modifyNth, modifyHead_eq_modifyNth,
  modifyNth_comm_of_comm]
State after:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyNth (fun x => List.append x l₂) (length (splitOnP P tail) - 1) (modifyNth (cons head) 0 (splitOnP P tail)) =
    modifyNth (fun x => List.append x l₂) (length (modifyNth (cons head) 0 (splitOnP P tail)) - 1)
      (modifyNth (cons head) 0 (splitOnP P tail))

α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyNth (fun x => List.append x l₂) (length (splitOnP P tail) - 1) (modifyNth (cons head) 0 (splitOnP P tail)) =
    modifyNth (fun x => List.append x l₂) (length (modifyNth (cons head) 0 (splitOnP P tail)) - 1)
      (modifyNth (cons head) 0 (splitOnP P tail))

α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂
Tactic:
simp only [List.append_eq, tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, modify_get?_length]
State after:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂

State before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂
Tactic:
simp only [Function.Commute, Function.Semiconj, List.append_eq, cons_append, forall_const]
State after:
no goals