case h1
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ n, some a ∈ get? s' n) → ∃ n, some a ∈ get? (cons b s') n

case h2
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (s : WSeq α), (∃ n, some a ∈ get? s n) → ∃ n, some a ∈ get? (think s) n
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : a ∈ s
⊢ ∃ n, some a ∈ get? s n
apply mem_rec_on h
case h1
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a' ∨ ∃ n, some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (cons a' s') n
case h1
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ n, some a ∈ get? s' n) → ∃ n, some a ∈ get? (cons b s') n
intro a' s' h
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ ∃ n, some a ∈ get? (cons a' s') n

case h1.inr
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : ∃ n, some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (cons a' s') n
case h1
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a' ∨ ∃ n, some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (cons a' s') n
cases' h with h h
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ get? (cons a' s') 0
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ ∃ n, some a ∈ get? (cons a' s') n
exists 0
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ Computation.pure (some a')
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ get? (cons a' s') 0
simp only [get?, drop, head_cons]
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a' ∈ Computation.pure (some a')
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ Computation.pure (some a')
rw [h]
no goals
case h1.inl
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a' ∈ Computation.pure (some a')
apply ret_mem
case h1.inr.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (cons a' s') n
case h1.inr
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : ∃ n, some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (cons a' s') n
cases' h with n h
case h1.inr.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ some a ∈ get? (cons a' s') (n + 1)
case h1.inr.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (cons a' s') n
exists n + 1
no goals
case h1.inr.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ some a ∈ get? (cons a' s') (n + 1)
simpa [get?]
case h2
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
h : ∃ n, some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (think s') n
case h2
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (s : WSeq α), (∃ n, some a ∈ get? s n) → ∃ n, some a ∈ get? (think s) n
intro s' h
case h2.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (think s') n
case h2
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
h : ∃ n, some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (think s') n
cases' h with n h
case h2.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ some a ∈ get? (think s') n
case h2.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ ∃ n, some a ∈ get? (think s') n
exists n
case h2.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ some a ∈ Computation.think (head (drop s' n))
case h2.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ some a ∈ get? (think s') n
simp [get?]
no goals
case h2.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ get? s' n
⊢ some a ∈ Computation.think (head (drop s' n))
apply think_mem h