a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
⊢ a ∣ b
a b n : ℕ
n0 : 0 < n
⊢ a ^ n ∣ b ^ n ↔ a ∣ b
refine' ⟨fun h => _, fun h => pow_dvd_pow_of_dvd h _⟩
case inl
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b = 0
⊢ a ∣ b

case inr
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b > 0
⊢ a ∣ b
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
⊢ a ∣ b
cases' Nat.eq_zero_or_pos (gcd a b) with g0 g0
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : (a' * g) ^ n ∣ (b' * g) ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
case inr
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b > 0
⊢ a ∣ b
rcases exists_coprime' g0 with ⟨g, a', b', g0', co, rfl, rfl⟩
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : a' ^ n * g ^ n ∣ b' ^ n * g ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : (a' * g) ^ n ∣ (b' * g) ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
rw [mul_pow, mul_pow] at h
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
⊢ a' * g ∣ b' * g
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : a' ^ n * g ^ n ∣ b' ^ n * g ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
replace h := Nat.dvd_of_mul_dvd_mul_right (pow_pos g0' _) h
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ^ succ 0 ∣ a' ^ n
⊢ a' * g ∣ b' * g
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
⊢ a' * g ∣ b' * g
have := pow_dvd_pow a' n0
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ∣ 1
⊢ a' * g ∣ b' * g
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ^ succ 0 ∣ a' ^ n
⊢ a' * g ∣ b' * g
rw [pow_one, (co.pow n n).eq_one_of_dvd h] at this
no goals
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ∣ 1
⊢ a' * g ∣ b' * g
simp [eq_one_of_dvd_one this]
no goals
case inl
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b = 0
⊢ a ∣ b
simp [eq_zero_of_gcd_eq_zero_right g0]