lean_workbook_plus_67683
Proved, so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67683 (a b c : ℝ) (h : b * c * (a * b * c - 1) - a = 2) : a = (b * c + 2) / (b ^ 2 * c ^ 2 - 1) := by sorry
Source
, so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_67683 (a b c : ℝ) (h : b * c * (a * b * c - 1) - a = 2) : a = (b * c + 2) / (b ^ 2 * c ^ 2 - 1) := by sorry