Proving simple injection

Stream: new members

[Golden]

Hi all,

Can someone help me fill in this proof?

example : Injective (fun (p : Nat × Nat) => 2^(p.1) * 3^(p.2)) := by
  intro x y h
  cases x with
  | mk x1 x2 => cases y with
  | mk y1 y2 =>
  simp at h
  simp
  -- show that  2 ^ x1 * 3 ^ x2 = 2 ^ y1 * 3 ^ y2 → 2 ^ x1 = 2 ^ y1 ∧ 3 ^ x2 = 3 ^ y2
  -- essentially 2 and 3 are prime, as are natural, the only way for both sides to be equal is if
  -- each of the exponents are the same - think of it like writing the number as prod. of primes.
  -- each number has a unique representation when written as product of primes
  have h2 : 2 ^ x1 = 2 ^ y1 := by sorry
  have h3 : 3 ^ x2 = 3 ^ y2 := by sorry
  have h4 : x1 = y1 := Nat.pow_right_injective (by simp_arith) h2
  have h5 : x2 = y2 := Nat.pow_right_injective (by simp_arith) h3
  simp [h4, h5]

Also please let me know if I'm doing anything excessive that I could do more concisely.

[Kevin Buzzard]

I would do it using p-adic valuations, that seems less painful than using unique factorization. The existence of the p-adic valuation function already contains the content of the uniqueness part of unique factorization (the nontrivial part).

[Ruben Van de Velde]

And note that your code is missing imports

[Giacomo Stevanato]

Here's how I would do this:

import Mathlib
open Function

example : Injective (fun (p : Nat × Nat) => 2^(p.1) * 3^(p.2)) := by
  intro (x1, x2) (y1, y2) h
  simp at h

  let h23 n m := padicValNat_mul_pow_left (p := 2) (q := 3) n m (by decide)
  rw [←h23 x1 x2, ←h23 y1 y2, h]

  let h32 n m := padicValNat_mul_pow_right (p := 2) (q := 3) n m (by decide)
  rw [←h32 x1 x2, ←h32 y1 y2, h]

Most of the difficulty is finding the right lemmas/theorems to use, here padicValNat_mul_pow_left were basically what you needed. I feel like there should be equivalents of those for factorization too, but I couldn't find it.

Apart from this you can simplify the initial cases by using pattern matching in the intro and removing a simp that's no longer needed.