α : Type u_1
β : Type ?u.1563
l : List α
⊢ range (get? l) = insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))
α : Type u_1
β : Type ?u.1563
l : List α
⊢ range (get? l) = insert none (some '' {x | x ∈ l})
rw [← range_list_nthLe, ← range_comp]
case refine'_1
α : Type u_1
β : Type ?u.1563
l : List α
n : ℕ
⊢ get? l n ∈ insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))

case refine'_2
α : Type u_1
β : Type ?u.1563
l : List α
⊢ none ∈ range (get? l)

case refine'_3
α : Type u_1
β : Type ?u.1563
l : List α
⊢ range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)) ⊆ range (get? l)
α : Type u_1
β : Type ?u.1563
l : List α
⊢ range (get? l) = insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))
refine' (range_subset_iff.2 fun n => _).antisymm (insert_subset.2 ⟨_, _⟩)
no goals
case refine'_1
α : Type u_1
β : Type ?u.1563
l : List α
n : ℕ
⊢ get? l n ∈ insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))

case refine'_2
α : Type u_1
β : Type ?u.1563
l : List α
⊢ none ∈ range (get? l)

case refine'_3
α : Type u_1
β : Type ?u.1563
l : List α
⊢ range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)) ⊆ range (get? l)
exacts [(le_or_lt l.length n).imp get?_eq_none.2 (fun hlt => ⟨⟨_, hlt⟩, (get?_eq_get hlt).symm⟩),
  ⟨_, get?_eq_none.2 le_rfl⟩, range_subset_iff.2 <| fun k => ⟨_, get?_eq_get _⟩]