rintro ⟨F, hF, rfl⟩
case mp
α : 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 : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) → e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
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})))