rw [le_iff_lt_or_eq, encard_eq_two, ← ENat.add_one_le_iff hne, (by norm_num : (2 : ℕ∞) = 1 + 1),
  WithTop.add_le_add_iff_right, encard_le_one_iff_eq] at h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I
α : 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

α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard + 1 ≤ 1 + 1 ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ 1 ≠ ⊤