rintro hi x (rfl | rfl)
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
case inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
hf : M.Nonloop f
x : α
he : M.Nonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})

case inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
x : α
hf : M.Nonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})