have unique_fac := two_pow_three_pow_unique_factorization heq
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
⊢ a = b
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : (↑a).1 = (↑b).1 ∧ (↑a).2 = (↑b).2
⊢ a = b