Solving a linear system with pi

Proved

WorkbookRestored.plus_43574

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

If real $I,J$ satisfy $I+J=4$ and $I-J=\pi$ , then $I=(4+\pi)/2$ and $J=(4-\pi)/2$ .

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_43574 (Apache-2.0).

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Nat

Formal statement

theorem WorkbookRestored.plus_43574 (I J : ℝ) (h₁ : I + J = 4) (h₂ : I - J = Real.pi) : I = (4 + Real.pi) / 2 ∧ J = (4 - Real.pi) / 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_43574; original Prove2Me node 6d52e182-3dd7-4736-bf4b-81aaa0318cd1; Apache-2.0

View graph