Theorem: Matroid.Indep.contract_dep_iff (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 α
hI : M.Indep I
⊢ (M ／ I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I)
Tactic:
rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_diff, disjoint_comm,
  union_subset_iff, and_iff_left hI.subset_ground]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
Tactic:
tauto
State after:
no goals