rintro ⟨rfl, hr, hM⟩
case mpr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple → M = unifOn E 2
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ M = unifOn M.E 2