-- Mathlib/Data/Seq/WSeq.lean
theorem exists_get?_of_mem {s : WSeq α} {a} (h : a ∈ s) : ∃ n, some a ∈ get? s n

Proof state:
case h2
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
h : ∃ n, some a ∈ s'.get? n
⊢ ∃ n, some a ∈ s'.think.get? n

Tactic:
obtain ⟨n, h⟩ := h

Result:
case h2.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ ∃ n, some a ∈ s'.think.get? n

Proof state:
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∃ n, some a ∈ s.get? n

Tactic:
apply mem_rec_on h

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

case h2
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (s : WSeq α), (∃ n, some a ∈ s.get? n) → ∃ n, some a ∈ s.think.get? n

Proof state:
case h1
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a' ∨ ∃ n, some a ∈ s'.get? n
⊢ ∃ n, some a ∈ (cons a' s').get? n

Tactic:
rcases h with h | h

Result:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ ∃ n, some a ∈ (cons a' s').get? n

case h1.inr
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : ∃ n, some a ∈ s'.get? n
⊢ ∃ n, some a ∈ (cons a' s').get? n

Proof state:
case h2.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ s'.think.get? n

Tactic:
simp only [get?, dropn_think, head_think]

Result:
case h2.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (s'.drop n).head.think

Proof state:
case h1
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ n, some a ∈ s'.get? n) → ∃ n, some a ∈ (cons b s').get? n

Tactic:
intro a' s' h

Result:
case h1
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a' ∨ ∃ n, some a ∈ s'.get? n
⊢ ∃ n, some a ∈ (cons a' s').get? n

Proof state:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ ∃ n, some a ∈ (cons a' s').get? n

Tactic:
exists 0

Result:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ (cons a' s').get? 0

Proof state:
case h2.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (s'.drop n).head.think

Tactic:
apply think_mem h

Result:
no goals

Proof state:
case h2.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ ∃ n, some a ∈ s'.think.get? n

Tactic:
exists n

Result:
case h2.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ s'.think.get? n

Proof state:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ (cons a' s').get? 0

Tactic:
simp only [get?, drop, head_cons]

Result:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ Computation.pure (some a')

Proof state:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ Computation.pure (some a')

Tactic:
rw [h]

Result:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a' ∈ Computation.pure (some a')

Proof state:
case h2
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (s : WSeq α), (∃ n, some a ∈ s.get? n) → ∃ n, some a ∈ s.think.get? n

Tactic:
intro s' h

Result:
case h2
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
h : ∃ n, some a ∈ s'.get? n
⊢ ∃ n, some a ∈ s'.think.get? n

Proof state:
case h1.inr.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (cons a' s').get? (n + 1)

Tactic:
simpa [get?]

Result:
no goals

Proof state:
case h1.inr.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ ∃ n, some a ∈ (cons a' s').get? n

Tactic:
exists n + 1

Result:
case h1.inr.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (cons a' s').get? (n + 1)

Proof state:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a' ∈ Computation.pure (some a')

Tactic:
apply ret_mem

Result:
no goals

Proof state:
case h1.inr
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : ∃ n, some a ∈ s'.get? n
⊢ ∃ n, some a ∈ (cons a' s').get? n

Tactic:
obtain ⟨n, h⟩ := h

Result:
case h1.inr.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ ∃ n, some a ∈ (cons a' s').get? n