Help solving the lemma `primes_injective_on_pos`

Stream: new members

[Kajani Kaunda]

Thank you in advance for your time and help.

import Mathlib

def primes_set := { n | Nat.Prime n }

instance : Infinite primes_set := Nat.infinite_setOf_prime.to_subtype

instance : DecidablePred (fun n => n ∈ primes_set) := fun n => Nat.decidablePrime n

def primes (n : ℕ) : ℕ := if (n = 0) then 0 else Nat.Subtype.ofNat primes_set (n - 1)

-- Injectivity of the `primes` enumeration on positive indices. If i > 0, j > 0 and primes i = primes j then i = j.

lemma primes_injective_on_pos {i j : ℕ} (hi : 0 < i) (hj : 0 < j) (h : primes i = primes j) : i = j := by sorry

[Chase Norman]

import Mathlib

noncomputable def primes (n : ℕ) : ℕ := Nat.nth Nat.Prime n

lemma primes_injective : Function.Injective primes :=
  Nat.nth_injective (Nat.infinite_setOf_prime)

Does this suit your purposes?

[Kajani Kaunda]

Chase Norman said:

import Mathlib

noncomputable def primes (n : ℕ) : ℕ := Nat.nth Nat.Prime n

lemma primes_injective : Function.Injective primes :=
  Nat.nth_injective (Nat.infinite_setOf_prime)

Does this suit your purposes?

Wow!, let me check will come back to you ...

[Kajani Kaunda]

Chase Norman said:

import Mathlib

noncomputable def primes (n : ℕ) : ℕ := Nat.nth Nat.Prime n

lemma primes_injective : Function.Injective primes :=
  Nat.nth_injective (Nat.infinite_setOf_prime)

Does this suit your purposes?

Thank you for the code @Chase Norman, it helped! Much appreciated.