Issues in !4a#2353 (SetTheory.Ordinal.NaturalOps)

Stream: mathlib4

[Arien Malec]

There are two big issues in this PR:

1) Previously in Lean 3 one could do this:

@[pattern] def ordinal.to_nat_ordinal : ordinal ≃o nat_ordinal := order_iso.refl _
@[pattern] def nat_ordinal.to_ordinal : nat_ordinal ≃o ordinal := order_iso.refl _

namespace nat_ordinal

variables {a b c : nat_ordinal.{u}}

theorem to_ordinal_to_nat_ordinal (a : nat_ordinal) : a.to_ordinal.to_nat_ordinal = a := rfl

In Lean 4, the equivalent of the theorem generates errors:

invalid field notation, function 'NatOrdinal.toOrdinal' does not have argument with type (NatOrdinal ...) that can be used, it must be explicit or implicit with a unique name

If I'm following the error, Lean wants a named parameter, but I haven't been able to figure out how to create one that typechecks for OrderIso

2. Lean 4 does not like scoped[NaturalOps] infixl:65 " ♯ " => Ordinal.nadd. Subsequent reference to ♯ gives an unexpected token error

[Jireh Loreaux]

I think the problem is that Lean 4 doesn't recognize the order iso (or more generally any equiv) as a function when you are calling it with dot notation.

[Arien Malec]

Ah, that's it

Ordinal.toNatOrdinal (NatOrdinal.toOrdinal a) = a works.

Not pretty....

[Arien Malec]

The fix for the second issue is ooen NaturalOps