casting and adding in zmod

Stream: new members

[Rose Lopez]

Hi! I am trying to simplify a goal:

⊢ ↑(x + y) = ↑x + ↑y

so I made a have statement

have add : (x : zmod n) + (y : zmod n) = ((x + y) : zmod n),

and the proof consisted of rfl

but afterwards, in the tactic state I see this,

add : ↑x + ↑y = ↑x + ↑y

and so my add statement is not helpful. Why is the goal state not recognizing that I casted then added in LHS and added then casted in RHS?

[Kevin Buzzard]

If you're using mathlib and you have import tactic at the top of your file, then norm_cast might solve this goal for you.

[Kevin Buzzard]

The answer to your cast question is that Lean casts x and y on the left hand side, and then it looks at the right hand side and says "OK so it says add x y and I read from left to right, and this is supposed to be an element of zmod n so add must be addition in zmod n, so the elements must be in zmod n, oh gosh they aren't, I'd better cast them.

[Kevin Buzzard]

You have to change the right hand side to `((x + y : int) : zmod n) (or whatever the type of x and y actually are, to ensure the right kind of addition is done)