lean_workbook_plus_32480

Proved

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

Do substitution. Let's find $x$ in terms of $y$ . \nFrom the second equation, we can find that $x=(12-4y)/3$ \nLet's substitute that value into the first equation. \n $((12-4y)/3)^2/16+y^2/9=1.$ \nAfter simplification, we get a fairly simple quadratic which yields the solutions $(0,3)$ and $(4,0)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32480  (x y : ℝ)
  (h₀ : (x^2 / 16 + y^2 / 9) = 1)
  (h₁ : x = (12 - 4 * y) / 3) :
  x = 0 ∧ y = 3 ∨ x = 4 ∧ y = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph