internlm/Lean-Github huggingface dataset:
Theorem: List.count_pos_iff_mem
Proof state before:
case mp.cons.inr.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < count a tail
⊢ a ∈ tail
Tactic:
apply ih hlt
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mpr.nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
ain : a ∈ []
⊢ count a [] > 0
Tactic:
simp only [not_mem_nil] at ain
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mpr.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : a ∈ tail → count a tail > 0
ain : a ∈ head :: tail
⊢ count a (head :: tail) > 0
Tactic:
cases mem_cons.1 ain with
| inl heq =>
  simp only [heq, count_cons, beq_self_eq_true, ite_true, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt,
    add_pos_iff, true_or]
| inr hin =>
  simp only [count_cons, beq_iff_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt, add_pos_iff, ih hin, or_true]
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mpr.cons.inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : a ∈ tail → count a tail > 0
ain : a ∈ head :: tail
heq : a = head
⊢ count a (head :: tail) > 0
Tactic:
simp only [heq, count_cons, beq_self_eq_true, ite_true, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt,
  add_pos_iff, true_or]
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mpr.cons.inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : a ∈ tail → count a tail > 0
ain : a ∈ head :: tail
hin : a ∈ tail
⊢ count a (head :: tail) > 0
Tactic:
simp only [count_cons, beq_iff_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt, add_pos_iff, ih hin, or_true]
Proof state after:
no goals
Theorem: List.splitOnList_intercalate
Proof 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
Proof state after:
no goals
Theorem: List.splitOnList_intercalate
Proof 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
Proof state after:
no goals
Theorem: List.splitOnList_intercalate
Proof 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
Proof 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
Theorem: List.splitOnList_intercalate
Proof 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
Proof state after:
no goals
Theorem: List.splitOnList_intercalate
Proof 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
Proof state after:
no goals
Theorem: List.splitOnList_intercalate
Proof 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
Proof state after:
no goals
Theorem: List.splitOnList_intercalate
Proof 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
Proof 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
Theorem: List.splitOnList_intercalate
Proof 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
Proof state after:
no goals
Theorem: List.splitOnList_intercalate
Proof 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
Proof 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]
Theorem: List.splitOnList_intercalate
Proof 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]
Proof 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]
Theorem: List.splitOnList_intercalate
Proof 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
Proof 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
Theorem: List.splitOnList_intercalate
Proof 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 _))
Proof 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
Theorem: List.splitOnList_intercalate
Proof 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⟩
Proof 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
Theorem: List.splitOnList_intercalate
Proof 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₃
Proof 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)
Theorem: List.splitOnList_intercalate
Proof 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))
Proof 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)
Theorem: List.splitOnList_intercalate
Proof 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]
Proof state after:
no goals
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₂
⊢ splitOnList (dhead :: dtail) (join (intersperse (dhead :: dtail) (head :: mid :: tail₂))) = head :: mid :: tail₂
Tactic:
simp only [join]
Proof 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₂
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₂
⊢ 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]
Proof 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)