## Stream: new members

### Topic: casting and adding in zmod

#### Rose Lopez (Jul 24 2020 at 22:17):

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 (Jul 24 2020 at 22:19):

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 (Jul 24 2020 at 22:21):

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 (Jul 24 2020 at 22:22):

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)

Last updated: Dec 20 2023 at 11:08 UTC