Theorem: List.mem_intersperse_of_mem (One.lean)

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

State before:
α✝ : Type u_1
a : α✝
l : List α✝
sep : α✝
h : a ∈ []
⊢ a ∈ intersperse sep []
Tactic:
simp only [not_mem_nil] at h
State after:
no goals

State before:
α✝ : Type u_1
a✝ : α✝
l : List α✝
sep a : α✝
h : a✝ ∈ [a]
⊢ a✝ ∈ intersperse sep [a]
Tactic:
simp_all only [mem_singleton, intersperse]
State after:
no goals

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

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

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

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

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