Theorem: ramsey_exists (FormalBook/Chapter_45.lean)

State before:
α : Type ?u.1805
X : Finset α
d : ℕ
h_d : d ≥ 2
m n : ℕ
h_m : m ≥ 2
h_n : n ≥ 2
⊢ ∃ N, ramsey_property m n N
Tactic:
sorry
State after:
no goals