Theorem: List.intercalate_eq_nil (One.lean)

State before:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : intercalate delim l = []
⊢ ∀ (e : List α✝), e ∈ l → e = []
Tactic:
rw [intercalate] at h
State after:
α✝ : Type u_1
delim : List α✝
l : List (List α✝)
h : join (intersperse delim l) = []
⊢ ∀ (e : List α✝), e ∈ l → e = []

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
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 = []

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
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 = []

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

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