Prove2Me

lean_workbook_plus_13695

Proved

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

x+y=7 x+y=7 \n x2−y2=21 x^2-y^2=21 \n y=7−x y=7-x \n x2−(7−x)2 x^2-(7-x)^2 \n x2−x2+14x−49 x^2-x^2+14x-49 \n 14x=70 14x=70 \n x=5 x=5 \n   ⟹   y=2 \implies\ y=2 \n 2x+3y=2∗5+3∗2=10+6=16 2x+3y=2*5+3*2=10+6=16

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13695  (x y : ℝ)
  (h₀ : x + y = 7)
  (h₁ : x^2 - y^2 = 21)
  (h₂ : y = 7 - x)
  (h₃ : x^2 - (7 - x)^2 = 21) :
  2 * x + 3 * y = 16   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph