m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ gcd m n = 1
m n : ℕ+
⊢ coprime ↑m ↑n ↔ Coprime m n
unfold coprime Coprime
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ ↑(gcd m n) = ↑1
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ gcd m n = 1
rw [← coe_inj]
no goals
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ ↑(gcd m n) = ↑1
simp