Theorem: Matroid.Indep.base_of_spanning (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hI : M.Indep I
hIs : M.Spanning I
⊢ M.Base I
Tactic:
obtain ⟨B, hB, hBI⟩ := hIs.exists_base_subset
State after:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.Base B
hBI : B ⊆ I
⊢ M.Base I

State before:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.Base B
hBI : B ⊆ I
⊢ M.Base I
Tactic:
rwa [← hB.eq_of_subset_indep hI hBI]
State after:
no goals