m n a b c d : ℕ
h : a ≡ b [MOD m]
h1 : gcd a m ∣ m
⊢ gcd a m = gcd b m
m n a b c d : ℕ
h : a ≡ b [MOD m]
⊢ gcd a m = gcd b m
have h1 := gcd_dvd_right a m
m n a b c d : ℕ
h : a ≡ b [MOD m]
h1 : gcd a m ∣ m
h2 : gcd b m ∣ m
⊢ gcd a m = gcd b m
m n a b c d : ℕ
h : a ≡ b [MOD m]
h1 : gcd a m ∣ m
⊢ gcd a m = gcd b m
have h2 := gcd_dvd_right b m
no goals
m n a b c d : ℕ
h : a ≡ b [MOD m]
h1 : gcd a m ∣ m
h2 : gcd b m ∣ m
⊢ gcd a m = gcd b m
exact
  dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1)
    (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)