## Stream: new members

### Topic: Usage of elim_cast

#### rory (Nov 05 2019 at 14:13):

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 (Nov 05 2019 at 14:13):

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

#### Johan Commelin (Nov 05 2019 at 14:22):

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

#### Johan Commelin (Nov 05 2019 at 14:23):

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

#### Johan Commelin (Nov 05 2019 at 14:23):

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 (Nov 05 2019 at 14:24):

That's a good way to do it.

#### rory (Nov 05 2019 at 15:22):

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.

Last updated: May 11 2021 at 22:14 UTC