rw [mem']
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ (1, 0)