exact h.1.2
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ ¬M.Spanning H
no goals