Theorem: List.mem_intersperse (One.lean)

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

State before:
α✝ : Type u_1
a sep : α✝
l : List α✝
h : a ∈ intersperse sep []
⊢ a = sep ∨ a ∈ []
Tactic:
rw [intersperse] at h
State after:
α✝ : Type u_1
a sep : α✝
l : List α✝
h : a ∈ []
⊢ a = sep ∨ a ∈ []

State before:
α✝ : Type u_1
a sep : α✝
l : List α✝
h : a ∈ []
⊢ a = sep ∨ a ∈ []
Tactic:
contradiction
State after:
no goals

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
State after:
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a = sep ∨ a ∈ [single]

State before:
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a = sep ∨ a ∈ [single]
Tactic:
right
State after:
case h
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a ∈ [single]

State before:
case h
α✝ : Type u_1
a sep : α✝
l : List α✝
single : α✝
h : a = single
⊢ a ∈ [single]
Tactic:
simp only [h, mem_singleton]
State after:
no goals

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

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

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

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

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

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