rw [← this] at h ⊢
case mp
x : ℕ
r : Range
h : x ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, x = r.get i
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, r.nth (r.ofNth x) = r.get i