Unable to apply dvd_sub

Stream: new members

[Ben Nale]

I want to show that gcd(a,b) \mid a-b
this is what I typed into lean:
have h3: nat.gcd a b ∣ a - b ,
cases nat.gcd_dvd a b,
apply dvd_sub,

However, I get an error under apply saying that unable to unify m_1 \mid m_2-m_3 even though the goal is in this exact form.
Note that using the exact same technique and div_add I am able to prove the addition version of this lemma.
image.png

[Kenny Lau]

the typeclasses are different

[Kenny Lau]

dvd_sub is for commutative rings

[Kenny Lau]

but nat is only a commutative semiring

[Kenny Lau]

the subtraction in nat is different

[Ben Nale]

Oh so I could say (nat.gcd a b : \Z ) \mid (a-b :\Z)

[Kevin Buzzard]

Yes

[Kevin Buzzard]

If you type #check @dvd_sub you can see all the type classes required to make the lemma work, and you can see if nat has them by trying to construct them with apply_instance, e.g. example : comm_ring \N := by apply_instance, which of course fails because nat isn't a ring.

[Ben Nale]

Oh the apply works now. Though using cases on nat.gcd_dvd a b produces to hypotheses with no arrows. But we need arrows

[Ben Nale]

image.png

[Kevin Buzzard]

the arrow is just the function from nat to int. You might be able to get rid of it with the norm_cast tactic.

[Ben Nale]

Nice. It works and I get it. Thanks.

[Ben Nale]

have h3: (nat.gcd a b :ℤ ) ∣ (a - b :ℤ) ,
cases nat.gcd_dvd a b,
apply dvd_sub,
norm_cast,
exact left,
norm_cast,
exact right,

[Ben Nale]

no goals :)

[Kenny Lau]

#backticks