Theorem: Matroid.Indep.contract_indep_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).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)
Tactic:
simp_rw [indep_iff, hI.contract_base_iff, union_subset_iff]
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
⊢ (∃ B, (M.Base (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B

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
⊢ (∃ B, (M.Base (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B
Tactic:
exact ⟨fun ⟨B, ⟨hBI, hdj⟩, hJB⟩ ↦
  ⟨disjoint_of_subset_left hJB hdj, _, hBI, hJB.trans subset_union_left,
    subset_union_right⟩,
  fun ⟨hdj, B, hB, hJB, hIB⟩ ↦ ⟨B \ I,⟨by simpa [union_eq_self_of_subset_right hIB],
    disjoint_sdiff_left⟩, subset_diff.2 ⟨hJB, hdj⟩ ⟩⟩
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 α
hI : M.Indep I
x✝ : Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B
hdj : Disjoint J I
B : Set α
hB : M.Base B
hJB : J ⊆ B
hIB : I ⊆ B
⊢ M.Base (B \ I ∪ I)
Tactic:
simpa [union_eq_self_of_subset_right hIB]
State after:
no goals