problem

Stream: mathlib4

[BANGJI HU]

import Mathlib.Data.Real.Cardinality
import Mathlib



theorem problem5 {x y : ℝ} (h1 : 2 ≤ x ∨ 2 ≤ y) (h2 : x ^ 2 + y ^ 2 = 4) :
    x ^ 2 * y ^ 2 = 0 := by
  apply le_antisymm
  obtain h1 | h2 := h1
  have h3 :=
  calc
    x ^ 2 = 4 - y^2 := by rw [ h2]
    _ = 4 - 0^2 := by rw [h2]
    _ ≥ 4 := by rw [h2]
  cancel 2 at h3
  calc
    y ^ 2 = 4 - x^2 := by ring
    _ = 4 - 0^2 := by rw[h1]
    _ ≥ 4 := by numbers
  cancel 2 at h3

[Heather Macbeth]

Hi @hand bob, could you please

1. not double-post
2. not ask about homework problems from my current course until the week after they are due?

[Kim Morrison]

Also, make sure to give context, explaining what you need help with, and asking a question, not just posting a blob of code. :-)