Convert wellOrderedRelation.1 into <

Stream: lean4

[Op From The Start]

I got it mostly simplified, but I need to show with this relation

instance wellFoundedRelation : WellFoundedRelation Ordinal :=
  ⟨(· < ·), lt_wf⟩

that

tactic 'apply' failed, failed to unify
  Prop
with
  Ordinal.wellFoundedRelation.1 ((Order.succ β).nmul (Order.succ xr)) ((Order.succ α).nmul (Order.succ β))

α β : Ordinal.{u_1}
x : Game α
y : Game β
xr : Ordinal.{u_1}
p : xr < x.RO
⊢ Ordinal.wellFoundedRelation.1 ((Order.succ β).nmul (Order.succ xr)) ((Order.succ α).nmul (Order.succ β))

And I know how to do all of it, except how to replace Ordinal.wellFoundedRelation.1 _ _ with _ < _. How do I simplify this?

[Op From The Start]

Nvm, I got it, it just took rw [Ordinal.wellFoundedRelation] instead of rw [Ordinal.wellFoundedRelation.1]