Theorem: Matroid.Circuit.contract_dep_of_not_subset (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 α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
⊢ (M ／ C).Dep (K \ C)
Tactic:
have h' := hK.contract_circuit (C := C ∩ K) (inter_subset_right.ssubset_of_ne (by simpa))
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ (C ∩ K))
⊢ (M ／ C).Dep (K \ C)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ (C ∩ K))
⊢ (M ／ C).Dep (K \ C)
Tactic:
simp only [diff_inter_self_eq_diff] at h'
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ C)
⊢ (M ／ C).Dep (K \ C)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ C)
⊢ (M ／ C).Dep (K \ C)
Tactic:
have hwin := h'.contract_dep (C := C \ K) disjoint_sdiff_sdiff
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)
Tactic:
rwa [contract_contract, inter_union_diff] at hwin
State after:
no goals

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
⊢ C ∩ K ≠ K
Tactic:
simpa
State after:
no goals