m n : ℤ
k : ℕ
k0 : 0 < k
h : m ^ k ∣ n ^ k
⊢ m ∣ n
m n : ℤ
k : ℕ
k0 : 0 < k
⊢ m ^ k ∣ n ^ k ↔ m ∣ n
refine' ⟨fun h => _, fun h => pow_dvd_pow_of_dvd h _⟩
no goals
m n : ℤ
k : ℕ
k0 : 0 < k
h : m ^ k ∣ n ^ k
⊢ m ∣ n
rwa [← natAbs_dvd_natAbs, ← Nat.pow_dvd_pow_iff k0, ← Int.natAbs_pow, ← Int.natAbs_pow,
  natAbs_dvd_natAbs]