Prove2Me

lean_workbook_plus_38994

Proved

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

if 0<x<1 0 < x < 1 and 0<y<1 0 < y < 1 and y(1−x)>14 y(1 - x) > \frac14 then y>x y > x.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38994 (x y : ℝ) (hx : 0 < x ∧ x < 1) (hy : 0 < y ∧ y < 1) (h : y * (1 - x) > 1 / 4) : y > x   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph