induction' o using Ordinal.induction with p hp
α : 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 ⋯)
case h
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
p : Ordinal.{u}
hp : ∀ k < p, ∀ (ho : k ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (ho : p ≤ Ordinal.type r), P (range fun p_1 => Ordinal.enum r ↑p_1 ⋯)