-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_some_of_destruct_tail_some {s : WSeq α} {a} (h : some a ∈ destruct (tail s)) :
    ∃ a', some a' ∈ destruct s

Proof state:
case intro.intro.intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
rcases t' with - | t' <;> rw [← ht2] at td <;> simp only [destruct_nil] at td

Result:
case intro.intro.intro.intro.none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
⊢ ∃ a', some a' ∈ s.destruct

case intro.intro.intro.intro.some
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ t'.snd.destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct

Proof state:
case intro.intro.intro.intro.some
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ t'.snd.destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
exact ⟨_, ht'⟩

Result:
no goals

Proof state:
α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct >>= destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
rcases exists_of_mem_bind h with ⟨t, tm, td⟩

Result:
case intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct >>= destruct
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
⊢ ∃ a', some a' ∈ s.destruct

Proof state:
α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ (flatten (Applicative.toFunctor.1 (fun o => Option.recOn o nil Prod.snd) s.destruct)).destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
simp only [destruct_flatten] at h

Result:
α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct >>= destruct
⊢ ∃ a', some a' ∈ s.destruct

Proof state:
α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ s.tail.destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
unfold tail Functor.map at h

Result:
α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ (flatten (Applicative.toFunctor.1 (fun o => Option.recOn o nil Prod.snd) s.destruct)).destruct
⊢ ∃ a', some a' ∈ s.destruct

Proof state:
case intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
rcases Computation.exists_of_mem_map tm with ⟨t', ht', ht2⟩

Result:
case intro.intro.intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ s.destruct

Proof state:
case intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct >>= destruct
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
clear h

Result:
case intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
⊢ ∃ a', some a' ∈ s.destruct

Proof state:
case intro.intro.intro.intro.none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
have := mem_unique td (ret_mem _)

Result:
case intro.intro.intro.intro.none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
this : some a = none
⊢ ∃ a', some a' ∈ s.destruct

Proof state:
case intro.intro.intro.intro.none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
this : some a = none
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
contradiction

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
clear tm

Result:
case intro.intro.intro.intro
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ s.destruct