Theorem: Matroid.contract_delete_minor (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ M ／ C ＼ D ≤m M
Tactic:
rw [contract_delete_diff, ← contract_inter_ground_eq, ← delete_inter_ground_eq,
  contract_ground, diff_inter_self_eq_diff, diff_inter_diff_right, inter_diff_right_comm]
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ M ／ (C ∩ M.E) ＼ (D \ C ∩ M.E) ≤m M

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ M ／ (C ∩ M.E) ＼ (D \ C ∩ M.E) ≤m M
Tactic:
refine ⟨_,_, inter_subset_right, inter_subset_right, ?_, rfl⟩
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ Disjoint (C ∩ M.E) (D \ C ∩ M.E)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ Disjoint (C ∩ M.E) (D \ C ∩ M.E)
Tactic:
exact disjoint_of_subset inter_subset_left inter_subset_left disjoint_sdiff_right
State after:
no goals