Theorem: Matroid.Minor.C_union_D_eq (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₂ : Matroid α
h : N ≤m M
⊢ h.C ∪ h.D = M.E \ N.E
Tactic:
simp only [h.eq_con_del, delete_ground, contract_ground, diff_diff]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
h : N ≤m M
⊢ h.C ∪ h.D = M.E \ (M.E \ (h.C ∪ h.D))

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
h : N ≤m M
⊢ h.C ∪ h.D = M.E \ (M.E \ (h.C ∪ h.D))
Tactic:
rw [Set.diff_diff_cancel_left]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
h : N ≤m M
⊢ h.C ∪ h.D ⊆ 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₂ : Matroid α
h : N ≤m M
⊢ h.C ∪ h.D ⊆ M.E
Tactic:
exact union_subset h.C_indep.subset_ground h.D_coindep.subset_ground
State after:
no goals