case a
m n : ℕ+
⊢ ↑(gcd m n) = ↑(gcd n m)
m n : ℕ+
⊢ gcd m n = gcd n m
apply eq
case a
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = Nat.gcd ↑n ↑m
case a
m n : ℕ+
⊢ ↑(gcd m n) = ↑(gcd n m)
simp only [gcd_coe]
no goals
case a
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = Nat.gcd ↑n ↑m
apply Nat.gcd_comm