Theorem: List.splitOnList_intercalate (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
l : List (List α)
h : ∀ (e : List α), e ∈ l → ¬delim <:+: e ++ dropLast delim
h₂ : l ≠ []
⊢ splitOnList delim (intercalate delim l) = l
Tactic:
induction l with
| nil => 
  contradiction
| cons head tail ih=>
  cases delim
  case nil =>
    simp only [find?, mem_cons, dropLast, append_nil, nil_isInfix, not_true, forall_eq_or_imp, false_and] at h head
  case cons dhead dtail=>
    unfold intercalate
    cases h₂:tail with
    | nil => 
      subst tail
      simp only [join, append_nil]
      apply List.splitOnList_nonmatching
      have h₃ := (h head (List.mem_singleton_self _))
      intro ⟨s,t, hcontr⟩
      apply h₃
      exists s, (t ++ dropLast (dhead :: dtail))
      simp only [append_assoc, cons_append, ← hcontr]
    | cons mid tail₂ =>
      simp only [join]
      rw [← List.append_assoc, List.splitOnList_progress, ← List.intercalate, ← h₂, ih]
      . simp only [singleton_append]
      . intro e ein
        apply h
        subst h₂
        simp_all only [find?, mem_cons, ne_eq, not_false_iff, or_true, implies_true, forall_const, forall_true_left,
          forall_eq_or_imp]
      . simp only [h₂, ne_eq, not_false_iff]
      . intro contr
        apply h head
        apply List.mem_cons_self
        exact contr
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : ∀ (e : List α), e ∈ [] → ¬delim <:+: e ++ dropLast delim
h₂ : [] ≠ []
⊢ splitOnList delim (intercalate delim []) = []
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
delim head : List α
tail : List (List α)
ih :
  (∀ (e : List α), e ∈ tail → ¬delim <:+: e ++ dropLast delim) →
    tail ≠ [] → splitOnList delim (intercalate delim tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬delim <:+: e ++ dropLast delim
h₂ : head :: tail ≠ []
⊢ splitOnList delim (intercalate delim (head :: tail)) = head :: tail
Tactic:
cases delim
State after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
ih : (∀ (e : List α), e ∈ tail → ¬[] <:+: e ++ dropLast []) → tail ≠ [] → splitOnList [] (intercalate [] tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬[] <:+: e ++ dropLast []
⊢ splitOnList [] (intercalate [] (head :: tail)) = head :: tail

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
head✝ : α
tail✝ : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬head✝ :: tail✝ <:+: e ++ dropLast (head✝ :: tail✝)) →
    tail ≠ [] → splitOnList (head✝ :: tail✝) (intercalate (head✝ :: tail✝) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬head✝ :: tail✝ <:+: e ++ dropLast (head✝ :: tail✝)
⊢ splitOnList (head✝ :: tail✝) (intercalate (head✝ :: tail✝) (head :: tail)) = head :: tail

State before:
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
ih : (∀ (e : List α), e ∈ tail → ¬[] <:+: e ++ dropLast []) → tail ≠ [] → splitOnList [] (intercalate [] tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬[] <:+: e ++ dropLast []
⊢ splitOnList [] (intercalate [] (head :: tail)) = head :: tail
Tactic:
case nil =>
  simp only [find?, mem_cons, dropLast, append_nil, nil_isInfix, not_true, forall_eq_or_imp, false_and] at h head
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) (head :: tail)) = head :: tail
Tactic:
case cons dhead dtail=>
  unfold intercalate
  cases h₂:tail with
  | nil => 
    subst tail
    simp only [join, append_nil]
    apply List.splitOnList_nonmatching
    have h₃ := (h head (List.mem_singleton_self _))
    intro ⟨s,t, hcontr⟩
    apply h₃
    exists s, (t ++ dropLast (dhead :: dtail))
    simp only [append_assoc, cons_append, ← hcontr]
  | cons mid tail₂ =>
    simp only [join]
    rw [← List.append_assoc, List.splitOnList_progress, ← List.intercalate, ← h₂, ih]
    . simp only [singleton_append]
    . intro e ein
      apply h
      subst h₂
      simp_all only [find?, mem_cons, ne_eq, not_false_iff, or_true, implies_true, forall_const, forall_true_left,
        forall_eq_or_imp]
    . simp only [h₂, ne_eq, not_false_iff]
    . intro contr
      apply h head
      apply List.mem_cons_self
      exact contr
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
ih : (∀ (e : List α), e ∈ tail → ¬[] <:+: e ++ dropLast []) → tail ≠ [] → splitOnList [] (intercalate [] tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬[] <:+: e ++ dropLast []
⊢ splitOnList [] (intercalate [] (head :: tail)) = head :: tail
Tactic:
simp only [find?, mem_cons, dropLast, append_nil, nil_isInfix, not_true, forall_eq_or_imp, false_and] at h head
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) (head :: tail)) = head :: tail
Tactic:
unfold intercalate
State after:
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) (join (intersperse (dhead :: dtail) (head :: tail))) = head :: tail

State before:
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) (join (intersperse (dhead :: dtail) (head :: tail))) = head :: tail
Tactic:
cases h₂:tail with
| nil => 
  subst tail
  simp only [join, append_nil]
  apply List.splitOnList_nonmatching
  have h₃ := (h head (List.mem_singleton_self _))
  intro ⟨s,t, hcontr⟩
  apply h₃
  exists s, (t ++ dropLast (dhead :: dtail))
  simp only [append_assoc, cons_append, ← hcontr]
| cons mid tail₂ =>
  simp only [join]
  rw [← List.append_assoc, List.splitOnList_progress, ← List.intercalate, ← h₂, ih]
  . simp only [singleton_append]
  . intro e ein
    apply h
    subst h₂
    simp_all only [find?, mem_cons, ne_eq, not_false_iff, or_true, implies_true, forall_const, forall_true_left,
      forall_eq_or_imp]
  . simp only [h₂, ne_eq, not_false_iff]
  . intro contr
    apply h head
    apply List.mem_cons_self
    exact contr
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₂ : tail = []
⊢ splitOnList (dhead :: dtail) (join (intersperse (dhead :: dtail) [head])) = [head]
Tactic:
subst tail
State after:
case nil
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) (join (intersperse (dhead :: dtail) [head])) = [head]

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) (join (intersperse (dhead :: dtail) [head])) = [head]
Tactic:
simp only [join, append_nil]
State after:
case nil
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) head = [head]

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ splitOnList (dhead :: dtail) head = [head]
Tactic:
apply List.splitOnList_nonmatching
State after:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ ¬dhead :: dtail <:+: head

State before:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
⊢ ¬dhead :: dtail <:+: head
Tactic:
have h₃ := (h head (List.mem_singleton_self _))
State after:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
⊢ ¬dhead :: dtail <:+: head

State before:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
⊢ ¬dhead :: dtail <:+: head
Tactic:
intro ⟨s,t, hcontr⟩
State after:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
s t : List α
hcontr : s ++ dhead :: dtail ++ t = head
⊢ False

State before:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
s t : List α
hcontr : s ++ dhead :: dtail ++ t = head
⊢ False
Tactic:
apply h₃
State after:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
s t : List α
hcontr : s ++ dhead :: dtail ++ t = head
⊢ dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)

State before:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
s t : List α
hcontr : s ++ dhead :: dtail ++ t = head
⊢ dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
exists s, (t ++ dropLast (dhead :: dtail))
State after:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
s t : List α
hcontr : s ++ dhead :: dtail ++ t = head
⊢ s ++ dhead :: dtail ++ (t ++ dropLast (dhead :: dtail)) = head ++ dropLast (dhead :: dtail)

State before:
case nil.h₁
α : Type u_1
inst✝ : DecidableEq α
head : List α
dhead : α
dtail : List α
h₂ : [head] ≠ []
ih :
  (∀ (e : List α), e ∈ [] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    [] ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) []) = []
h : ∀ (e : List α), e ∈ [head] → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
h₃ : ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
s t : List α
hcontr : s ++ dhead :: dtail ++ t = head
⊢ s ++ dhead :: dtail ++ (t ++ dropLast (dhead :: dtail)) = head ++ dropLast (dhead :: dtail)
Tactic:
simp only [append_assoc, cons_append, ← hcontr]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ splitOnList (dhead :: dtail) (join (intersperse (dhead :: dtail) (head :: mid :: tail₂))) = head :: mid :: tail₂
Tactic:
simp only [join]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ splitOnList (dhead :: dtail) (head ++ (dhead :: dtail ++ join (intersperse (dhead :: dtail) (mid :: tail₂)))) =
    head :: mid :: tail₂

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ splitOnList (dhead :: dtail) (head ++ (dhead :: dtail ++ join (intersperse (dhead :: dtail) (mid :: tail₂)))) =
    head :: mid :: tail₂
Tactic:
rw [← List.append_assoc, List.splitOnList_progress, ← List.intercalate, ← h₂, ih]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ [head] ++ tail = head :: tail

case cons.h
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)

case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ [head] ++ tail = head :: tail

case cons.h
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)

case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
. simp only [singleton_append]
State after:
case cons.h
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)

case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)

State before:
case cons.h
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)

case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
. intro e ein
  apply h
  subst h₂
  simp_all only [find?, mem_cons, ne_eq, not_false_iff, or_true, implies_true, forall_const, forall_true_left,
    forall_eq_or_imp]
State after:
case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)

State before:
case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
. simp only [h₂, ne_eq, not_false_iff]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
. intro contr
  apply h head
  apply List.mem_cons_self
  exact contr
State after:
no goals