case a
a b : ℤ
⊢ ↑(natAbs (EuclideanDomain.gcd a b)) ∣ ↑(gcd a b)

case a
a b : ℤ
⊢ ↑(gcd a b) ∣ ↑(natAbs (EuclideanDomain.gcd a b))
a b : ℤ
⊢ natAbs (EuclideanDomain.gcd a b) = gcd a b
apply Nat.dvd_antisymm <;> rw [← Int.coe_nat_dvd]
case a
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ ↑(gcd a b)
case a
a b : ℤ
⊢ ↑(natAbs (EuclideanDomain.gcd a b)) ∣ ↑(gcd a b)
rw [Int.natAbs_dvd]
no goals
case a
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ ↑(gcd a b)
exact Int.dvd_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)
case a
a b : ℤ
⊢ ↑(gcd a b) ∣ EuclideanDomain.gcd a b
case a
a b : ℤ
⊢ ↑(gcd a b) ∣ ↑(natAbs (EuclideanDomain.gcd a b))
rw [Int.dvd_natAbs]
no goals
case a
a b : ℤ
⊢ ↑(gcd a b) ∣ EuclideanDomain.gcd a b
exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left _ _) (Int.gcd_dvd_right _ _)