Unable to simplify due to dependent types

Stream: lean4

[Op From The Start]

I have the tactics:

rename_i x y
  rw [←hx, ←hy]
  simp [Ordinal.nadd_comm]
  let ryyr : right y = yR := by
    rw [hy]
    simp [right]
  let yr2 := yr
  rw [←ryyr] at yr2
  let hb := birthday_right_child_lt y yr2

and state:

**x y** : PreNo
**xL xR** : Type
**xLS** : xL → PreNo
**xRS** : xR → PreNo
**yL yR** : Type
**yLS** : yL → PreNo
**yRS** : yR → PreNo
**hx** : x = PreNo.mk xL xR xLS xRS
**hy** : y = PreNo.mk yL yR yLS yRS
**yr** : yR
**ryyr** : right y = yR
**yr2** : right y
**hb** : birthday (rightm y yr2) < birthday y
**⊢** birthday (yRS yr) < birthday y

By definition yRS = rightm y and yr=yr2, but as they have differing types I am unable to simplify them to solve the goal. What should I do?

[Op From The Start]

I've reduced it a bit to

**x y** : PreNo
**xL xR** : Type
**xLS** : xL → PreNo
**xRS** : xR → PreNo
**yL yR** : Type
**yLS** : yL → PreNo
**yRS** : yR → PreNo
**hx** : x = PreNo.mk xL xR xLS xRS
**hy** : y = PreNo.mk yL yR yLS yRS
**yr** : yR
**ryyr** : right y = yR
**yr2** : right y
**hb** : birthday (rightm y yr2) < birthday y
**⊢** yRS yr = rightm y yr2

[Op From The Start]

def rightm (x: PreNo) : right x → PreNo :=
  match x with
  | PreNo.mk _ _ _ xRS => xRS

let yr2 := yr
rw [←ryyr] at yr2

So they are both definitionally equal