Theorem: Matroid.Basis.exchange_base_of_indep (Matroid/Old/_ModularCut.lean)

State before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
⊢ M.Basis (insert f (B \ {e})) X
Tactic:
have X_sub := hB.subset_ground
State after:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ M.Basis (insert f (B \ {e})) X

State before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ M.Basis (insert f (B \ {e})) X
Tactic:
rw [← base_restrict_iff] at hB ⊢
State after:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : (M ↾ X).Base B
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ (M ↾ X).Base (insert f (B \ {e}))

State before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : (M ↾ X).Base B
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ (M ↾ X).Base (insert f (B \ {e}))
Tactic:
apply hB.exchange_base_of_indep hf.2 (hI.indep_restrict_of_subset (insert_subset hf.1
(diff_subset.trans hB.subset_ground)))
State after:
no goals