Theorem: List.splitOnList_intercalate
Proof 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]
Proof 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)