have inj_f : Function.Injective f := by
  intros a b heq
  simp only [f] at heq
  have unique_fac := two_pow_three_pow_unique_factorization heq
  rw [←Prod.eq_iff_fst_eq_snd_eq] at unique_fac
  exact SetCoe.ext unique_fac
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
⊢ ∃ f, Function.Injective f
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
inj_f : Function.Injective f
⊢ ∃ f, Function.Injective f