The uniformity of the meagre ideal is at most the rearrangement number

Both cardinals have their literal definitions: nonM uses nonmeagre subsets of the real line, and rr uses rearranging families of permutations of ℕ. All preceding construction and category lemmas have been proved over mathlib.

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

The defining minimum of the rearrangement number has an actual witness.

theorem NonMRR.nonM_le_rr : nonM ≤ rr

The uniformity of the meagre ideal on the real line is at most the rearrangement number. There are no additional hypotheses.