Theorem: Matroid.relRank_cl_right (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 X (M.cl Y) = M.relRank X Y
Tactic:
refine le_antisymm ?_ ?_
State after:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (M.cl Y) ≤ M.relRank X Y

case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y ≤ M.relRank X (M.cl Y)

State before:
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y ≤ M.relRank X (M.cl Y)
Tactic:
rw [relRank, ← er_inter_ground_eq, contract_ground, ← inter_diff_assoc]
State after:
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er ((Y ∩ M.E) \ X) ≤ M.relRank X (M.cl Y)

State before:
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er ((Y ∩ M.E) \ X) ≤ M.relRank X (M.cl Y)
Tactic:
exact er_mono _ <| diff_subset.trans
  ((M.subset_cl _).trans (M.cl_subset_cl inter_subset_left))
State after:
no goals

State before:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (M.cl Y) ≤ M.relRank X Y
Tactic:
rw [relRank_eq_er_diff_contract,  relRank, ← (M ／ X).er_cl_eq Y, contract_cl_eq]
State after:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er (M.cl Y \ X) ≤ (M ／ X).er (M.cl (Y ∪ X) \ X)

State before:
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er (M.cl Y \ X) ≤ (M ／ X).er (M.cl (Y ∪ X) \ X)
Tactic:
exact (M ／ X).er_mono (diff_subset_diff_left (M.cl_subset_cl subset_union_left))
State after:
no goals