Theorem: Matroid.relRank_cl_left (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank (M.cl X) Y = M.relRank X Y
Tactic:
rw [relRank, relRank, contract_cl_eq_contract_delete, delete_er_eq', LoopEquiv.er_eq_er]
State after:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).LoopEquiv (Y \ (M.cl X \ X)) Y

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).LoopEquiv (Y \ (M.cl X \ X)) Y
Tactic:
rw [loopEquiv_iff_union_eq_union, contract_loops_eq, diff_union_self]
State after:
no goals