refine Indep.base_of_spanning ?_ ?_
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Base (insert e I)
case refine_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Indep (insert e I)

case refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Spanning (insert e I)