α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ head (drop (↑s) n) = Computation.pure (Seq.get? s n)
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ get? (↑s) n = Computation.pure (Seq.get? s n)
dsimp [get?]
no goals
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ head (drop (↑s) n) = Computation.pure (Seq.get? s n)
rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]