case h
α : Type u_1
β : Type ?u.905
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ x ∈ {x | x ∈ l}
α : Type u_1
β : Type ?u.905
l : List α
⊢ (range fun k => nthLe l ↑k (_ : ↑k < length l)) = {x | x ∈ l}
ext x
case h
α : Type u_1
β : Type ?u.905
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ ∃ n, List.get l n = x
case h
α : Type u_1
β : Type ?u.905
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ x ∈ {x | x ∈ l}
rw [mem_setOf_eq, mem_iff_get]
no goals
case h
α : Type u_1
β : Type ?u.905
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ ∃ n, List.get l n = x
exact ⟨fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩, fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩⟩