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
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90

/-
This file was edited by Aristotle.

Lean Toolchain version: leanprover/lean4:v4.20.0-rc5
Mathlib version: d62eab0cc36ea522904895389c301cf8d844fd69 (May 9, 2025)

The following was proved by Aristotle:

- example n : (∃ a b c, valid_tuple a b c n) ∧ ∀ a₁ b₁ c₁ a₂ b₂ c₂, valid_tuple a₁ b₁ c₁ n ∧ valid_tuple a₂ b₂ c₂ n → a₁ = a₂ ∧ b₁ = b₂ ∧ c₁ = c₂
-/

import Mathlib


def valid_tuple (a b c n : ℕ) := a < b ∧ b < c ∧ a.choose 1 + b.choose 2 + c.choose 3 = n

example n : (∃ a b c, valid_tuple a b c n) ∧ ∀ a₁ b₁ c₁ a₂ b₂ c₂, valid_tuple a₁ b₁ c₁ n ∧ valid_tuple a₂ b₂ c₂ n → a₁ = a₂ ∧ b₁ = b₂ ∧ c₁ = c₂ := by
  -- To prove the existence of such a tuple, we can use the fact that for any natural number $n$, there exists a unique tuple $(a, b, c)$ satisfying the given conditions.
  constructor
  · -- Let's choose x such that C(x,3) ≤ n < C(x+1,3). Then take z = n - C(x,3) and find y such that C(y,2) ≤ z < C(y+1,2). Finally, take x' = z - C(y,2).
    obtain ⟨x, hx⟩ : ∃ x, Nat.choose x 3 ≤ n ∧ n < Nat.choose (x + 1) 3 := by
      -- Since $\binom{x}{3}$ grows without bound, there exists some $x$ such that $\binom{x}{3} > n_1$.
      have hx_bound : ∃ x, Nat.choose x 3 > n := ⟨n + 3, by simp +arith [Nat.choose]⟩
      contrapose! hx_bound
      exact fun x => Nat.recOn x (by norm_num) hx_bound
    -- Let $z = n_1 - \binom{x}{3}$. Then $0 \leq z < \binom{x+1}{3} - \binom{x}{3} = \binom{x}{2}$.
    set z := n - Nat.choose x 3
    have hz : 0 ≤ z ∧ z < Nat.choose x 2 := by grind [Nat.choose]
    -- Let $y$ be such that $\binom{y}{2} \leq z < \binom{y+1}{2}$.
    obtain ⟨y, hy⟩ : ∃ y, Nat.choose y 2 ≤ z ∧ z < Nat.choose (y + 1) 2 := by
      -- We can find such a $y$ using binary search since $\binom{y}{2}$ is strictly increasing for $y \geq 2$.
      have h_exists_y : ∃ y, Nat.choose y 2 > z := ⟨z + 2, by simp +arith [Nat.choose]⟩
      contrapose! h_exists_y
      exact fun x => Nat.recOn x (by norm_num) h_exists_y
    -- Let $a = n_1 - \binom{x}{3} - \binom{y}{2}$.
    set a := n - Nat.choose x 3 - Nat.choose y 2
    use a, y, x
    simp_all only [zero_le, true_and, z, a]
    obtain ⟨left_1, right_1⟩ := hy
    constructor
    · rcases y with (_ | _ | y) <;> simp_all +arith +decide [Nat.choose]
    · simp_all only [Nat.choose_one_right, Nat.sub_add_cancel, and_true]
      contrapose! right_1
      exact absurd left_1 (not_le_of_gt (lt_of_lt_of_le hz (Nat.choose_le_choose _ right_1)))
  · -- To prove uniqueness, assume there are two triples $(a_1, b_1, c_1)$ and $(a_2, b_2, c_2)$ that both satisfy the conditions for $n$.
    intros a₁ b₁ c₁ a₂ b₂ c₂ h
    obtain ⟨h₁, h₂⟩ := h
    have hc : c₁ = c₂ := by
      unfold valid_tuple at *
      simp_all only [Nat.choose_one_right]
      obtain ⟨left, right⟩ := h₁
      obtain ⟨left_1, right_1⟩ := h₂
      obtain ⟨left_2, right⟩ := right
      obtain ⟨left_3, right_1⟩ := right_1
      subst right
      -- By contradiction, assume $c₁ \ne c₂$. Without loss of generality, let $c₁ > c₂$.
      by_contra hc_ne
      wlog hc_gt : c₁ > c₂ generalizing c₁ c₂ a₁ b₁ a₂ b₂
      · exact this a₂ b₂ c₂ a₁ b₁ c₁ left_1 left left_3 left_2 (by linarith) (Ne.symm hc_ne) (lt_of_le_of_ne (le_of_not_gt hc_gt) hc_ne)
      · -- Since $c_1 > c_2$, we have $\binom{c_1}{3} \geq \binom{c_2 + 1}{3}$.
        have h_binom_c : Nat.choose c₁ 3 ≥ Nat.choose (c₂ + 1) 3 := Nat.choose_le_choose _ hc_gt
        rcases c₂ with (_ | _ | c₂) <;> simp_all +arith +decide [Nat.choose]
        -- Since $b_2 \leq c_2 + 1$, we have $\binom{b_2}{2} \leq \binom{c_2 + 1}{2}$.
        have h_binom_b : Nat.choose b₂ 2 ≤ Nat.choose (c₂ + 1) 2 := Nat.choose_le_choose _ left_3
        simp_all [Nat.choose_succ_succ]
        grind
    have hb : b₁ = b₂ := by
      unfold valid_tuple at h₁ h₂
      subst hc
      simp_all only [Nat.choose_one_right]
      obtain ⟨left, right⟩ := h₁
      obtain ⟨left_1, right_1⟩ := h₂
      obtain ⟨left_2, right⟩ := right
      obtain ⟨left_3, right_1⟩ := right_1
      subst right_1
      simp_all only [Nat.add_right_cancel_iff]
      contrapose! right
      cases lt_or_gt_of_ne right <;> simp_all only [ne_eq, Nat.choose_two_right]
      · nlinarith [Nat.div_mul_cancel (show 2 ∣ b₁ * (b₁ - 1) from even_iff_two_dvd.mp (Nat.even_mul_pred_self _)), Nat.div_mul_cancel (show 2 ∣ b₂ * (b₂ - 1) from even_iff_two_dvd.mp (Nat.even_mul_pred_self _)), Nat.sub_add_cancel (by linarith : 1 ≤ b₁), Nat.sub_add_cancel (by linarith : 1 ≤ b₂)]
      · exact ne_of_gt <| by nlinarith [Nat.div_mul_cancel (show 2 ∣ b₁ * (b₁ - 1) from even_iff_two_dvd.mp <| Nat.even_mul_pred_self _), Nat.div_mul_cancel (show 2 ∣ b₂ * (b₂ - 1) from even_iff_two_dvd.mp <| Nat.even_mul_pred_self _), Nat.sub_add_cancel (by linarith : 1 ≤ b₁), Nat.sub_add_cancel (by linarith : 1 ≤ b₂)]
    have ha : a₁ = a₂ := by
      unfold valid_tuple at h₁ h₂
      subst hb hc
      simp_all only [Nat.choose_one_right, true_and]
      obtain ⟨left, right⟩ := h₁
      obtain ⟨left_1, right_1⟩ := h₂
      obtain ⟨left_2, right_1⟩ := right_1
      subst right
      simp_all only [Nat.add_right_cancel_iff]
    exact ⟨ha, hb, hc⟩