case zero
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ head (drop s Nat.zero) = get? s Nat.zero

case succ
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
n : ℕ
IH : ∀ (s : Seq α), head (drop s n) = get? s n
s : Seq α
⊢ head (drop s (Nat.succ n)) = get? s (Nat.succ n)
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ head (drop s n) = get? s n
induction' n with n IH generalizing s
case succ
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
n : ℕ
IH : ∀ (s : Seq α), head (drop s n) = get? s n
s : Seq α
⊢ head (drop (tail s) n) = get? (tail s) n
case succ
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
n : ℕ
IH : ∀ (s : Seq α), head (drop s n) = get? s n
s : Seq α
⊢ head (drop s (Nat.succ n)) = get? s (Nat.succ n)
rw [Nat.succ_eq_add_one, ← get?_tail, ← dropn_tail]
no goals
case succ
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
n : ℕ
IH : ∀ (s : Seq α), head (drop s n) = get? s n
s : Seq α
⊢ head (drop (tail s) n) = get? (tail s) n
apply IH
no goals
case zero
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ head (drop s Nat.zero) = get? s Nat.zero
rfl