simple problem

Stream: new members

[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

[BANGJI HU]

seem to be some mistake

[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?

[Heather Macbeth]

(I'm not sure how you encountered this problem, but it did not exist on the internet until 5 days ago when I made it up for my homework.)

[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]
  simp only [ge_iff_le]
  calc
    y ^ 2 = 4 - x^2 := by ring
    _ = 4 - 0^2 := by rw[h1]
    _ ≥ 4 := by

[BANGJI HU]

can you give me some hint

[BANGJI HU]

@Heather Macbeth

[Heather Macbeth]

@hand bob If you are one of my students, please email me directly! If not, please wait a few days, and then post here again (and explain your question more precisely).