case a
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ↑(toSeq ↑s) = ↑s
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ toSeq ↑s = s
apply Subtype.eq
case a.h
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ ↑(toSeq ↑s) n = ↑s n
case a
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ↑(toSeq ↑s) = ↑s
funext n
case a.h
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ Computation.get (get? (↑s) n) = ↑s n
case a.h
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ ↑(toSeq ↑s) n = ↑s n
dsimp [toSeq]
case a.h.a
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ ↑s n ∈ get? (↑s) n
case a.h
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ Computation.get (get? (↑s) n) = ↑s n
apply get_eq_of_mem
case a.h.a
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ ↑s n ∈ Computation.pure (Seq.get? s n)
case a.h.a
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ ↑s n ∈ get? (↑s) n
rw [get?_ofSeq]
no goals
case a.h.a
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ ↑s n ∈ Computation.pure (Seq.get? s n)
apply ret_mem