lean_workbook_plus_80145
ProvedLet the escalater move at stairs in a time unit, person move stairs in that same time unit and person move stairs in the time unit. \n\nSo in the case of person , the escalator moves stairs in the same time that person moves stairs. Therefore, we can set up the equation that: \n\n \n\nSimilarly, for person , the escalator moves as person moves stairs. Thus: \n\n \n\nDividing the second by the first gives the following. \n\n \n\nThis gives that, \n\n \n \n\nTherefore the answer is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_80145 (a b z n : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < z ∧ 0 < n) (h₁ : 3 * z = 2 * b) (h₂ : (n - 27) / a = 27 / (2 * b)) (h₃ : (n - 18) / a = 18 / b) : n = 54 := by sorry
Source