Zulip Chat Archive

Stream: new members

Topic: Usage of elim_cast


view this post on Zulip 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

view this post on Zulip 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 : (

view this post on Zulip Johan Commelin (Nov 05 2019 at 14:22):

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

view this post on Zulip Johan Commelin (Nov 05 2019 at 14:23):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2019 at 14:24):

That's a good way to do it.

view this post on Zulip Johan Commelin (Nov 05 2019 at 14:27):

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

view this post on Zulip 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