refine' ⟨fun h ↦ ⟨h.subset,h.indep, h.er_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩  ↦ _⟩
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
⊢ M.Basis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis' I X