Theorem: ClMatroid.cl_inter_ground (Matroid/Constructions/ClosureAxioms.lean)

State before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
X : Set α
⊢ M.cl (X ∩ M.E) = M.cl X
Tactic:
rw [← inter_eq_self_of_subset_left (M.cl_subset_ground (X ∩ M.E)), M.cl_inter_inter_ground]
State after:
no goals