have mem' := Set.eq_of_mem_singleton mem
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)