isPrimePow_def in N

Stream: new members

[Ralf Stephan]

How does the code in docs#Nat/Factorization/PrimePow manage to use isPrimePow_def? I tried a similar variable line but still fail to unify:

variable {R : Type*} [CommMonoidWithZero R] (p : R)
theorem h (m n: ℕ) (hn: n > 1): 0 < m ∧ 2 ^ m = n → IsPrimePow n := by
  apply (isPrimePow_def n).mpr

tactic 'apply' failed, failed to unify
  (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → IsPrimePow n
with
  0 < m ∧ 2 ^ m = n → IsPrimePow n
m n : ℕ
hn : n > 1
⊢ 0 < m ∧ 2 ^ m = n → IsPrimePow n

[Ruben Van de Velde]

First use intro

[Ralf Stephan]

Ok thanks, and after that I use 2...

[Ralf Stephan]

This works now. Is it too clumsy?

theorem h {m n : ℕ}: 0 < m ∧ 2 ^ m = n → IsPrimePow n := by
  intro hh
  apply (isPrimePow_def n).mpr
  use 2
  obtain ⟨h1, h2⟩ := hh
  have hp2: Prime 2 := by refine Nat.prime_iff.mp Nat.prime_two
  exact ⟨m, hp2, h1, h2⟩

[Kevin Buzzard]

import Mathlib

-- move hh left of the colon and split it up into pieces in the statement
-- because this is more idiomatic in type theory.
theorem h {m n : ℕ} (h1 : 0 < m) (h2 : 2 ^ m = n) : IsPrimePow n := by
  -- more idiomatic than `apply foo.mpr` is just `rw [foo]`
  rw [isPrimePow_def]
  -- `by` takes you from term mode to tactic mode; `refine` takes you from tactic
  -- mode to term mode, so they cancel out and you can delete them both.
  have hp2: Prime 2 := Nat.prime_iff.mp Nat.prime_two
  -- you don't need `use`, you can just make the entire term
  exact ⟨2, m, hp2, h1, h2⟩

[Ralf Stephan]

This is even shorter and shows that structurally there is "nothing" in this lemma except re-routing of arguments:

theorem h {m n : ℕ} (h1 : 0 < m) (h2 : 2 ^ m = n) : IsPrimePow n := by
  rw [isPrimePow_def]
  exact ⟨2, m, (Nat.prime_iff.mp Nat.prime_two), h1, h2⟩

[Kevin Buzzard]

I doubt you need the brackets around the proof of Prime 2.

[Ruben Van de Velde]

import Mathlib

theorem h {m n : ℕ} (h1 : 0 < m) (h2 : 2 ^ m = n) : IsPrimePow n := by
  rw [isPrimePow_def]
  exact ⟨2, m, Nat.prime_two.prime, h1, h2⟩

[Ruben Van de Velde]

Or even

import Mathlib

theorem h {m n : ℕ} (h1 : 0 < m) (h2 : 2 ^ m = n) : IsPrimePow n :=
  ⟨2, m, Nat.prime_two.prime, h1, h2⟩