exact fun I hIE ↦ ⟨fun hI ↦ ⟨hI.encard_le_erk.trans hr, hIE⟩,
  fun ⟨hcard, _⟩ ↦ indep_of_encard_le_two hcard⟩
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
no goals