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

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.
  have h_exists : ∀ n : ℕ, ∃ a b c : ℕ, valid_tuple a b c n := by
    bound;
    -- 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_1 ∧ n_1 < 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_1 := by
        exact ⟨ n_1 + 3, by simp +arith +decide [ 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_1 - Nat.choose x 3
    have hz : 0 ≤ z ∧ z < Nat.choose x 2 := by
      simp +zetaDelta at *;
      rcases x with ( _ | _ | x ) <;> simp +arith +decide [ Nat.choose ] at * ; omega;
    -- 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_binary_search : ∃ y, Nat.choose y 2 ≤ z ∧ z < Nat.choose (y + 1) 2 := by
        have h_exists_y : ∃ y, Nat.choose y 2 > z := by
          exact ⟨ z + 2, by simp +arith +decide [ Nat.choose ] ⟩
        contrapose! h_exists_y;
        intro y; induction y <;> aesop;
      exact h_binary_search;
    -- Let $a = n_1 - \binom{x}{3} - \binom{y}{2}$.
    set a := n_1 - Nat.choose x 3 - Nat.choose y 2;
    use a, y, x;
    aesop;
    constructor;
    · rcases y with ( _ | _ | y ) <;> simp_all +arith +decide [ Nat.choose ];
    · aesop;
      contrapose! right_1;
      exact absurd left_1 ( not_le_of_gt ( lt_of_lt_of_le hz ( Nat.choose_le_choose _ right_1 ) ) );
  sorry