lean_workbook_plus_79422

Proved

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

Doing so, we have $23A+23B = 12C \implies 23(A+B) = 12C \implies \frac{C}{A+B} = \frac{23}{12}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79422  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a + b + c = 1)
  (h₂ : 23 * a + 23 * b = 12 * c) :
  c / (a + b) = 23 / 12   :=  by sorry

Source

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

View graph