rw [← basis_ground_iff, basis_iff_indep_subset_cl, and_congr_right_iff]
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Base B ↔ M.Indep B ∧ M.cl B = M.E
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.cl B ↔ M.cl B = M.E)