convert hwin (Ordinal.type r) rfl.le
α : 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)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ M.cl (⋂ i, Xs i) = {k}
case h.e'_2.h.e'_3.h.e'_3.h
α : 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)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
x✝ : ι
⊢ Xs x✝ = ⋂ (_ : x✝ ∈ range fun p => Ordinal.enum r ↑p ⋯), Xs x✝

case h.e'_3
α : 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)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ {k} = ⋂ i ∈ range fun p => Ordinal.enum r ↑p ⋯, M.cl (Xs i)