lean_workbook_plus_45482
ProvedLet . We're given that . Cross-multiplying, we get . From the quadratic formula, we have or . It's given that is positive, so we must have .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_45482 (m n : ℤ) (a : ℚ) (h₀ : 0 < a) (h₁ : 0 < n) (h₂ : ¬ 5 * m = 13 * n) (h₃ : (m : ℚ) / n = a) (h₄ : a = (7 + 1 / a) / (65 - 1 / a)) : a = 1 / 5 := by sorry
Source