simp only [sq_le_one_iff_abs_le_one, abs_le] at h
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : (-1 ≤ p.1 ∧ p.1 ≤ 1) ∧ -1 ≤ p.2 ∧ p.2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)