α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
h : some a ∈ destruct (flatten (Applicative.toFunctor.1 (fun o => Option.recOn o nil Prod.snd) (destruct s)))
⊢ ∃ a', some a' ∈ destruct s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
h : some a ∈ destruct (tail s)
⊢ ∃ a', some a' ∈ destruct s
unfold tail Functor.map at h
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s) >>= destruct
⊢ ∃ a', some a' ∈ destruct s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
h : some a ∈ destruct (flatten (Applicative.toFunctor.1 (fun o => Option.recOn o nil Prod.snd) (destruct s)))
⊢ ∃ a', some a' ∈ destruct s
simp at h
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s) >>= destruct
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
td : some a ∈ destruct t
⊢ ∃ a', some a' ∈ destruct s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s) >>= destruct
⊢ ∃ a', some a' ∈ destruct s
rcases exists_of_mem_bind h with ⟨t, tm, td⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
td : some a ∈ destruct t
⊢ ∃ a', some a' ∈ destruct s
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s) >>= destruct
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
td : some a ∈ destruct t
⊢ ∃ a', some a' ∈ destruct s
clear h
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
td : some a ∈ destruct t
t' : Option (α × WSeq α)
ht' : t' ∈ destruct s
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ destruct s
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
td : some a ∈ destruct t
⊢ ∃ a', some a' ∈ destruct s
rcases Computation.exists_of_mem_map tm with ⟨t', ht', ht2⟩
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ destruct t
t' : Option (α × WSeq α)
ht' : t' ∈ destruct s
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ destruct s
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
td : some a ∈ destruct t
t' : Option (α × WSeq α)
ht' : t' ∈ destruct s
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ destruct s
clear tm
case intro.intro.intro.intro.none
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ destruct s
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
⊢ ∃ a', some a' ∈ destruct s

case intro.intro.intro.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ destruct t'.snd
ht' : some t' ∈ destruct s
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ destruct s
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ destruct t
t' : Option (α × WSeq α)
ht' : t' ∈ destruct s
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ destruct s
cases' t' with t' <;> rw [← ht2] at td <;> simp at td
case intro.intro.intro.intro.none
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ destruct s
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
this : some a = none
⊢ ∃ a', some a' ∈ destruct s
case intro.intro.intro.intro.none
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ destruct s
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
⊢ ∃ a', some a' ∈ destruct s
have := mem_unique td (ret_mem _)
no goals
case intro.intro.intro.intro.none
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ destruct s
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
this : some a = none
⊢ ∃ a', some a' ∈ destruct s
contradiction
no goals
case intro.intro.intro.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ destruct t'.snd
ht' : some t' ∈ destruct s
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ destruct s
exact ⟨_, ht'⟩