Theorem: Matroid.rFin.contract_rFin_of_subset_union (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
h : M.rFin Z
X C : Set α
hX : X ⊆ M.cl (Z ∪ C)
⊢ X \ C ⊆ (M ／ C).cl Z
Tactic:
rw [contract_cl_eq]
State after:
α : Type u_1
M N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
h : M.rFin Z
X C : Set α
hX : X ⊆ M.cl (Z ∪ C)
⊢ X \ C ⊆ M.cl (Z ∪ C) \ C

State before:
α : Type u_1
M N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
h : M.rFin Z
X C : Set α
hX : X ⊆ M.cl (Z ∪ C)
⊢ X \ C ⊆ M.cl (Z ∪ C) \ C
Tactic:
exact diff_subset_diff_left hX
State after:
no goals