intros mem i hle0i hlei1
case mpr
x : ℝ × ℝ
⊢ x ∈ Set.singleton (1, 0) → ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)