obtain (rfl | ⟨x, rfl⟩) | ⟨x, y, -, rfl⟩ := h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : (I = ∅ ∨ ∃ x, I = {x}) ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I
case inl.inl
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
hI : autoParam (∅ ⊆ M.E) _auto✝
hne : ∅.encard ≠ ⊤
⊢ M.Indep ∅

case inl.inr.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ M.Indep {x}

case inr.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x y : α
hI : autoParam ({x, y} ⊆ M.E) _auto✝
hne : {x, y}.encard ≠ ⊤
⊢ M.Indep {x, y}