-- Mathlib/Data/Seq/WSeq.lean
theorem get?_mem {s : WSeq α} {a n} : some a ∈ get? s n → a ∈ s

Proof state:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.tail.get? n → a ∈ s.tail
⊢ a ∈ s

Tactic:
rw [get?_tail] at this

Result:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.get? (n + 1) → a ∈ s.tail
⊢ a ∈ s

Proof state:
case zero
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
⊢ a ∈ s

Tactic:
dsimp only [get?, head] at h

Result:
case zero
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
⊢ a ∈ s

Proof state:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.get? (n + 1) → a ∈ s.tail
⊢ a ∈ s

Tactic:
exact mem_of_mem_tail (this h)

Result:
no goals

Proof state:
case zero.intro.intro.some
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> some o = some a
⊢ a ∈ s

Tactic:
injection h2 with h'

Result:
case zero.intro.intro.some
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h' : o.fst = a
⊢ a ∈ s

Proof state:
case zero.intro.intro
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
o : Option (α × WSeq α)
h1 : o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> o = some a
⊢ a ∈ s

Tactic:
rcases o with - | o

Result:
case zero.intro.intro.none
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
h1 : none ∈ (s.drop 0).destruct
h2 : Prod.fst <$> none = some a
⊢ a ∈ s

case zero.intro.intro.some
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> some o = some a
⊢ a ∈ s

Proof state:
case zero.intro.intro.some
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h' : o.fst = a
⊢ a ∈ s

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

Result:
case zero.intro.intro.some.mk
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
a' : α
s' : WSeq α
h1 : some (a', s') ∈ (s.drop 0).destruct
h' : (a', s').fst = a
⊢ a ∈ s

Proof state:
α : Type u
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s

Tactic:
induction' n with n IH <;> intro s h

Result:
case zero
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
⊢ a ∈ s

case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
⊢ a ∈ s

Proof state:
case zero
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
⊢ a ∈ s

Tactic:
rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩

Result:
case zero.intro.intro
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
o : Option (α × WSeq α)
h1 : o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> o = some a
⊢ a ∈ s

Proof state:
case zero.intro.intro.none
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
h1 : none ∈ (s.drop 0).destruct
h2 : Prod.fst <$> none = some a
⊢ a ∈ s

Tactic:
injection h2

Result:
no goals

Proof state:
case zero.intro.intro.some.mk
α : Type u
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop 0).destruct
a' : α
s' : WSeq α
h1 : some (a', s') ∈ (s.drop 0).destruct
h' : (a', s').fst = a
⊢ a ∈ s

Tactic:
exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)

Result:
no goals

Proof state:
α : Type u
s : WSeq α
a : α
n : ℕ
⊢ some a ∈ s.get? n → a ∈ s

Tactic:
revert s

Result:
α : Type u
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s

Proof state:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
⊢ a ∈ s

Tactic:
have := @IH (tail s)

Result:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.tail.get? n → a ∈ s.tail
⊢ a ∈ s