Theorem: List.mem_intercalate_of_mem (One.lean)

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]
State after:
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ join (intersperse delim l)

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

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

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₂
State after:
case al
α✝ : Type u_1
a : α✝
e : List α✝
l : List (List α✝)
delim : List α✝
h₁ : a ∈ e
h₂ : e ∈ l
⊢ a ∈ e

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