Theorem: Matroid.Circuit.contract_dep (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
hCK : Disjoint C K
⊢ (M ／ C).Dep K
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (C ∩ M.E)
State after:
case intro
α : 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
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ (M ／ C).Dep K

State before:
case intro
α : 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
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ (M ／ C).Dep K
Tactic:
rw [← contract_inter_ground_eq, Dep, hI.contract_indep_iff,
  and_iff_left (hCK.mono_left inter_subset_left), contract_ground, subset_diff,
  and_iff_left (hCK.symm.mono_right inter_subset_left), and_iff_left hK.subset_ground]
State after:
case intro
α : 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
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)

State before:
case intro
α : 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
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)
Tactic:
exact fun hi ↦ hK.dep.not_indep (hi.subset subset_union_left)
State after:
no goals