chore(data/nat/prime): golf some proofs (#10599)

src/data/nat/prime.lean

@@ -317,17 +317,11 @@ begin
   { intro h,
     have ub := min_fac_le_of_dvd (le_refl 2) h,
     have lb := min_fac_pos n,
-    -- If `interval_cases` and `norm_num` were already available here,
-    -- this would be easy and pleasant.
-    -- But they aren't, so it isn't.
-    cases h : n.min_fac with m,
-    { rw h at lb, cases lb, },
-    { cases m with m,
-      { simp at h, subst h, cases h with n h, cases n; cases h, },
-      { cases m with m,
-        { refl, },
-        { rw h at ub,
-          cases ub with _ ub, cases ub with _ ub, cases ub, } } } }
+    apply ub.eq_or_lt.resolve_right (λ h', _),
+    have := le_antisymm (nat.succ_le_of_lt lb) (lt_succ_iff.mp h'),
+    rw [eq_comm, nat.min_fac_eq_one_iff] at this,
+    subst this,
+    exact not_lt_of_le (le_of_dvd zero_lt_one h) one_lt_two }
 end
 
 end min_fac
@@ -358,21 +352,18 @@ have np : n ≤ p, from le_of_not_ge $ λ h,
 ⟨p, np, pp⟩
 
 lemma prime.eq_two_or_odd {p : ℕ} (hp : prime p) : p = 2 ∨ p % 2 = 1 :=
-(nat.mod_two_eq_zero_or_one p).elim
-  (λ h, or.inl ((hp.2 2 (dvd_of_mod_eq_zero h)).resolve_left dec_trivial).symm)
-  or.inr
+p.mod_two_eq_zero_or_one.imp_left
+  (λ h, ((hp.2 2 (dvd_of_mod_eq_zero h)).resolve_left dec_trivial).symm)
 
 theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, prime k → k ∣ m → ¬ k ∣ n) : coprime m n :=
 begin
-  cases nat.eq_zero_or_pos (gcd m n) with g0 g1,
-  { rw [eq_zero_of_gcd_eq_zero_left g0, eq_zero_of_gcd_eq_zero_right g0] at H,
-    exfalso,
+  have g1 : 1 ≤ gcd m n,
+  { refine nat.succ_le_of_lt (pos_iff_ne_zero.mpr (λ g0, _)),
+    rw [eq_zero_of_gcd_eq_zero_left g0, eq_zero_of_gcd_eq_zero_right g0] at H,
     exact H 2 prime_two (dvd_zero _) (dvd_zero _) },
-  apply eq.symm,
-  change 1 ≤ _ at g1,
-  apply (lt_or_eq_of_le g1).resolve_left,
-  intro g2,
-  obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2,
+  rw [coprime_iff_gcd_eq_one, eq_comm],
+  refine g1.lt_or_eq.resolve_left (λ g2, _),
+  obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd (succ_le_of_lt g2),
   apply H p hp; apply dvd_trans hpdvd,
   { exact gcd_dvd_left _ _ },
   { exact gcd_dvd_right _ _ }
@@ -502,15 +493,17 @@ theorem prime.not_dvd_mul {p m n : ℕ} (pp : prime p)
 mt pp.dvd_mul.1 $ by simp [Hm, Hn]
 
 theorem prime.dvd_of_dvd_pow {p m n : ℕ} (pp : prime p) (h : p ∣ m^n) : p ∣ m :=
-by induction n with n IH;
-   [exact pp.not_dvd_one.elim h,
-    by { rw pow_succ at h, exact (pp.dvd_mul.1 h).elim id IH } ]
+begin
+  induction n with n IH,
+  { exact pp.not_dvd_one.elim h },
+  { rw pow_succ at h, exact (pp.dvd_mul.1 h).elim id IH }
+end
 
 lemma prime.pow_dvd_of_dvd_mul_right {p n a b : ℕ} (hp : p.prime) (h : p ^ n ∣ a * b)
   (hpb : ¬ p ∣ b) : p ^ n ∣ a :=
 begin
   induction n with n ih,
-  { simp },
+  { simp only [one_dvd, pow_zero] },
   { rw [pow_succ'] at *,
     rcases ih ((dvd_mul_right _ _).trans h) with ⟨c, rfl⟩,
     rw [mul_assoc] at h,
@@ -588,38 +581,30 @@ by rw [pp.dvd_iff_not_coprime]; apply em
 
 lemma coprime_of_lt_prime {n p} (n_pos : 0 < n) (hlt : n < p) (pp : prime p) :
   coprime p n :=
-begin
-   cases coprime_or_dvd_of_prime pp n,
-   { exact h },
-   { exfalso, exact lt_le_antisymm hlt (le_of_dvd n_pos h) },
-end
+(coprime_or_dvd_of_prime pp n).resolve_right $ λ h, lt_le_antisymm hlt (le_of_dvd n_pos h)
 
 lemma eq_or_coprime_of_le_prime {n p} (n_pos : 0 < n) (hle : n ≤ p) (pp : prime p) :
   p = n ∨ coprime p n :=
-begin
-  by_cases p = n,
-  { exact or.inl h, },
-  { right, exact coprime_of_lt_prime n_pos ((ne.symm h).le_iff_lt.mp hle) pp },
-end
+hle.eq_or_lt.imp eq.symm (λ h, coprime_of_lt_prime n_pos h pp)
 
 theorem dvd_prime_pow {p : ℕ} (pp : prime p) {m i : ℕ} : i ∣ (p^m) ↔ ∃ k ≤ m, i = p^k :=
 begin
-  induction m with m IH generalizing i, {simp [pow_succ, le_zero_iff] at *},
+  induction m with m IH generalizing i, { simp },
   by_cases p ∣ i,
   { cases h with a e, subst e,
     rw [pow_succ, nat.mul_dvd_mul_iff_left pp.pos, IH],
     split; intro h; rcases h with ⟨k, h, e⟩,
     { exact ⟨succ k, succ_le_succ h, by rw [e, pow_succ]; refl⟩ },
     cases k with k,
     { apply pp.not_dvd_one.elim,
-      simp at e, rw ← e, apply dvd_mul_right },
+      rw [← pow_zero, ← e], apply dvd_mul_right },
     { refine ⟨k, le_of_succ_le_succ h, _⟩,
       rwa [mul_comm, pow_succ', nat.mul_left_inj pp.pos] at e } },
   { split; intro d,
     { rw (pp.coprime_pow_of_not_dvd h).eq_one_of_dvd d,
-      exact ⟨0, zero_le _, rfl⟩ },
-    { rcases d with ⟨k, l, e⟩,
-      rw e, exact pow_dvd_pow _ l } }
+      exact ⟨0, zero_le _, (pow_zero p).symm⟩ },
+    { rcases d with ⟨k, l, rfl⟩,
+      exact pow_dvd_pow _ l } }
 end
 
 /--
@@ -721,24 +706,23 @@ lemma perm_of_prod_eq_prod : ∀ {l₁ l₂ : list ℕ}, prod l₁ = prod l₂ 
 /-- **Fundamental theorem of arithmetic**-/
 lemma factors_unique {n : ℕ} {l : list ℕ} (h₁ : prod l = n) (h₂ : ∀ p ∈ l, prime p) :
   l ~ factors n :=
-have hn : 0 < n := nat.pos_of_ne_zero $ λ h, begin
-  rw h at *, clear h,
-  induction l with a l hi,
-  { exact absurd h₁ dec_trivial },
-  { rw prod_cons at h₁,
-    exact nat.mul_ne_zero (ne_of_lt (prime.pos (h₂ a (mem_cons_self _ _)))).symm
-      (hi (λ p hp, h₂ p (mem_cons_of_mem _ hp))) h₁ }
-end,
-perm_of_prod_eq_prod (by rwa prod_factors hn) h₂ (@prime_of_mem_factors _)
+begin
+  refine perm_of_prod_eq_prod _ h₂ (λ p, prime_of_mem_factors),
+  rw h₁,
+  refine (prod_factors (nat.pos_of_ne_zero _)).symm,
+  rintro rfl,
+  rw prod_eq_zero_iff at h₁,
+  exact prime.ne_zero (h₂ 0 h₁) rfl,
+end
 
 lemma prime.factors_pow {p : ℕ} (hp : p.prime) (n : ℕ) :
   (p ^ n).factors = list.repeat p n :=
 begin
   symmetry,
   rw ← list.repeat_perm,
   apply nat.factors_unique (list.prod_repeat p n),
-  { intros q hq,
-    rwa eq_of_mem_repeat hq },
+  intros q hq,
+  rwa eq_of_mem_repeat hq,
 end
 
 /-- For positive `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b` -/
@@ -850,11 +834,10 @@ end
 lemma min_fac_helper_0 (n : ℕ) (h : 0 < n) : min_fac_helper n 1 :=
 begin
   refine ⟨zero_lt_one, lt_of_le_of_ne _ min_fac_ne_bit0.symm⟩,
-  refine @lt_of_le_of_ne ℕ _ _ _ (nat.min_fac_pos _) _,
-  intro e,
-  have := nat.min_fac_prime _,
-  { rw ← e at this, exact nat.not_prime_one this },
-  { exact ne_of_gt (nat.bit1_lt h) }
+  rw nat.succ_le_iff,
+  refine lt_of_le_of_ne (nat.min_fac_pos _) (λ e, nat.not_prime_one _),
+  rw e,
+  exact nat.min_fac_prime (nat.bit1_lt h).ne',
 end
 
 lemma min_fac_helper_1 {n k k' : ℕ} (e : k + 1 = k')
@@ -889,8 +872,8 @@ end
 
 lemma min_fac_helper_4 (n k : ℕ) (hd : bit1 n % bit1 k = 0)
   (h : min_fac_helper n k) : nat.min_fac (bit1 n) = bit1 k :=
-by rw ← nat.dvd_iff_mod_eq_zero at hd; exact
-le_antisymm (nat.min_fac_le_of_dvd (nat.bit1_lt h.1) hd) h.2
+by { rw ← nat.dvd_iff_mod_eq_zero at hd,
+  exact le_antisymm (nat.min_fac_le_of_dvd (nat.bit1_lt h.1) hd) h.2 }
 
 lemma min_fac_helper_5 (n k k' : ℕ) (e : bit1 k * bit1 k = k')
   (hd : bit1 n < k') (h : min_fac_helper n k) : nat.min_fac (bit1 n) = bit1 n :=