What is 2?

Stream: mathlib4

[Siddhartha Gadgil]

The following fails while porting:

variable [Semiring α] [Semiring β] {m n : α}
example : (2 : α) = (1 : α) + (1 : α) := by rfl

I am trying to deconstruct the definition of 2 in a Semiring, but perhaps someone here knows what to simp/rw/unfold.

Thanks.

[Ruben Van de Velde]

This is rather more painful in lean 4. I think zero_le_two and related lemmas could be used for inspiration

[Siddhartha Gadgil]

Thanks. That indeed uses one_add_one_equals_two, which is just what I needed.

[Siddhartha Gadgil]

And indeed two errors were fixed by that and the final one by copying from its proof

[Kevin Buzzard]

I suppose it's inevitable that some things are defeq that didn't used to be (eta for structures) and some things are not defeq that used to be (numerals, mod, fin stuff).

[Siddhartha Gadgil]

It's not a problem as long as there are theorems for rewriting.

[Riccardo Brasca]

We can maybe add this to the common problems section of the wiki.

[Kevin Buzzard]

Yes I guess the only problem is the pain making the API itself