ι : Type ?u.106668
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : Fin (length l)
x : α
⊢ get l n = x ↔ ∃ h, get l { val := ↑n, isLt := h } = x
ι : Type ?u.106668
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : Fin (length l)
x : α
⊢ get l n = x ↔ get? l ↑n = some x
rw [get?_eq_some]
no goals
ι : Type ?u.106668
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : Fin (length l)
x : α
⊢ get l n = x ↔ ∃ h, get l { val := ↑n, isLt := h } = x
simp [n.2]