lean_workbook_plus_942
ProvedLet be reals such that Prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_942 (x y : ℝ) (h : x^2 + y^2 ≤ 2 * x + y) : 2 * x + y ≤ 5 := by sorry
Source
Let be reals such that Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_942 (x y : ℝ) (h : x^2 + y^2 ≤ 2 * x + y) : 2 * x + y ≤ 5 := by sorry