## Stream: new members

### Topic: more casting issues

#### Alex Kontorovich (Apr 21 2020 at 23:35):

Can someone please help with this proof? I realize I'm using subtraction within naturals, but nothing I've tried has worked on this...

lemma z (n m :ℕ ): 1 + (↑m - ↑n)= (1 + ↑m) - ↑n :=
begin
sorry,
end


Thanks!

#### Dan Stanescu (Apr 22 2020 at 00:25):

@Alex Kontorovich I could make this work with some effort. You can probably trim this down to half the size by working on the goal instead of G, and I can bet someone with more experience can prove it in a couple lines or so.

lemma z (n m :ℕ ): 1 + ((m:ℤ) - (n:ℤ)) = (1 + (m:ℤ)) - (n:ℤ) :=
begin
have G : 1 + ((m:ℤ) - (n:ℤ)) = 1 + ((m:ℤ) - (n:ℤ)), refl,
rw add_comm at G {occs := occurrences.pos [1]},
have F : -↑n = (-1:ℤ)*↑n, norm_num,
have E : ↑m - ↑n = ↑m + (-1:ℤ)*↑n, norm_num, linarith,
rw E at G {occs := occurrences.pos [2]},
set zn := (-1:ℤ)*↑n with hzn,
have D : 1 + (↑m + zn) = 1 + ↑m + zn, linarith,
rw D at G,
rw ← F at G,
exact G,
end


Without the casts it wouldn't be valid, of course:

#eval 1 + (0-1)    --  1
#eval (1+0) - 1    -- 0


#### Alex Kontorovich (Apr 22 2020 at 00:33):

Amazing, thank you! (Glad I wasn't missing something trivial...)

#### Dan Stanescu (Apr 22 2020 at 00:36):

These casting problems have a tendency to be tough because they're so counter-intuitive for most of us!

#### Bryan Gin-ge Chen (Apr 22 2020 at 00:43):

If you're willing to use mathlib:

import tactic

lemma z (n m :ℕ ): 1 + ((m:ℤ) - (n:ℤ)) = (1 + (m:ℤ)) - (n:ℤ) :=
by ring


#### Alex J. Best (Apr 22 2020 at 00:56):

If you are casting to any add_group this is the lemma add_sub in mathlib

lemma z (n m :ℕ ): 1 + ((↑m:ℤ) - ↑n)= (1 + ↑m) - ↑n := add_sub 1 (↑ m) (↑ n)


and by library_search should find it for you.

Last updated: Dec 20 2023 at 11:08 UTC