Simplest way to finish

Stream: new members

[Gareth Ma]

Hi! I am wondering what is the "fastest way" to finish this off? As you can see, I am pretty close to the goal, the only difference is p | x should be p | k instead, which is handled by x | k:

k: ℕ
x: ℕ
x_div: x ∣ k
hk: ∃ (p : ℕ), nat.prime p ∧ p ∣ x
⊢ ∃ (p : ℕ), nat.prime p ∧ p ∣ k

[Mario Carneiro]

I would do something like let \<p, hp, h\> := hk in \<p, hp, h.trans x_div\>

[Gareth Ma]

Hmm, seems to give some syntax error, invalid constructor ⟨...⟩, 'tactic_state' is not an inductive type and a lot of unknown identifiers. Here is the full code if you want to try (?)

theorem exists_prime_factor {n : nat} (h : 2 ≤ n) :
  ∃ p : nat, p.prime ∧ p ∣ n :=
begin
  by_cases np : n.prime,
  {
    exact ⟨n, np, dvd_refl n⟩,
  },
  induction n using nat.strong_induction_on with k hk,
  dsimp at hk,
  rw nat.prime_def_lt at np,
  push_neg at np,
  rcases np h with ⟨x, x_lt_k, x_div_k, x_ne_one⟩,
  have x_ne_zero : x ≠ 0,
  {
    intro hx,
    rw [hx, zero_dvd_iff] at x_div_k,
    linarith,
  },
  have two_le_x : 2 ≤ x, from two_le x_ne_zero x_ne_one,
  by_cases hx : x.prime,
  {
    exact ⟨x, hx, x_div_k⟩,
  },
  {
    specialize hk x x_lt_k two_le_x hx,
    rcases hk with ⟨p, p_prime, p_div_x⟩,
    exact ⟨p, p_prime, dvd_trans p_div_x x_div_k⟩, -- works
    -- let ⟨p, hp, h⟩ := hk in ⟨p, hp, dvd_trans h x_div⟩,
  }
end

[Kyle Miller]

The fastest way is to use docs#nat.exists_prime_and_dvd :smile:

[Mario Carneiro]

that expression I gave was a term not a tactic, so you have to precede it by exact in tactic mode

[Gareth Ma]

Oh! Now it works with exact let ⟨p, hp, h⟩ := hk in ⟨p, hp, dvd_trans h x_div_k⟩. That's super cool, I will learn more about it :D Thanks!

[Gareth Ma]

Kyle Miller said:

The fastest way is to use docs#nat.exists_prime_and_dvd :smile:

Hahaha I am following https://leanprover-community.github.io/mathematics_in_lean/05_Number_Theory.html tutorial, so trying not to use existing functions :)

[Kyle Miller]

Just so you know, in mathlib you'll often see that let line written instead as

  obtain ⟨p, hp, h⟩ := hk,
  exact ⟨p, hp, dvd_trans h x_div_k⟩,

(obtain is rcases but with the pattern coming first. I personally prefer it. It's a generalization of have as well.)

[Gareth Ma]

I see, I had a similar line with rcases instead of obtain.

[Gareth Ma]

Hi, hope it is okay to ask here another question. I am trying to finish off another proof, and I essentially have p | (n + 1) and p | n, which means I should get p | 1 by applying nat.div_sub. However, linarith fails to resolve. Can you help with how I should finish?

theorem primes_infinite : ∀ n, ∃ p > n, nat.prime p :=
begin
  -- construct N = factorial(n) + 1
  -- then by contradiction prove !(p <= n)
  intro n,
  let N := nat.factorial n + 1,
  have two_le_N : 2 ≤ N, by linarith [nat.factorial_pos n],
  rcases exists_prime_factor two_le_N with ⟨p, p_prime, p_div_N⟩,
  have p_gt_N : p > n,
  {
    by_contradiction,
    push_neg at h,
    have p_div_fact_n : p ∣ nat.factorial n,
    { apply nat.dvd_factorial (nat.prime.pos p_prime) h },
    -- above, we have p | N in p_div_N and p | n.factorial in p_div_fact_N
    -- i want to prove p | 1, since N := n.factorial + 1
    -- but linarith failed to resolve
    have p_div_1 : p ∣ 1,
    {
      linarith [nat.dvd_sub (by linarith) p_div_N p_div_fact_n], -- *here*
    }
  }
end

State at here looks like

linarith failed to find a contradiction
state:
n : ℕ,
N : ℕ := n.factorial + 1,
p : ℕ,
p_div_N : p ∣ N,
p_div_fact_n : p ∣ n.factorial,
h_1 : p ∣ N - n.factorial
⊢ false

[Mario Carneiro]

you probably don't want div_sub here, but rather div_add_iff

[Mario Carneiro]

this is also not really a job for linarith, there are no inequalities in the goal

[Gareth Ma]

I can't seem to get div_add_iff to work :tear:

[Gareth Ma]

I got exact (nat.dvd_add_iff_right p_div_fact_n).2 p_div_N to work! Or exact (nat.dvd_add_right p_div_fact_n).1 p_div_N. Thanks :)