-- Mathlib/Data/Seq/WSeq.lean
theorem mem_of_mem_tail {s : WSeq α} {a} : a ∈ tail s → a ∈ s

Proof state:
case intro.succ.h3.mk
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
val✝ : Stream' (Option (Option α))
property✝ : val✝.IsSeq
⊢ ↑(think ⟨val✝, property✝⟩) (n + 1) = ↑⟨val✝, property✝⟩ n

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s : WSeq α
a : α
h this : a ∈ s.tail
⊢ a ∈ s

Tactic:
obtain ⟨n, e⟩ := h

Result:
case intro
α : Type u
s : WSeq α
a : α
this : a ∈ s.tail
n : ℕ
e : some (some a) = (↑s.tail).get n
⊢ a ∈ s

Proof state:
case intro
α : Type u
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n → a ∈ s

Tactic:
simp only [Stream'.get]

Result:
case intro
α : Type u
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s

Proof state:
case intro.succ.h3
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
⊢ a ∈ s

Tactic:
apply IH m

Result:
case intro.succ.h3
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
⊢ some (some a) = ↑s.tail n

Proof state:
α : Type u
s : WSeq α
a : α
h : a ∈ s.tail
⊢ a ∈ s

Tactic:
have := h

Result:
α : Type u
s : WSeq α
a : α
h this : a ∈ s.tail
⊢ a ∈ s

Proof state:
case intro.zero.h2
α : Type u
a x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s 0
⊢ a = x ∨ a ∈ s

Tactic:
exact Or.inr m

Result:
no goals

Proof state:
case intro.succ.h3
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
⊢ ↑s.tail.think (n + 1) = ↑s.tail n

Tactic:
cases tail s

Result:
case intro.succ.h3.mk
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
val✝ : Stream' (Option (Option α))
property✝ : val✝.IsSeq
⊢ ↑(think ⟨val✝, property✝⟩) (n + 1) = ↑⟨val✝, property✝⟩ n

Proof state:
α : Type u
s : WSeq α
a : α
⊢ a ∈ s.tail → a ∈ s

Tactic:
intro h

Result:
α : Type u
s : WSeq α
a : α
h : a ∈ s.tail
⊢ a ∈ s

Proof state:
case intro.succ.h3
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
⊢ some (some a) = ↑s.tail n

Tactic:
rw [e]

Result:
case intro.succ.h3
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
⊢ ↑s.tail.think (n + 1) = ↑s.tail n

Proof state:
case intro.succ.h2
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s (n + 1)
⊢ a = x ∨ a ∈ s

Tactic:
exact Or.inr m

Result:
no goals

Proof state:
case intro
α : Type u
s : WSeq α
a : α
this : a ∈ s.tail
n : ℕ
e : some (some a) = (↑s.tail).get n
⊢ a ∈ s

Tactic:
revert s

Result:
case intro
α : Type u
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n → a ∈ s

Proof state:
case intro
α : Type u
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s

Tactic:
induction' n with n IH <;> intro s <;> induction' s using WSeq.recOn with x s s <;>
  simp <;> intro m e <;>
  injections

Result:
case intro.zero.h2
α : Type u
a x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s 0
⊢ a = x ∨ a ∈ s

case intro.succ.h2
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s (n + 1)
⊢ a = x ∨ a ∈ s

case intro.succ.h3
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = ↑s.tail n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = ↑s.tail.think (n + 1)
⊢ a ∈ s