Theorem: Matroid.Basis.diff_subset_loops_contract (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X \ I ⊆ (M ／ I).cl ∅
Tactic:
rw [diff_subset_iff, contract_loops_eq, union_diff_self,
  union_eq_self_of_subset_left (M.subset_cl I)]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X ⊆ M.cl I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X ⊆ M.cl I
Tactic:
exact hIX.subset_cl
State after:
no goals