internlm/Lean-Github huggingface dataset:
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₂
Tactic:
rw [← len_sum_eq]
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₁ + (length t + length s)
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₁ + (length t + length s)
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
h : a ∈ intersperse sep l
⊢ a = sep ∨ a ∈ l
Tactic:
match l with
| [] => rw [intersperse] at h; contradiction
| [single] =>
  simp only [intersperse, mem_singleton] at h
  right
  simp only [h, mem_singleton]
| head::mid::tail =>
  simp only [intersperse, mem_cons] at h
  simp only [mem_cons]
  rcases h with hd | sp | mem
  . simp only [hd, true_or, or_true]
  . simp only [sp, true_or]
  . rcases mem_intersperse mem with mid | tl
    . simp only [mid, true_or]
    . simp only [mem_cons] at tl
      simp only [tl, or_true]
Proof state after:
no goals
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
h : a ∈ intersperse sep []
⊢ a = sep ∨ a ∈ []
Tactic:
rw [intersperse] at h
Proof state after:
α✝ : Type u_1
a sep : α✝
l : List α✝
h : a ∈ []
⊢ a = sep ∨ a ∈ []
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
h : a ∈ []
⊢ a = sep ∨ a ∈ []
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a ∈ intersperse sep [single]
⊢ a = sep ∨ a ∈ [single]
Tactic:
simp only [intersperse, mem_singleton] at h
Proof state after:
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a = sep ∨ a ∈ [single]
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a = sep ∨ a ∈ [single]
Tactic:
right
Proof state after:
case h
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a ∈ [single]
Theorem: List.mem_intersperse
Proof state before:
case h
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a ∈ [single]
Tactic:
simp only [h, mem_singleton]
Proof state after:
no goals
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
h : a ∈ intersperse sep (head :: mid :: tail)
⊢ a = sep ∨ a ∈ head :: mid :: tail
Tactic:
simp only [intersperse, mem_cons] at h
Proof state after:
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
h : a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a ∈ head :: mid :: tail
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
h : a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a ∈ head :: mid :: tail
Tactic:
simp only [mem_cons]
Proof state after:
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
h : a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Theorem: List.mem_intersperse
Proof state before:
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
h : a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Tactic:
rcases h with hd | sp | mem
Proof state after:
case inl
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
hd : a = head
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail

case inr.inl
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
sp : a = sep
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail

case inr.inr
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
mem : a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Theorem: List.mem_intersperse
Proof state before:
case inl
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
hd : a = head
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail

case inr.inl
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
sp : a = sep
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail

case inr.inr
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
mem : a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Tactic:
. simp only [hd, true_or, or_true]
Proof state after:
case inr.inl
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
sp : a = sep
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail

case inr.inr
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
mem : a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Theorem: List.mem_intersperse
Proof state before:
case inr.inl
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
sp : a = sep
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail

case inr.inr
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
mem : a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Tactic:
. simp only [sp, true_or]
Proof state after:
case inr.inr
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
mem : a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Theorem: List.mem_intersperse
Proof state before:
case inr.inr
α✝ : Type u_1
a sep : α✝
l : List α✝
head mid : α✝
tail : List α✝
mem : a ∈ intersperse sep (mid :: tail)
⊢ a = sep ∨ a = head ∨ a = mid ∨ a ∈ tail
Tactic:
. rcases mem_intersperse mem with mid | tl
  . simp only [mid, true_or]
  . simp only [mem_cons] at tl
    simp only [tl, or_true]
Proof state after:
no goals
Theorem: List.mem_intersperse_of_mem
Proof state before:
α✝ : Type u_1
a : α✝
l : List α✝
sep : α✝
h : a ∈ l
⊢ a ∈ intersperse sep l
Tactic:
match l with
| [] => simp only [not_mem_nil] at h
| [a] => simp_all only [mem_singleton, intersperse]
| head::mid::tail =>
  simp only [intersperse, mem_cons]
  simp at h
  rcases h with h |m |t <;> simp_all
  . right; right; apply mem_intersperse_of_mem; simp only [mem_cons, true_or]
  . right; right; apply mem_intersperse_of_mem; simp only [t, mem_cons, or_true]
Proof state after:
no goals
Theorem: List.mem_intersperse_of_mem
Proof state before:
α✝ : Type u_1
a : α✝
l : List α✝
sep : α✝
h : a ∈ []
⊢ a ∈ intersperse sep []
Tactic:
simp only [not_mem_nil] at h
Proof state after:
no goals
Theorem: List.mem_intersperse_of_mem
Proof state before:
α✝ : Type u_1
a✝ : α✝
l : List α✝
sep a : α✝
h : a✝ ∈ [a]
⊢ a✝ ∈ intersperse sep [a]
Tactic:
simp_all only [mem_singleton, intersperse]
Proof state after:
no goals
Theorem: List.mem_intersperse_of_mem
Proof state before:
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
h : a ∈ head :: mid :: tail
⊢ a ∈ intersperse sep (head :: mid :: tail)
Tactic:
simp only [intersperse, mem_cons]
Proof state after:
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
h : a ∈ head :: mid :: tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Theorem: List.mem_intersperse_of_mem
Proof state before:
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
h : a ∈ head :: mid :: tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Tactic:
simp at h
Proof state after:
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
h : a = head ∨ a = mid ∨ a ∈ tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Theorem: List.mem_intersperse_of_mem
Proof state before:
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
h : a = head ∨ a = mid ∨ a ∈ tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Tactic:
rcases h with h |m |t <;> simp_all
Proof state after:
case inr.inl
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
m : a = mid
⊢ mid = head ∨ mid = sep ∨ mid ∈ intersperse sep (mid :: tail)

case inr.inr
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
t : a ∈ tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Theorem: List.mem_intersperse_of_mem
Proof state before:
case inr.inl
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
m : a = mid
⊢ mid = head ∨ mid = sep ∨ mid ∈ intersperse sep (mid :: tail)

case inr.inr
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
t : a ∈ tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Tactic:
. right; right; apply mem_intersperse_of_mem; simp only [mem_cons, true_or]
Proof state after:
case inr.inr
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
t : a ∈ tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Theorem: List.mem_intersperse_of_mem
Proof state before:
case inr.inr
α✝ : Type u_1
a : α✝
l : List α✝
sep head mid : α✝
tail : List α✝
t : a ∈ tail
⊢ a = head ∨ a = sep ∨ a ∈ intersperse sep (mid :: tail)
Tactic:
. right; right; apply mem_intersperse_of_mem; simp only [t, mem_cons, or_true]
Proof state after:
no goals
Theorem: List.mem_intercalate
Proof state before:
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : a ∈ intercalate delim l
⊢ a ∈ delim ∨ ∃ e, e ∈ l ∧ a ∈ e
Tactic:
simp only [intercalate, mem_join] at h
Proof state after:
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
⊢ a ∈ delim ∨ ∃ e, e ∈ l ∧ a ∈ e
Theorem: List.mem_intercalate
Proof state before:
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
⊢ a ∈ delim ∨ ∃ e, e ∈ l ∧ a ∈ e
Tactic:
have ⟨e, ein, ain⟩ := h
Proof state after:
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
e : List α✝
ein : e ∈ intersperse delim l
ain : a ∈ e
⊢ a ∈ delim ∨ ∃ e, e ∈ l ∧ a ∈ e
Theorem: List.mem_intercalate
Proof state before:
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
e : List α✝
ein : e ∈ intersperse delim l
ain : a ∈ e
⊢ a ∈ delim ∨ ∃ e, e ∈ l ∧ a ∈ e
Tactic:
cases List.mem_intersperse ein with
| inl heq =>
  simp only [← heq, ain, true_or]
| inr heq =>
  right
  exists e
Proof state after:
no goals
Theorem: List.mem_intercalate
Proof state before:
case inl
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
e : List α✝
ein : e ∈ intersperse delim l
ain : a ∈ e
heq : e = delim
⊢ a ∈ delim ∨ ∃ e, e ∈ l ∧ a ∈ e
Tactic:
simp only [← heq, ain, true_or]
Proof state after:
no goals
Theorem: List.mem_intercalate
Proof state before:
case inr
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
e : List α✝
ein : e ∈ intersperse delim l
ain : a ∈ e
heq : e ∈ l
⊢ a ∈ delim ∨ ∃ e, e ∈ l ∧ a ∈ e
Tactic:
right
Proof state after:
case inr.h
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
e : List α✝
ein : e ∈ intersperse delim l
ain : a ∈ e
heq : e ∈ l
⊢ ∃ e, e ∈ l ∧ a ∈ e
Theorem: List.mem_intercalate
Proof state before:
case inr.h
α✝ : Type u_1
a : α✝
delim : List α✝
l : List (List α✝)
h : ∃ l_1, l_1 ∈ intersperse delim l ∧ a ∈ l_1
e : List α✝
ein : e ∈ intersperse delim l
ain : a ∈ e
heq : e ∈ l
⊢ ∃ e, e ∈ l ∧ a ∈ e
Tactic:
exists e
Proof state after:
no goals
Theorem: List.mem_intercalate_of_mem
Proof state before:
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ intercalate delim l
Tactic:
rw [intercalate]
Proof state after:
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ join (intersperse delim l)
Theorem: List.mem_intercalate_of_mem
Proof state before:
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ join (intersperse delim l)
Tactic:
apply mem_join_of_mem
Proof state after:
case lL
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ ?l ∈ intersperse delim l

case al
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ ?l

case l
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ List α✝
Theorem: List.mem_intercalate_of_mem
Proof state before:
case lL
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ ?l ∈ intersperse delim l

case al
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ ?l

case l
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ List α✝
Tactic:
apply mem_intersperse_of_mem
Proof state after:
case lL.h
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ ?l ∈ l

case al
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ ?l

case l
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ List α✝
Theorem: List.mem_intercalate_of_mem
Proof state before:
case lL.h
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ ?l ∈ l

case al
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ ?l

case l
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ List α✝
Tactic:
apply h₂
Proof state after:
case al
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ e
Theorem: List.mem_intercalate_of_mem
Proof state before:
case al
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ e
Tactic:
apply h₁
Proof state after:
no goals
Theorem: List.join_eq_nil
Proof state before:
α✝ : Type u_1
l : List (List α✝)
h : join l = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Tactic:
induction l with
| nil =>
  simp only [not_mem_nil, IsEmpty.forall_iff, forall_const]
| cons head tail ih=>
  simp_all only [join, append_eq_nil, mem_cons, forall_eq_or_imp, true_and, forall_true_left]
  apply ih
Proof state after:
no goals
Theorem: List.join_eq_nil
Proof state before:
case nil
α✝ : Type u_1
h : join [] = []
⊢ ∀ (e : List α✝), e ∈ [] → e = []
Tactic:
simp only [not_mem_nil, IsEmpty.forall_iff, forall_const]
Proof state after:
no goals
Theorem: List.join_eq_nil
Proof state before:
case cons
α✝ : Type u_1
head : List α✝
tail : List (List α✝)
ih : join tail = [] → ∀ (e : List α✝), e ∈ tail → e = []
h : join (head :: tail) = []
⊢ ∀ (e : List α✝), e ∈ head :: tail → e = []
Tactic:
simp_all only [join, append_eq_nil, mem_cons, forall_eq_or_imp, true_and, forall_true_left]
Proof state after:
case cons
α✝ : Type u_1
head : List α✝
tail : List (List α✝)
ih : ∀ (e : List α✝), e ∈ tail → e = []
h : head = [] ∧ join tail = []
⊢ ∀ (a : List α✝), a ∈ tail → a = []
Theorem: List.join_eq_nil
Proof state before:
case cons
α✝ : Type u_1
head : List α✝
tail : List (List α✝)
ih : ∀ (e : List α✝), e ∈ tail → e = []
h : head = [] ∧ join tail = []
⊢ ∀ (a : List α✝), a ∈ tail → a = []
Tactic:
apply ih
Proof state after:
no goals
Theorem: List.intercalate_eq_nil
Proof state before:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : intercalate delim l = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Tactic:
rw [intercalate] at h
Proof state after:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Theorem: List.intercalate_eq_nil
Proof state before:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Tactic:
have all_nil := join_eq_nil h
Proof state after:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
all_nil : ∀ (e : List α✝), e ∈ intersperse delim l → e = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Theorem: List.intercalate_eq_nil
Proof state before:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
all_nil : ∀ (e : List α✝), e ∈ intersperse delim l → e = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Tactic:
intro e ein
Proof state after:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
all_nil : ∀ (e : List α✝), e ∈ intersperse delim l → e = []
e : List α✝
ein : e ∈ l
⊢ e = []
Theorem: List.intercalate_eq_nil
Proof state before:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
all_nil : ∀ (e : List α✝), e ∈ intersperse delim l → e = []
e : List α✝
ein : e ∈ l
⊢ e = []
Tactic:
apply all_nil
Proof state after:
case a
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
all_nil : ∀ (e : List α✝), e ∈ intersperse delim l → e = []
e : List α✝
ein : e ∈ l
⊢ e ∈ intersperse delim l
Theorem: List.intercalate_eq_nil
Proof state before:
case a
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
all_nil : ∀ (e : List α✝), e ∈ intersperse delim l → e = []
e : List α✝
ein : e ∈ l
⊢ e ∈ intersperse delim l
Tactic:
apply mem_intersperse_of_mem ein
Proof state after:
no goals
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
⊢ l ≠ []
Tactic:
intro contr
Proof state after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ False
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ False
Tactic:
apply h₂
Proof state after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim l = []
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim l = []
Tactic:
rw [contr]
Proof state after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim [] = []
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim [] = []
Tactic:
simp only [intercalate._eq_1, join]
Proof state after:
no goals
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
⊢ getLast l (_ : l = [] → False) ≠ []
Tactic:
intro contr
Proof state after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ False
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ False
Tactic:
apply not_nil
Proof state after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some []
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some []
Tactic:
rw[←contr]
Proof state after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some (getLast l (_ : l = [] → False))
Theorem: List.getLast_intercalate
Proof state before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some (getLast l (_ : l = [] → False))
Tactic:
apply List.getLast?_eq_getLast
Proof state after:
no goals
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
⊢ getLast (intercalate delim l) h₂ =
    getLast (getLast l (_ : l = [] → False)) (_ : getLast l (_ : l = [] → False) = [] → False)
Tactic:
match l with
| [] => simp only [intercalate._eq_1, join, ne_eq, not_true] at h₂
| [a] =>
  simp [intercalate]
| [a,b] =>
  simp [intercalate]
  simp [← intercalate._eq_1]
  simp only [← append_assoc]
  rw [getLast_append']
| head::mid::mid₂::tail =>
  simp [intercalate]
  simp [← intercalate._eq_1]
  simp only [← append_assoc]
  rw [getLast_append', getLast_intercalate (mid₂::tail)]
  . intro contr
    apply not_nil
    rw [List.getLast?_eq_getLast]
    simp only [ne_eq, not_false_iff, getLast_cons, Option.some.injEq]
    generalize_proofs hp
    apply List.intercalate_eq_nil contr (getLast (mid₂ :: tail) hp)
    apply List.getLast_mem
    simp only [ne_eq, not_false_iff]
  . intro contr
    apply not_nil
    simp only [getLast?_cons_cons, contr]
  . exact a
Proof state after:
no goals
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim [] ≠ []
not_nil : getLast? [] ≠ some []
⊢ getLast (intercalate delim []) h₂ =
    getLast (getLast [] (_ : [] = [] → False)) (_ : getLast [] (_ : [] = [] → False) = [] → False)
Tactic:
simp only [intercalate._eq_1, join, ne_eq, not_true] at h₂
Proof state after:
no goals
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a : List α
h₂ : intercalate delim [a] ≠ []
not_nil : getLast? [a] ≠ some []
⊢ getLast (intercalate delim [a]) h₂ =
    getLast (getLast [a] (_ : [a] = [] → False)) (_ : getLast [a] (_ : [a] = [] → False) = [] → False)
Tactic:
simp [intercalate]
Proof state after:
no goals
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (intercalate delim [a, b]) h₂ =
    getLast (getLast [a, b] (_ : [a, b] = [] → False)) (_ : getLast [a, b] (_ : [a, b] = [] → False) = [] → False)
Tactic:
simp [intercalate]
Proof state after:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ (delim ++ b)) (_ : a ++ (delim ++ b) ≠ []) = getLast b (_ : b ≠ [])
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ (delim ++ b)) (_ : a ++ (delim ++ b) ≠ []) = getLast b (_ : b ≠ [])
Tactic:
simp only [← append_assoc]
Proof state after:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ delim ++ b) (_ : a ++ delim ++ b ≠ []) = getLast b (_ : b ≠ [])
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ delim ++ b) (_ : a ++ delim ++ b ≠ []) = getLast b (_ : b ≠ [])
Tactic:
rw [getLast_append']
Proof state after:
no goals