Skip to content

Commit

Permalink
[Usa2023Q2] finish proof of monotonicity
Browse files Browse the repository at this point in the history
  • Loading branch information
dwrensha committed Sep 23, 2023
1 parent ffbe739 commit 086f83c
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion MathPuzzles/Usa2023Q2.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 086f83c

Please sign in to comment.