ZMod.coe_add_eq_ite changed

Stream: mathlib4

[Kevin Buzzard]

In Lean 3 the type of docs3#zmod.coe_add_eq_ite was ↑(a + b) = ite (↑n ≤ ↑a + ↑b) (↑a + ↑b - ↑n) (↑a + ↑b) (the up-arrows are all from $\Z/n\Z$ to $\Z$) so this lemma has a little content. In Lean 4 it is currently ↑(a + b) = ↑(if ↑n ≤ ↑a + ↑b then a + b - ↑n else a + b) which is much easier to prove: it says that coerced (a+b) is equal to coerced (a+b) or coerced (a+b-0); indeed the current Lean 4 theorem can be proved with simp which is a bit suspicious.

Assuming I've not made a mistake above, this means that the type of coe_add_eq_ite has changed. I would expect to see some warning about this in the mathlib3port file, but it seems fine. What have I misunderstood?

[Chris Hughes]

It happened a lot in the port that lemma statements involving coercions changed, and I don't remember mathport giving warnings about these ones. I would just make a PR fixing the Lean4 statement.

[Kevin Buzzard]

#5981

[Ruben Van de Velde]

The warnings would probably have caught this, but we turned them off because they were mostly false positives

[Eric Wieser]

The final straw that led to turning them off was that some warnings were 100s of Mb of text (in a single line!), and that made github unhappy