obtain (heF | heF) := em (e ∈ F) <;> simp [heF, hF]
case mp.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
F : Set α
hF : M.Flat F
⊢ e ∉ F \ {e} ∧ (M.Flat (F \ {e}) ∨ M.Flat (insert e (F \ {e})))
no goals