intro o
α : 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 ⋯)
α : 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 ⋯)