lean_workbook_plus_12630

Proved

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

We have $c^2 = a^2+b^2$ in our problem. Since in every right triangle we have $[ABC]=(u-a)(u-b) = \dfrac{ab}2$ , where $u$ is semiperimeter, $\begin{array}{rcl} \dfrac{b(b+c)}{a(a+c)} &=& \dfrac{2b(b+c-a)+2ab}{2a(a+c-b)+2ab}\ \ &=& \dfrac{2b(b+c-a)+(b+c-a)(a+c-b)}{2a(a+c-b)+(b+c-a)(a+c-b)} \ \ &=& \dfrac{(b+c-a)(a+b+c)}{(a+c-b)(a+bc)} \ \ &=& \dfrac{u-a}{u-b} \end{array}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12630  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : c^2 = a^2 + b^2) :
  (b * (b + c)) / (a * (a + c)) = (2 * b * (b + c - a) + 2 * a * b) / (2 * a * (a + c - b) + 2 * a * b)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph