Usage of elim_cast

Stream: new members

[rory]

I'm trying to prove this

theorem cor8 (p : ℕ) (a b : ℤ):
nat.prime p ∧ ↑p ∣ a*b → (↑p ∣ a) ∨ (↑p ∣ b) :=
begin
 intros hp,
 apply (iff.elim_left (nat.prime.dvd_mul hp.left)),
 -- goal not match
 -- have this (p ∣ a) ∨ (p ∣ b)
end

But I'm not sure how to do the coercion from nat to int

[rory]

I'm guessing elim_cast is what I need, but I'm not sure how to use it : (

[Johan Commelin]

There is the norm_cast tactic, but I don't think it will work here.

[Johan Commelin]

nat.prime.dvd_mul is a lemma about natural numbers, you want something for integers

[Johan Commelin]

What you need is a lemma saying that ↑p is an irreducible (or prime) element in ℤ. I think we have such a lemma in the library

[Kevin Buzzard]

That's a good way to do it.

[Johan Commelin]

@rory https://github.com/leanprover-community/mathlib/blob/81a31ca4a8c0287bf0b0ce40f1a0df16543b7abe/src/algebra/gcd_domain.lean#L571

[rory]

Fore future reference, I eventually solve it like this.

theorem cor8 (p : ℕ) (a b : ℤ):
nat.prime p ∧ ↑p ∣ a*b → (↑p ∣ a) ∨ (↑p ∣ b) :=
begin
 intros hp,
 have h₁ : prime ↑p,
 apply iff.elim_left nat.prime_iff_prime_int hp.left,
 apply prime.div_or_div,
 exact h₁,
 exact hp.right
end

I haven't figure out how to clean it, so maybe I will re-edit this in the future.