no goals
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
simp_rw [← Int.coe_nat_modEq_iff, ← modEq_iff_int_modEq, ← @int_cast_modEq_int_cast α,
  Int.cast_ofNat]