by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Let the initial population of Sudbury be s and the initial population of Victoria be v . All we want is vs .\nNow, poplulation of sudsbury decreased be 6 , so at the end of 1996, the population became s−(1006×s)=s×(10094) .\nSimilarly, the new population of Victoria will be v+(10014×v)=v×(100114) .\nAccording to the condition, v×(100114)=s×(10094) .\n\nWhy does s/v=57/47?\n\nWe know v×(100114)=s×(10094) .\nThen when we simplify, we get, vs=94×100114×100=4757
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2967 (s v : ℝ)
(h₀ : 0 < s ∧ 0 < v)
(h₁ : v * (114 / 100) = s * (94 / 100)) :
s / v = 57 / 47 := by sorry