refactor(data/nat/gcd): simplify proof of pow_dvd_pow_iff

Author: digama0

algebra/ring.lean

@@ -34,6 +34,7 @@ instance [semiring α] : semiring (with_zero α) :=
   ..with_zero.mul_zero_class,
   ..with_zero.monoid }
 
+attribute [refl] dvd_refl
 attribute [trans] dvd.trans
 
 section

data/nat/basic.lean

@@ -375,6 +375,10 @@ by induction n; simp [*, pow_succ, mul_assoc]
 theorem pow_dvd_pow (a : ℕ) {m n : ℕ} (h : m ≤ n) : a^m ∣ a^n :=
 by rw [← nat.add_sub_cancel' h, pow_add]; apply dvd_mul_right
 
+theorem pow_dvd_pow_of_dvd {a b : ℕ} (h : a ∣ b) : ∀ n:ℕ, a^n ∣ b^n
+| 0     := dvd_refl _
+| (n+1) := mul_dvd_mul (pow_dvd_pow_of_dvd n) h
+
 theorem mul_pow (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := 
 by induction n; simp [*, nat.pow_succ, mul_comm, mul_assoc, mul_left_comm]
 

data/nat/gcd.lean

@@ -301,32 +301,18 @@ or.elim (eq_zero_or_pos (gcd k m))
     dvd_of_mul_dvd_mul_left gpos $ by rw [←hd, ←gcd_mul_right]; exact
       dvd_gcd (dvd_mul_right _ _) H⟩)
 
-lemma dvd_of_pow_dvd_pow : ∀ {a b n : ℕ}, 0 < n → a ^ n ∣ b ^ n → a ∣ b
-| a 0     := λ n hn h, dvd_zero _
-| a (b+1) := λ n hn h,
-let d := nat.gcd a (b + 1) in
-have hd : nat.gcd a (b + 1) = d := rfl,
-  match d, hd with
-  | 0 := λ hd, (eq_zero_of_gcd_eq_zero_right hd).symm ▸ dvd_zero _
-  | 1 := λ hd,
-    begin
-      have h₁ : a ^ n = 1 := coprime.eq_one_of_dvd (coprime.pow n n hd) h,
-      have := pow_dvd_pow a hn,
-      rw [nat.pow_one, h₁] at this,
-      exact dvd.trans this (one_dvd _),
-    end
-  | (d+2) := λ hd,
-    have (b+1) / (d+2) < (b+1) := div_lt_self dec_trivial dec_trivial,
-    have ha : a = (d+2) * (a / (d+2)) :=
-      by rw [← hd, nat.mul_div_cancel' (gcd_dvd_left _ _)],
-    have hb : (b+1) = (d+2) * ((b+1) / (d+2)) :=
-      by rw [← hd, nat.mul_div_cancel' (gcd_dvd_right _ _)],
-    have a / (d+2) ∣ (b+1) / (d+2) := dvd_of_pow_dvd_pow hn $ dvd_of_mul_dvd_mul_left
-      (show (d + 2) ^ n > 0, from pos_pow_of_pos _ dec_trivial)
-      (by rwa [← nat.mul_pow, ← nat.mul_pow, ← ha, ← hb]),
-    by rw [ha, hb];
-    exact mul_dvd_mul_left _ this
-  end
-using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf psigma.snd⟩]}
+theorem pow_dvd_pow_iff {a b n : ℕ} (n0 : 0 < n) : a ^ n ∣ b ^ n ↔ a ∣ b :=
+begin
+  refine ⟨λ h, _, λ h, pow_dvd_pow_of_dvd h _⟩,
+  cases eq_zero_or_pos (gcd a b) with g0 g0,
+  { simp [eq_zero_of_gcd_eq_zero_right g0, dvd_zero] },
+  rcases exists_coprime g0 with ⟨a', b', co, h₁, h₂⟩,
+  generalize_hyp : gcd a b = g at g0 h₁ h₂, substs a b,
+  rw [mul_pow, mul_pow] at h,
+  replace h := dvd_of_mul_dvd_mul_right (pos_pow_of_pos _ g0) h,
+  have := pow_dvd_pow a' n0,
+  rw [pow_one, (co.pow n n).eq_one_of_dvd h] at this,
+  simp [eq_one_of_dvd_one this]
+end
 
 end nat