Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1980P1

module

public import Mathlib.Analysis.Normed.Field.Basic
public import Mathlib.Analysis.Real.Sqrt
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1980, Problem 1

A balance has unequal arms and pans of unequal weight. It is used to weigh
two objects of unequal weight. The first object balances against a weight A,
when placed in the left pan and against a weight a, when placed in the right
pan. The corresponding weights for the second object are B and b. A third
object balances against a weight C, when placed in the left pan. What is its
true weight?
-/

namespace Usa1980P1

open Real

noncomputable /- determine -/ abbrev solution (A a B b C : ℝ) : ℝ := sorry

theorem usa1980_p1 {A a B b C h k x₁ x₂ x₃ : ℝ} (hh : 0 < h)
    (h1 : x₁ = h * A + k) (h2 : a = h * x₁ + k)
    (h3 : x₂ = h * B + k) (h4 : b = h * x₂ + k)
    (h5 : x₃ = h * C + k) (hne : x₁ ≠ x₂) :
    x₃ = solution A a B b C := sorry

end Usa1980P1

File author(s): Kimi K3

This problem has a complete formalized solution.