no goals
ι : Type ?u.450946
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
i : Fin (length (enumFrom n l))
⊢ ↑i < length l
simpa [length_enumFrom] using i.2
ι : Type ?u.450946
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
i : Fin (length (enumFrom n l))
hi : optParam (↑i < length l) (_ : ↑i < length l)
⊢ get? (enumFrom n l) ↑i = some (n + ↑i, get l { val := ↑i, isLt := hi })
ι : Type ?u.450946
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
i : Fin (length (enumFrom n l))
hi : optParam (↑i < length l) (_ : ↑i < length l)
⊢ get (enumFrom n l) i = (n + ↑i, get l { val := ↑i, isLt := hi })
rw [← Option.some_inj, ← get?_eq_get]
no goals
ι : Type ?u.450946
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
i : Fin (length (enumFrom n l))
hi : optParam (↑i < length l) (_ : ↑i < length l)
⊢ get? (enumFrom n l) ↑i = some (n + ↑i, get l { val := ↑i, isLt := hi })
simp [enumFrom_get?, get?_eq_get hi]