simp only [eq_iff_indep_iff_indep_forall, unifOn_ground_eq, unifOn_indep_iff, true_and]
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
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ ∀ I ⊆ M.E, M.Indep I ↔ I.encard ≤ 2 ∧ I ⊆ M.E