suffices hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r),
    P (range (fun p : Iio o ↦ Ordinal.enum r p.1 (lt_of_lt_of_le p.2 ho))) by
  convert hwin (Ordinal.type r) rfl.le
  rw [eq_comm, eq_univ_iff_forall]
  refine fun i ↦ ⟨⟨Ordinal.typein r i, Ordinal.typein_lt_type r i⟩, Ordinal.enum_typein _ _⟩
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ P univ
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)