1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59

import Mathlib

def check := Id.run do
  for j in [1:99] do
    for k in [1:49] do
      let x := (100 : ℚ) / 99 * j
      let y := (99 : ℚ) * k / 98 / j
      let z := (98 : ℚ) / k
      if x * y * z ≠ 100 ∨ x.floor * y * z ≠ 99 ∨ (x * y).floor * z ≠ 98 then
        return false
  return true

example : check := by
  native_decide

example {x y z : ℚ} (hx : 0 ≤ x) (hy : 0 ≤ y)
    (h₁ : x * y * z = 100) (h₂ : x.floor * y * z = 99) (h₃ : (x * y).floor * z = 98) :
    ∃ j k, 0 < j ∧ j < 99 ∧ 0 < k ∧ k < 49
    ∧ x = (100 : ℚ) / 99 * j ∧ y = (99 : ℚ) * k / 98 / j ∧ z = (98 : ℚ) / k := by
  use x.floor, (x * y).floor
  and_intros
  · by_contra! h
    suffices x.floor = 0 by grind [this ▸ h₂]
    norm_cast at h
    have : Rat.floor 0 = 0 := rfl
    linarith [this ▸ Rat.floor_monotone hx]
  · have : 100 * x.floor < 99 * (x.floor + 1) := by
      have : 100 * x.floor = 99 * x := by grind
      have : 100 * x.floor < 99 * ((x.floor : ℚ) + 1) := by grind [Rat.lt_floor_add_one x]
      norm_cast at this
    norm_cast
    grind
  · by_contra! h
    suffices (x * y).floor = 0 by grind [this ▸ h₃]
    norm_cast at h
    have hxy : 0 ≤ x * y := by positivity
    have : Rat.floor 0 = 0 := rfl
    linarith [this ▸ Rat.floor_monotone hxy]
  · have : 50 * (x * y).floor < 49 * ((x * y).floor + 1) := by
      have : 50 * (x * y).floor = 49 * x * y := by grind
      have : 50 * (x * y).floor < 49 * (((x * y).floor : ℚ) + 1) := by grind [Rat.lt_floor_add_one <| x * y]
      norm_cast at this
    norm_cast
    grind
  all_goals grind

/-
Bad proof:

set_option maxHeartbeats 1000000 in
example {j k : ℕ} (hj : 0 < j ∧ j < 99) (hk : 0 < k ∧ k < 49) :
    let x := (100 : ℚ) / 99 * j
    let y := (99 : ℚ) * k / 98 / j
    let z := (98 : ℚ) / k
    x * y * z = 100 ∧ x.floor * y * z = 99 ∧ (x * y).floor * z = 98 := by
  obtain ⟨_, _⟩ := hj
  obtain ⟨_, _⟩ := hk
  interval_cases j <;> interval_cases k <;> native_decide
-/