exact ⟨fun h ↦ ⟨h.basis_cl_right, h.subset.trans inter_subset_left⟩,
  fun h ↦ h.1.basis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_cl _)⟩
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis I (X ∩ M.E) ↔ M.Basis I (M.cl (X ∩ M.E)) ∧ I ⊆ X
no goals