Theorem: List.mem_intercalate (One.lean)

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
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

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
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

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
State after:
no goals

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]
State after:
no goals

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
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

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
State after:
no goals