lean_workbook_plus_57799

Proved

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

Prove for all $a,b \in \mathbb{R}$ the inequality \n\n $(1+a^2)(1+b^2) \geq (a+b)(1+ab)$ and determine when equality holds.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57799 (a b : ℝ) : (1 + a ^ 2) * (1 + b ^ 2) ≥ (a + b) * (1 + a * b)   :=  by sorry

Source