no goals
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
n : ℕ
h : some a ∈ get? s n
⊢ ∃ a', some a' ∈ head s
induction n generalizing a with
| zero => exact ⟨_, h⟩
| succ n IH =>
    let ⟨a', h'⟩ := head_some_of_head_tail_some h
    exact IH h'
no goals
case zero
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : some a ∈ get? s Nat.zero
⊢ ∃ a', some a' ∈ head s
exact ⟨_, h⟩
case succ
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ get? s n → ∃ a', some a' ∈ head s
a : α
h : some a ∈ get? s (Nat.succ n)
a' : α
h' : some a' ∈ head (drop s n)
⊢ ∃ a', some a' ∈ head s
case succ
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ get? s n → ∃ a', some a' ∈ head s
a : α
h : some a ∈ get? s (Nat.succ n)
⊢ ∃ a', some a' ∈ head s
let ⟨a', h'⟩ := head_some_of_head_tail_some h
no goals
case succ
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ get? s n → ∃ a', some a' ∈ head s
a : α
h : some a ∈ get? s (Nat.succ n)
a' : α
h' : some a' ∈ head (drop s n)
⊢ ∃ a', some a' ∈ head s
exact IH h'