Missing constraint in amc12a_2013_p8

[albertqjiang]

https://github.com/openai/miniF2F/blob/18b1400db731999f6501ef777fc3c8b0e2e529f3/lean/src/valid.lean#L1130

theorem amc12a_2013_p8 (x y : ℝ) (h₀ : x ≠ 0) (h₁ : y ≠ 0) (h₂ : x + 2 / x = y + 2 / y) : x * y = 2 :=

Original problem:

Problem
Given that $x$ and $y$ are distinct nonzero real numbers such that $x+\tfrac{2}{x} = y + \tfrac{2}{y}$, what is $xy$?

Missing a constraint on x and y being distinct.

[albertqjiang]

Same issue with mathd_algebra_131

[albertqjiang]

Same issue with mathd_algebra_482