Theorem: Matroid.Indep.contract_base_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).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
have hIE := 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
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I

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
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
rw [← dual_dual M, ← coindep_def, coindep_iff_exists] at hI
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : ∃ B, M✶.Base B ∧ B ⊆ M✶.E \ I
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : ∃ B, M✶.Base B ∧ B ⊆ M✶.E \ I
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
obtain ⟨B₀, hB₀, hfk⟩ := hI
State after:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I

State before:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
rw [← dual_dual M, ← dual_delete_dual_eq_contract, dual_base_iff', dual_base_iff',
  delete_base_iff, dual_dual, delete_ground, diff_diff, union_comm, union_subset_iff,
  subset_diff, ← and_assoc, and_congr_left_iff, dual_ground, and_iff_left hIE, and_congr_left_iff]
State after:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ Disjoint B I → B ⊆ M.E → (M✶.Basis (M.E \ (B ∪ I)) (M.E \ I) ↔ M✶.Base (M.E \ (B ∪ I)))

State before:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ Disjoint B I → B ⊆ M.E → (M✶.Basis (M.E \ (B ∪ I)) (M.E \ I) ↔ M✶.Base (M.E \ (B ∪ I)))
Tactic:
refine' fun _ _ ↦
  ⟨fun h ↦ h.base_of_base_subset hB₀ (subset_diff.mpr ⟨hB₀.subset_ground, _⟩), fun hB ↦
    hB.basis_of_subset diff_subset (diff_subset_diff_right subset_union_right)⟩
State after:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
x✝¹ : Disjoint B I
x✝ : B ⊆ M.E
h : M✶.Basis (M.E \ (B ∪ I)) (M.E \ I)
⊢ Disjoint B₀ I

State before:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
x✝¹ : Disjoint B I
x✝ : B ⊆ M.E
h : M✶.Basis (M.E \ (B ∪ I)) (M.E \ I)
⊢ Disjoint B₀ I
Tactic:
exact disjoint_of_subset_left hfk disjoint_sdiff_left
State after:
no goals