-- Mathlib/Data/Seq/WSeq.lean
theorem exists_dropn_of_mem {s : WSeq α} {a} (h : a ∈ s) :
    ∃ n s', some (a, s') ∈ destruct (drop s n) :=
  let ⟨n, h⟩ := exists_get?_of_mem h
  ⟨n, by
    rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩
    have := Computation.mem_unique (Computation.mem_map _ om) h
    rcases o with - | o
    · injection this
    injection this with i
    obtain ⟨a', s'⟩ := o
    dsimp at i
    rw [i] at om
    exact ⟨_, om⟩⟩

Proof state:
case mk.intro.some.mk
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a, s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
exact ⟨_, om⟩

Result:
no goals

Proof state:
case mk.intro.none
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
om : none ∈ (s.drop n).destruct
this : Prod.fst <$> none = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
injection this

Result:
no goals

Proof state:
case mk.intro.some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : α × WSeq α
om : some o ∈ (s.drop n).destruct
this : Prod.fst <$> some o = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
injection this with i

Result:
case mk.intro.some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : α × WSeq α
om : some o ∈ (s.drop n).destruct
i : o.fst = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Proof state:
case mk.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
this : Prod.fst <$> o = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
rcases o with - | o

Result:
case mk.intro.none
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
om : none ∈ (s.drop n).destruct
this : Prod.fst <$> none = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

case mk.intro.some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : α × WSeq α
om : some o ∈ (s.drop n).destruct
this : Prod.fst <$> some o = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Proof state:
case mk.intro.some.mk
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : (a', s').fst = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
dsimp at i

Result:
case mk.intro.some.mk
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Proof state:
case mk.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
have := Computation.mem_unique (Computation.mem_map _ om) h

Result:
case mk.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
this : Prod.fst <$> o = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Proof state:
case mk.intro.some.mk
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
rw [i] at om

Result:
case mk.intro.some.mk
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a, s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Proof state:
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩

Result:
case mk.intro
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Proof state:
case mk.intro.some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : α × WSeq α
om : some o ∈ (s.drop n).destruct
i : o.fst = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
obtain ⟨a', s'⟩ := o

Result:
case mk.intro.some.mk
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : (a', s').fst = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct