simp [nonempty_iso_unif_iff', ← and_assoc, and_congr_left_iff, eq_unifOn_two_iff, and_comm]
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' n : ℕ
⊢ Nonempty (M ≂ unif 2 n) ↔ M.Simple ∧ M.erk ≤ 2 ∧ M.E.encard = ↑n
no goals