Adding two cubic constraints

Proved

WorkbookSource.problem_13207

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Another solution: Again, we suppose that $AD$ is a diameter of the semicircle. Let $e = CE$ and $f = CA$ . From a result of the previous post, $a^2 + b^2 + e^2 + abe = 4$ and $f^2 + c^2 + d^2 + fcd = 4$ . Adding these gives $a^2 + b^2 + c^2 + d^2 + e^2 + f^2 + abe + fcd = 8$ .

Source: InternLM Lean-Workbook, record lean_workbook_13207 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_13207  (a b c d e f : ℝ)
  (h₀ : a^2 + b^2 + e^2 + a * b * e = 4)
  (h₁ : f^2 + c^2 + d^2 + f * c * d = 4) :
  a^2 + b^2 + c^2 + d^2 + e^2 + f^2 + a * b * e + f * c * d = 8  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_13207; Apache-2.0

View graph