sorry
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
this : ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)

case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}