ch 4.1 - why is natCast automatically distributed over +

Stream: Analysis I

[Rado Kirov]

I am trying to prove something in Ch4.1 that reduces to

 ↑u + ↑t = 0

statement is in Int, and casts are from Nats to Int (we are using mathlib Nats at this point). We have

Section_4_1.Int.cast_eq_0_iff_eq_0 (n : ℕ) : ↑n = 0 ↔ n = 0

So the next step is to apply this, but it doesn't apply because there is addition in the way. So I tried to define my own theorem that the cast is a homomorphism between Nat and Int as monoids, but Lean keeps distributing it over addition so I can't even get to see ↑(u + t) to apply cast_eq_0_iff_eq_0

Screenshot 2025-08-06 at 10.39.21 PM.png

[Rado Kirov]

In the screen shot I expected to see ↑(a + b) = ↑a + ↑b as the theorem statement, which is what I thought I wrote?

[Ruben Van de Velde]

Add an up arrow between the two opening parentheses on the left hand side

[Edward van de Meent]

Or, add : Nat inside the brackets on the lhs

[Rado Kirov]

Ah, I see, + is overloaded on Int too, so Lean is interpreting the cast (a + b): Int as + is in Int, and then making two casts for a and b. Indeed both (↑(a + b) : Int) and (((a + b) : Nat): Int) fix it.

[Li Xuanji]

My mental model of the design decision (not sure if accurate) is that we want 5/6 : Rat to work as expected (ie produce a strictly positive number), so you have to write (5:Nat/6) : Rat if you want the cast to be performed as late as possible (ie produce 0). Then this carries over to all the other numeric types.

I definitely keep accidentally doing the wrong thing though - I sometimes want a mode which is "force me to specify all the coercions myself, and show a type error if the types don't match" vs the default mode, which is something like "if the types don't match, insert coercions as needed"

[Terence Tao]

You can use @HDiv.hDiv to force specific types for division (and @HAdd.hAdd for addition, etc.) if you really want, though it gets messy if you have too many of these operations together.