From 086f83ce5c01aee1cb3b91f9e4ad4ec958dd52e8 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Fri, 22 Sep 2023 20:11:45 -0400
Subject: [PATCH] [Usa2023Q2] finish proof of monotonicity

---
 MathPuzzles/Usa2023Q2.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/MathPuzzles/Usa2023Q2.lean b/MathPuzzles/Usa2023Q2.lean
index b6601695..8f157fa9 100644
--- a/MathPuzzles/Usa2023Q2.lean
+++ b/MathPuzzles/Usa2023Q2.lean
@@ -84,7 +84,9 @@ problem usa2023Q2 (f : ℝ+ → ℝ+) :
         rw [mul_assoc a (ynum / yden) yden, div_mul_cancel']
         rw [mul_assoc b (ynum / yden) yden, div_mul_cancel']
         unfold_let ynum yden
-        sorry
+        rw [←Subtype.coe_inj]
+        simp only [Positive.coe_add, Positive.val_mul]
+        ring
       rw [hpab] at hpa
       rw [hpa] at hpb
       -- ... gives a⬝f(y) + 2 = b⬝f(y) + 2, which is impossible