Proved Palomar declarations

These declarations discharge the three statements in Challenge.lean using the substantive proof development in this repository. Challenge and Solution are separate environments: never import Challenge here.

theorem PalomarRR.nonM_minimum : ∃ (s : Set ℝ), ¬IsMeagre s ∧ Cardinal.mk ↑s = NonMRR.nonM

The real nonmeagre minimum exists by the Baire category theorem.

theorem PalomarRR.rr_minimum : ∃ (P : Set (Equiv.Perm ℕ)), NonMRR.IsRearranging P ∧ Cardinal.mk ↑P = NonMRR.rr

Rearranging families exist and their cardinal minimum is attained.

theorem PalomarRR.nonM_le_rr : NonMRR.nonM ≤ NonMRR.rr

The lower-bound direction of the manuscript's Main Theorem 1.2.