Theorem: Matroid.contract_inter_ground_eq (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 α
M : Matroid α
C : Set α
⊢ M ／ (C ∩ M.E) = M ／ C
Tactic:
rw [← dual_delete_dual_eq_contract, (show M.E = M✶.E from rfl), delete_inter_ground_eq]
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶ = M ／ C

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶ = M ／ C
Tactic:
rfl
State after:
no goals