lean_workbook_plus_53710

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

After equating $y_1y_2y_3y_4=1$ and $x_1x_2y_1y_2=1$ and canceling out $y_1y_2$ , prove that $x_1x_2=y_3y_4$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53710 (x₁ x₂ y₁ y₂ y₃ y₄ : ℝ) (h₁ : y₁ * y₂ * y₃ * y₄ = 1) (h₂ : x₁ * x₂ * y₁ * y₂ = 1) : x₁ * x₂ = y₃ * y₄   :=  by sorry

Source