-- Mathlib/Data/Seq/WSeq.lean
theorem eq_or_mem_iff_mem {s : WSeq α} {a a' s'} :
    some (a', s') ∈ destruct s → (a ∈ s ↔ a = a' ∨ a ∈ s')

Proof state:
case h1.h2.intro
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'

Tactic:
rw [i1, i2]

Result:
case h1.h2.intro
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'

Proof state:
α : Type u
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (a', ⟨f, al⟩) ∈ c
m : (cons x s).destruct = Computation.pure (some (a', ⟨f, al⟩))
i2 : s = ⟨f, al⟩
⊢ a = a' ↔ some (some a) = some (some a')

Tactic:
simp

Result:
no goals

Proof state:
case h1.h2.intro.mk
α : Type u
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (a', ⟨f, al⟩) ∈ c
m : (cons x s).destruct = Computation.pure (some (a', ⟨f, al⟩))
i2 : s = ⟨f, al⟩
⊢ a ∈ cons a' ⟨f, al⟩ ↔ a = a' ∨ a ∈ ⟨f, al⟩

Tactic:
dsimp only [cons, Membership.mem, WSeq.Mem, Seq.Mem, Seq.cons]

Result:
case h1.h2.intro.mk
α : Type u
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (a', ⟨f, al⟩) ∈ c
m : (cons x s).destruct = Computation.pure (some (a', ⟨f, al⟩))
i2 : s = ⟨f, al⟩
⊢ Any (fun b => some (some a) = b) (some (some a') :: f) ↔ a = a' ∨ Any (fun b => some (some a) = b) f

Proof state:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
h : some (a', s') ∈ c
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'

Tactic:
revert s

Result:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')

Proof state:
case h1.h2.intro.mk.inr
α : Type u
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (a', ⟨f, al⟩) ∈ c
m✝ : (cons x s).destruct = Computation.pure (some (a', ⟨f, al⟩))
i2 : s = ⟨f, al⟩
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b => some (some a) = b) f
⊢ Any (fun b => some (some a) = b) (some (some a') :: f)

Tactic:
exact Stream'.mem_cons_of_mem _ m

Result:
no goals

Proof state:
case h1.h2
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
this : x = a' ∧ s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'

Tactic:
obtain ⟨i1, i2⟩ := this

Result:
case h1.h2.intro
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'

Proof state:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
⊢ some (a', s') ∈ c → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
intro h

Result:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
h : some (a', s') ∈ c
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'