Snapshot

src/analysis/asymptotics/asymptotics.lean

@@ -1180,7 +1180,7 @@ theorem is_O_with.pow [norm_one_class R] {f : α → R} {g : α → 𝕜} (h : i
 theorem is_O_with.of_pow {n : ℕ} {f : α → 𝕜} {g : α → R} (h : is_O_with c l (f ^ n) (g ^ n))
   (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') : is_O_with c' l f g :=
 is_O_with.of_bound $ (h.weaken hc).bound.mono $ λ x hx,
-  le_of_pow_le_pow n (mul_nonneg hc' $ norm_nonneg _) hn.bot_lt $
+  le_of_pow_le_pow n (mul_nonneg hc' $ norm_nonneg _) hn $
     calc ‖f x‖ ^ n = ‖(f x) ^ n‖ : (norm_pow _ _).symm
                ... ≤ c' ^ n * ‖(g x) ^ n‖ : hx
                ... ≤ c' ^ n * ‖g x‖ ^ n :

src/analysis/normed/field/basic.lean

@@ -483,23 +483,18 @@ begin
   simp,
 end
 
-lemma norm_one_of_pow_eq_one {x : α} {k : ℕ+} (h : x ^ (k : ℕ) = 1) :
-  ‖x‖ = 1 :=
-begin
-  rw ( _ :  ‖x‖ = 1 ↔ ‖x‖₊ = 1),
-  apply (@pow_left_inj nnreal _ _ _ ↑k zero_le' zero_le' (pnat.pos k)).mp,
-  { rw [← nnnorm_pow, one_pow, h, nnnorm_one], },
-  { exact subtype.mk_eq_mk.symm, },
-end
-
-lemma norm_map_one_of_pow_eq_one [comm_monoid β] (φ : β →* α) {x : β} {k : ℕ+}
+lemma norm_map_one_of_pow_eq_one [monoid β] (φ : β →* α) {x : β} {k : ℕ+}
   (h : x ^ (k : ℕ) = 1) :
   ‖φ x‖ = 1 :=
 begin
-  have : (φ x) ^ (k : ℕ) = 1 := by rw [← monoid_hom.map_pow, h, monoid_hom.map_one],
-  exact norm_one_of_pow_eq_one this,
+  rw [← pow_left_inj, ← norm_pow, ← map_pow, h, map_one, norm_one, one_pow],
+  exacts [norm_nonneg _, zero_le_one, k.ne_zero],
 end
 
+lemma norm_one_of_pow_eq_one {x : α} {k : ℕ+} (h : x ^ (k : ℕ) = 1) :
+  ‖x‖ = 1 :=
+norm_map_one_of_pow_eq_one (monoid_hom.id α) h
+
 end normed_division_ring
 
 /-- A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖. -/

src/analysis/special_functions/japanese_bracket.lean

@@ -35,8 +35,8 @@ variables {E : Type*} [normed_add_comm_group E]
 
 lemma sqrt_one_add_norm_sq_le (x : E) : real.sqrt (1 + ‖x‖^2) ≤ 1 + ‖x‖ :=
 begin
-  refine le_of_pow_le_pow 2 (by positivity) two_pos _,
-  simp [sq_sqrt (zero_lt_one_add_norm_sq x).le, add_pow_two],
+  rw [real.sqrt_le_left (add_nonneg zero_le_one (norm_nonneg _)), add_sq, one_pow, mul_one],
+  exact add_le_add_right ((le_add_iff_nonneg_right _).2 $ mul_nonneg zero_le_two (norm_nonneg _)) _
 end
 
 lemma one_add_norm_le_sqrt_two_mul_sqrt (x : E) : 1 + ‖x‖ ≤ (real.sqrt 2) * sqrt (1 + ‖x‖^2) :=

src/analysis/special_functions/trigonometric/bounds.lean

@@ -107,7 +107,7 @@ begin
     have bd2 : cos y ^ 2 < 1,
     { apply lt_of_le_of_ne y.cos_sq_le_one,
       rw cos_sq',
-      simpa only [ne.def, sub_eq_self, pow_eq_zero_iff, nat.succ_pos']
+      simpa only [ne.def, sub_eq_self, pow_eq_zero_iff, nat.succ_ne_zero]
         using (sin_pos hy).ne' },
     rwa [lt_inv, inv_one],
     { exact zero_lt_one },

src/combinatorics/additive/behrend.lean

@@ -468,7 +468,7 @@ begin
   have hn₂ : 2 ≤ n := two_le_n_value (hN.trans' $ by norm_num1),
   have : (2 * d_value N - 1)^n ≤ N := le_N (hN.trans' $ by norm_num1),
   refine ((bound_aux hd.ne' hn₂).trans $ cast_le.2 $ roth_number_nat.mono this).trans_lt' _,
-  refine (div_lt_div_of_lt hn $ pow_lt_pow_of_lt_left (bound hN) _ _).trans_le' _,
+  refine (div_lt_div_of_lt hn $ pow_lt_pow_of_lt_left (bound hN) _ (ne_of_gt _)).trans_le' _,
   { exact div_nonneg (rpow_nonneg_of_nonneg (cast_nonneg _) _) (exp_pos _).le },
   { exact tsub_pos_of_lt (three_le_n_value $ hN.trans' $ by norm_num1) },
   rw [←rpow_nat_cast, div_rpow (rpow_nonneg_of_nonneg hN₀.le _) (exp_pos _).le, ←rpow_mul hN₀.le,

src/data/finite/card.lean

@@ -56,8 +56,8 @@ begin
   rw [nat.card_eq_fintype_card, fintype.card_pos_iff],
 end
 
-lemma finite.card_pos [finite α] [h : nonempty α] : 0 < nat.card α :=
-finite.card_pos_iff.mpr h
+lemma finite.card_pos [finite α] [h : nonempty α] : 0 < nat.card α := finite.card_pos_iff.mpr h
+lemma finite.card_ne_zero [finite α] [h : nonempty α] : nat.card α ≠ 0 := finite.card_pos.ne'
 
 namespace finite
 

src/data/nat/choose/factorization.lean

@@ -40,7 +40,7 @@ begin
   by_cases h : (choose n k).factorization p = 0, { simp [h] },
   have hp : p.prime := not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h,
   have hkn : k ≤ n, { refine le_of_not_lt (λ hnk, h _), simp [choose_eq_zero_of_lt hnk] },
-  rw [factorization_def _ hp, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
+  rw [factorization_def _ hp, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn).ne'],
   simp only [hp.multiplicity_choose hkn (lt_add_one _), part_enat.get_coe],
   refine (finset.card_filter_le _ _).trans (le_of_eq (nat.card_Ico _ _)),
 end
@@ -69,7 +69,7 @@ begin
   { exact factorization_eq_zero_of_non_prime (choose n k) hp },
   cases lt_or_le n k with hnk hkn,
   { simp [choose_eq_zero_of_lt hnk] },
-  rw [factorization_def _ hp, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
+  rw [factorization_def _ hp, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn).ne'],
   simp only [hp.multiplicity_choose hkn (lt_add_one _), part_enat.get_coe,
     finset.card_eq_zero, finset.filter_eq_empty_iff, not_le],
   intros i hi,

src/data/nat/factorization/basic.lean

@@ -436,7 +436,7 @@ begin
   apply add_left_injective d.factorization,
   simp only,
   rw [tsub_add_cancel_of_le $ (nat.factorization_le_iff_dvd hd hn).mpr h,
-      ←nat.factorization_mul (nat.div_pos (nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
+      ←nat.factorization_mul (nat.div_pos (nat.le_of_dvd hn.bot_lt h) hd).ne' hd,
       nat.div_mul_cancel h],
 end
 
@@ -487,7 +487,7 @@ and `n'` such that `n'` is not divisible by `p` and `n = p^e * n'`. -/
 lemma exists_eq_pow_mul_and_not_dvd {n : ℕ} (hn : n ≠ 0) (p : ℕ) (hp : p ≠ 1) :
   ∃ e n' : ℕ, ¬ p ∣ n' ∧ n = p ^ e * n' :=
 let ⟨a', h₁, h₂⟩ := multiplicity.exists_eq_pow_mul_and_not_dvd
-                      (multiplicity.finite_nat_iff.mpr ⟨hp, nat.pos_of_ne_zero hn⟩) in
+                      (multiplicity.finite_nat_iff.mpr ⟨hp, hn⟩) in
 ⟨_, a', h₂, h₁⟩
 
 lemma dvd_iff_div_factorization_eq_tsub {d n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) :
@@ -712,7 +712,7 @@ def rec_on_prime_pow {P : ℕ → Sort*} (h0 : P 0) (h1 : P 1)
       exact pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp },
     { exact htp },
     { apply hk _ (nat.div_lt_of_lt_mul _),
-      simp [lt_mul_iff_one_lt_left nat.succ_pos', one_lt_pow_iff htp.ne, hp.one_lt] },
+      simp [lt_mul_iff_one_lt_left nat.succ_pos', one_lt_pow_iff htp.ne', hp.one_lt] },
     end
   end
 

src/data/nat/prime.lean

@@ -291,8 +291,8 @@ theorem min_fac_pos (n : ℕ) : 0 < min_fac n :=
 by by_cases n1 : n = 1;
     [exact n1.symm ▸ dec_trivial, exact (min_fac_prime n1).pos]
 
-theorem min_fac_le {n : ℕ} (H : 0 < n) : min_fac n ≤ n :=
-le_of_dvd H (min_fac_dvd n)
+theorem min_fac_le {n : ℕ} (H : n ≠ 0) : min_fac n ≤ n :=
+le_of_dvd H.bot_lt (min_fac_dvd n)
 
 theorem le_min_fac {m n : ℕ} : n = 1 ∨ m ≤ min_fac n ↔ ∀ p, prime p → p ∣ n → m ≤ p :=
 ⟨λ h p pp d, h.elim
@@ -326,19 +326,19 @@ much faster.
 instance decidable_prime (p : ℕ) : decidable (prime p) :=
 decidable_of_iff' _ prime_def_min_fac
 
-theorem not_prime_iff_min_fac_lt {n : ℕ} (n2 : 2 ≤ n) : ¬ prime n ↔ min_fac n < n :=
-(not_congr $ prime_def_min_fac.trans $ and_iff_right n2).trans $
-  (lt_iff_le_and_ne.trans $ and_iff_right $ min_fac_le $ le_of_succ_le n2).symm
+theorem not_prime_iff_min_fac_lt {n : ℕ} (hn : 1 < n) : ¬ prime n ↔ min_fac n < n :=
+(not_congr $ prime_def_min_fac.trans $ and_iff_right hn).trans $
+  (lt_iff_le_and_ne.trans $ and_iff_right $ min_fac_le $ hn.ne_bot).symm
 
-lemma min_fac_le_div {n : ℕ} (pos : 0 < n) (np : ¬ prime n) : min_fac n ≤ n / min_fac n :=
+lemma min_fac_le_div {n : ℕ} (hn : n ≠ 0) (np : ¬ prime n) : min_fac n ≤ n / min_fac n :=
 match min_fac_dvd n with
-| ⟨0, h0⟩     := absurd pos $ by rw [h0, mul_zero]; exact dec_trivial
+| ⟨0, h0⟩     := (hn $ h0.trans (mul_zero _)).elim
 | ⟨1, h1⟩     :=
   begin
     rw mul_one at h1,
     rw [prime_def_min_fac, not_and_distrib, ← h1, eq_self_iff_true, not_true, or_false,
       not_le] at np,
-    rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), min_fac_one, nat.div_one]
+    rw [le_antisymm (le_of_lt_succ np) (one_le_iff_ne_zero.2 hn), min_fac_one, nat.div_one]
   end
 | ⟨(x+2), hx⟩ :=
   begin
@@ -351,8 +351,8 @@ end
 /--
 The square of the smallest prime factor of a composite number `n` is at most `n`.
 -/
-lemma min_fac_sq_le_self {n : ℕ} (w : 0 < n) (h : ¬ prime n) : (min_fac n)^2 ≤ n :=
-have t : (min_fac n) ≤ (n/min_fac n) := min_fac_le_div w h,
+lemma min_fac_sq_le_self {n : ℕ} (h0 : n ≠ 0) (h : ¬ prime n) : (min_fac n)^2 ≤ n :=
+have t : (min_fac n) ≤ (n / min_fac n) := min_fac_le_div h0 h,
 calc
 (min_fac n)^2 = (min_fac n) * (min_fac n)   : sq (min_fac n)
           ... ≤ (n/min_fac n) * (min_fac n) : nat.mul_le_mul_right (min_fac n) t
@@ -585,13 +585,13 @@ theorem coprime_pow_primes {p q : ℕ} (n m : ℕ) (pp : prime p) (pq : prime q)
 theorem coprime_or_dvd_of_prime {p} (pp : prime p) (i : ℕ) : coprime p i ∨ p ∣ i :=
 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) :
+lemma coprime_of_lt_prime {n p} (h0 : n ≠ 0) (hlt : n < p) (pp : prime p) :
   coprime p n :=
-(coprime_or_dvd_of_prime pp n).resolve_right $ λ h, lt_le_antisymm hlt (le_of_dvd n_pos h)
+(coprime_or_dvd_of_prime pp n).resolve_right $ λ h, lt_le_antisymm hlt (le_of_dvd h0.bot_lt h)
 
-lemma eq_or_coprime_of_le_prime {n p} (n_pos : 0 < n) (hle : n ≤ p) (pp : prime p) :
+lemma eq_or_coprime_of_le_prime {n p} (h0 : n ≠ 0) (hle : n ≤ p) (pp : prime p) :
   p = n ∨ coprime p n :=
-hle.eq_or_lt.imp eq.symm (λ h, coprime_of_lt_prime n_pos h pp)
+hle.eq_or_lt.imp eq.symm (λ h, coprime_of_lt_prime h0 h pp)
 
 theorem dvd_prime_pow {p : ℕ} (pp : prime p) {m i : ℕ} : i ∣ (p^m) ↔ ∃ k ≤ m, i = p^k :=
 by simp_rw [dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]

src/data/nat/squarefree.lean

@@ -148,24 +148,24 @@ begin
     exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, λ p pp dp, H3 _ pp (this _ pp dp)⟩ }
 end
 
-theorem min_sq_fac_aux_has_prop : ∀ {n : ℕ} k, 0 < n → ∀ i, k = 2*i+3 →
+theorem min_sq_fac_aux_has_prop : ∀ {n : ℕ} k, n ≠ 0 → ∀ i, k = 2*i+3 →
   (∀ m, prime m → m ∣ n → k ≤ m) → min_sq_fac_prop n (min_sq_fac_aux n k)
 | n k := λ n0 i e ih, begin
   rw min_sq_fac_aux,
   by_cases h : n < k*k; simp [h],
   { refine squarefree_iff_prime_squarefree.2 (λ p pp d, _),
     have := ih p pp (dvd_trans ⟨_, rfl⟩ d),
     have := nat.mul_le_mul this this,
-    exact not_le_of_lt h (le_trans this (le_of_dvd n0 d)) },
+    exact not_le_of_lt h (le_trans this (le_of_dvd n0.bot_lt d)) },
   have k2 : 2 ≤ k, { subst e, exact dec_trivial },
-  have k0 : 0 < k := lt_of_lt_of_le dec_trivial k2,
+  have k0 : k ≠ 0 := (lt_of_lt_of_le dec_trivial k2).ne',
   have IH : ∀ n', n' ∣ n → ¬ k ∣ n' → min_sq_fac_prop n' (n'.min_sq_fac_aux (k + 2)),
   { intros n' nd' nk,
-    have hn' := le_of_dvd n0 nd',
+    have hn' := le_of_dvd n0.bot_lt nd',
     refine
       have nat.sqrt n' - k < nat.sqrt n + 2 - k, from
         lt_of_le_of_lt (nat.sub_le_sub_right (nat.sqrt_le_sqrt hn') _) (nat.min_fac_lemma n k h),
-      @min_sq_fac_aux_has_prop n' (k+2) (pos_of_dvd_of_pos nd' n0)
+      @min_sq_fac_aux_has_prop n' (k+2) (pos_of_dvd_of_pos nd' n0.bot_lt).ne'
         (i+1) (by simp [e, left_distrib]) (λ m m2 d, _),
     cases nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml,
     { subst me, contradiction },
@@ -191,10 +191,10 @@ begin
   { exact ⟨prime_two, (dvd_div_iff d2).1 d4, λ p pp _, pp.two_le⟩ },
   { cases nat.eq_zero_or_pos n with n0 n0, { subst n0, cases d4 dec_trivial },
     refine min_sq_fac_prop_div _ prime_two d2 (mt (dvd_div_iff d2).2 d4) _,
-    refine min_sq_fac_aux_has_prop 3 (nat.div_pos (le_of_dvd n0 d2) dec_trivial) 0 rfl _,
+    refine min_sq_fac_aux_has_prop 3 (nat.div_pos (le_of_dvd n0 d2) dec_trivial).ne' 0 rfl _,
     refine λ p pp dp, succ_le_of_lt (lt_of_le_of_ne pp.two_le _),
     rintro rfl, contradiction },
-  { cases nat.eq_zero_or_pos n with n0 n0, { subst n0, cases d2 dec_trivial },
+  { rcases eq_or_ne n 0 with rfl | n0, { cases d2 dec_trivial },
     refine min_sq_fac_aux_has_prop _ n0 0 rfl _,
     refine λ p pp dp, succ_le_of_lt (lt_of_le_of_ne pp.two_le _),
     rintro rfl, contradiction },
@@ -213,7 +213,7 @@ begin
   have fd := min_fac_dvd m,
   exact le_trans
     (this.2.2 _ (min_fac_prime $ ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
-    (min_fac_le $ lt_of_lt_of_le dec_trivial m2),
+    (min_fac_le (lt_of_lt_of_le dec_trivial m2).ne'),
 end
 
 lemma squarefree_iff_min_sq_fac {n : ℕ} :
@@ -306,15 +306,15 @@ begin
   rw hsa at hn,
   obtain ⟨hlts, hlta⟩ := canonically_ordered_comm_semiring.mul_pos.mp hn,
   rw hsb at hsa hn hlts,
-  refine ⟨a, b, hlta, (pow_pos_iff zero_lt_two).mp hlts, hsa.symm, _⟩,
+  refine ⟨a, b, hlta, (pow_pos_iff two_ne_zero).mp hlts, hsa.symm, _⟩,
   rintro x ⟨y, hy⟩,
   rw nat.is_unit_iff,
   by_contra hx,
   refine lt_le_antisymm _ (finset.le_max' S ((b * x) ^ 2) _),
   { simp_rw [S, hsa, finset.sep_def, finset.mem_filter, finset.mem_range],
     refine ⟨lt_succ_iff.mpr (le_of_dvd hn _), _, ⟨b * x, rfl⟩⟩; use y; rw hy; ring },
   { convert lt_mul_of_one_lt_right hlts
-      (one_lt_pow 2 x zero_lt_two (one_lt_iff_ne_zero_and_ne_one.mpr ⟨λ h, by simp * at *, hx⟩)),
+      (one_lt_pow 2 x two_ne_zero (one_lt_iff_ne_zero_and_ne_one.mpr ⟨λ h, by simp * at *, hx⟩)),
     rw mul_pow },
 end
 
@@ -419,7 +419,7 @@ lemma squarefree_helper_3 (n n' k k' c : ℕ) (e : k + 1 = k')
   { rw [← hn', nat.mul_div_cancel _ k0'] },
   have k2 : 2 ≤ bit1 k := nat.succ_le_succ (bit0_pos k0),
   have pk : (bit1 k).prime,
-  { refine nat.prime_def_min_fac.2 ⟨k2, le_antisymm (nat.min_fac_le k0') _⟩,
+  { refine nat.prime_def_min_fac.2 ⟨k2, le_antisymm (nat.min_fac_le k0'.ne') _⟩,
     exact ih _ (nat.min_fac_prime (ne_of_gt k2)) (dvd_trans (nat.min_fac_dvd _) dk) },
   have dkk' : ¬ bit1 k ∣ bit1 n', {rw [nat.dvd_iff_mod_eq_zero, hc], exact ne_of_gt c0},
   have dkk : ¬ bit1 k * bit1 k ∣ bit1 n, {rwa [← nat.dvd_div_iff dk, this]},

src/data/nat/totient.lean

@@ -42,10 +42,17 @@ lemma totient_le (n : ℕ) : φ n ≤ n :=
 lemma totient_lt (n : ℕ) (hn : 1 < n) : φ n < n :=
 (card_lt_card (filter_ssubset.2 ⟨0, by simp [hn.ne', pos_of_gt hn]⟩)).trans_eq (card_range n)
 
-lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
+@[simp] lemma totient_eq_zero : ∀ {n : ℕ}, φ n = 0 ↔ n = 0
 | 0 := dec_trivial
 | 1 := by simp [totient]
-| (n+2) := λ h, card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 dec_trivial, coprime_one_right _⟩⟩
+| (n + 2) :=
+  iff_of_false (card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 dec_trivial, coprime_one_right _⟩⟩).ne'
+    (n + 1).succ_ne_zero
+
+lemma totient_ne_zero {n : ℕ} : φ n ≠ 0 ↔ n ≠ 0 := totient_eq_zero.not
+
+@[simp] lemma totient_pos {n : ℕ} : 0 < φ n ↔ n ≠ 0 :=
+pos_iff_ne_zero.trans totient_ne_zero
 
 lemma filter_coprime_Ico_eq_totient (a n : ℕ) :
   ((Ico n (n+a)).filter (coprime a)).card = totient a :=
@@ -54,17 +61,17 @@ begin
   exact periodic_coprime a,
 end
 
-lemma Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) :
+lemma Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (h0 : a ≠ 0) :
   ((Ico k (k + n)).filter (coprime a)).card ≤ totient a * (n / a + 1) :=
 begin
   conv_lhs { rw ←nat.mod_add_div n a },
   induction n / a with i ih,
   { rw ←filter_coprime_Ico_eq_totient a k,
-    simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n a_pos)],
+    simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n h0.bot_lt)],
     mono,
     refine monotone_filter_left a.coprime _,
     simp only [finset.le_eq_subset],
-    exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k), },
+    exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n h0.bot_lt)) k), },
   simp only [mul_succ],
   simp_rw ←add_assoc at ih ⊢,
   calc (filter a.coprime (Ico k (k + n % a + a * i + a))).card
@@ -354,7 +361,7 @@ lemma totient_mul_of_prime_of_dvd {p n : ℕ} (hp : p.prime) (h : p ∣ n) :
 begin
   have h1 := totient_gcd_mul_totient_mul p n,
   rw [(gcd_eq_left h), mul_assoc] at h1,
-  simpa [(totient_pos hp.pos).ne', mul_comm] using h1,
+  simpa [totient_ne_zero.2 hp.ne_zero, mul_comm] using h1,
 end
 
 lemma totient_mul_of_prime_of_not_dvd {p n : ℕ} (hp : p.prime) (h : ¬ p ∣ n) :

src/field_theory/abel_ruffini.lean

@@ -94,10 +94,9 @@ section gal_X_pow_sub_C
 
 lemma gal_X_pow_sub_one_is_solvable (n : ℕ) : is_solvable (X ^ n - 1 : F[X]).gal :=
 begin
-  rcases n.eq_zero_or_pos with rfl|hn,
+  rcases eq_or_ne n 0 with rfl|hn,
   { rw [pow_zero, sub_self],
     exact gal_zero_is_solvable },
-  have hn' : 0 < n := pos_iff_ne_zero.mpr hn,
   have hn'' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1,
   apply is_solvable_of_comm,
   intros σ τ,
@@ -124,7 +123,7 @@ begin
   { rw [hn, pow_zero, ←C_1, ←C_sub],
     exact gal_C_is_solvable (1 - a) },
   have hn' : 0 < n := pos_iff_ne_zero.mpr hn,
-  have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn' a,
+  have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn a,
   have hn''' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1,
   have mem_range : ∀ {c}, c ^ n = 1 → ∃ d, algebra_map F (X ^ n - C a).splitting_field d = c :=
     λ c hc, ring_hom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c (h.def.resolve_left hn'''

src/group_theory/schreier.lean

@@ -192,7 +192,7 @@ begin
   have h2 := card_commutator_dvd_index_center_pow (closure_commutator_representatives G),
   rw card_commutator_set_closure_commutator_representatives at h1 h2,
   rw card_commutator_closure_commutator_representatives at h2,
-  replace h1 := h1.trans (nat.pow_le_pow_of_le_right finite.card_pos
+  replace h1 := h1.trans (nat.pow_le_pow_of_le_right finite.card_ne_zero
     (rank_closure_commutator_representations_le G)),
   replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_right (mul_le_mul_right' h1 _) 1)),
   rw ← pow_succ' at h2,

src/number_theory/fermat4.lean

@@ -91,7 +91,7 @@ begin
     exact (fermat_42.mul (int.coe_nat_ne_zero.mpr (nat.prime.ne_zero hp))).mpr h.1,
   apply nat.le_lt_antisymm (h.2 _ _ _ hf),
   rw [int.nat_abs_mul, lt_mul_iff_one_lt_left, int.nat_abs_pow, int.nat_abs_of_nat],
-  { exact nat.one_lt_pow _ _ zero_lt_two (nat.prime.one_lt hp) },
+  { exact nat.one_lt_pow _ _ two_ne_zero hp.one_lt },
   { exact (nat.pos_of_ne_zero (int.nat_abs_ne_zero_of_ne_zero (ne_zero hf))) },
 end
 

src/number_theory/lucas_lehmer.lean

@@ -41,19 +41,13 @@ The tactic for certified computation of Lucas-Lehmer residues was provided by Ma
 /-- The Mersenne numbers, 2^p - 1. -/
 def mersenne (p : ℕ) : ℕ := 2^p - 1
 
-lemma mersenne_pos {p : ℕ} (h : 0 < p) : 0 < mersenne p :=
-begin
-  dsimp [mersenne],
-  calc 0 < 2^1 - 1 : by norm_num
-     ... ≤ 2^p - 1 : nat.pred_le_pred (nat.pow_le_pow_of_le_right (nat.succ_pos 1) h)
-end
+lemma mersenne_pos {p : ℕ} (h : p ≠ 0) : 0 < mersenne p :=
+tsub_pos_of_lt $ one_lt_pow one_lt_two h
 
-@[simp]
-lemma succ_mersenne (k : ℕ) : mersenne k + 1 = 2 ^ k :=
-begin
-  rw [mersenne, tsub_add_cancel_of_le],
-  exact one_le_pow_of_one_le (by norm_num) k
-end
+lemma mersenne_ne_zero {p : ℕ} (h : p ≠ 0) : mersenne p ≠ 0 := (mersenne_pos h).ne'
+
+@[simp] lemma succ_mersenne (k : ℕ) : mersenne k + 1 = 2 ^ k :=
+tsub_add_cancel_of_le $ nat.one_le_iff_ne_zero.2 $ pow_ne_zero _ two_ne_zero
 
 namespace lucas_lehmer
 
@@ -85,30 +79,27 @@ def s_mod (p : ℕ) : ℕ → ℤ
 | 0 := 4 % (2^p - 1)
 | (i+1) := ((s_mod i)^2 - 2) % (2^p - 1)
 
-lemma mersenne_int_ne_zero (p : ℕ) (w : 0 < p) : (2^p - 1 : ℤ) ≠ 0 :=
-begin
-  apply ne_of_gt, simp only [gt_iff_lt, sub_pos],
-  exact_mod_cast nat.one_lt_two_pow p w,
-end
+lemma mersenne_int_ne_zero (p : ℕ) (hp : p ≠ 0) : (2^p - 1 : ℤ) ≠ 0 :=
+sub_ne_zero.2 $ (one_lt_pow one_lt_two hp).ne'
 
-lemma s_mod_nonneg (p : ℕ) (w : 0 < p) (i : ℕ) : 0 ≤ s_mod p i :=
+lemma s_mod_nonneg (p : ℕ) (hp : p ≠ 0) (i : ℕ) : 0 ≤ s_mod p i :=
 begin
   cases i; dsimp [s_mod],
   { exact sup_eq_right.mp rfl },
-  { apply int.mod_nonneg, exact mersenne_int_ne_zero p w },
+  { apply int.mod_nonneg, exact mersenne_int_ne_zero p hp },
 end
 
 lemma s_mod_mod (p i : ℕ) : s_mod p i % (2^p - 1) = s_mod p i :=
 by cases i; simp [s_mod]
 
-lemma s_mod_lt (p : ℕ) (w : 0 < p) (i : ℕ) : s_mod p i < 2^p - 1 :=
+lemma s_mod_lt (p : ℕ) (hp : p ≠ 0) (i : ℕ) : s_mod p i < 2^p - 1 :=
 begin
   rw ←s_mod_mod,
   convert int.mod_lt _ _,
   { refine (abs_of_nonneg _).symm,
     simp only [sub_nonneg, ge_iff_le],
     exact_mod_cast nat.one_le_two_pow p, },
-  { exact mersenne_int_ne_zero p w, },
+  { exact mersenne_int_ne_zero p hp, },
 end
 
 lemma s_zmod_eq_s (p' : ℕ) (i : ℕ) : s_zmod (p'+2) i = (s i : zmod (2^(p'+2) - 1)):=
@@ -119,9 +110,9 @@ begin
 end
 
 -- These next two don't make good `norm_cast` lemmas.
-lemma int.coe_nat_pow_pred (b p : ℕ) (w : 0 < b) : ((b^p - 1 : ℕ) : ℤ) = (b^p - 1 : ℤ) :=
+lemma int.coe_nat_pow_pred (b p : ℕ) (hb : b ≠ 0) : ((b^p - 1 : ℕ) : ℤ) = (b^p - 1 : ℤ) :=
 begin
-  have : 1 ≤ b^p := nat.one_le_pow p b w,
+  have : 1 ≤ b^p := nat.one_le_pow p b hb,
   norm_cast
 end
 
@@ -145,8 +136,8 @@ begin
     intro h,
     simp [zmod.int_coe_zmod_eq_zero_iff_dvd] at h,
     apply int.eq_zero_of_dvd_of_nonneg_of_lt _ _ h; clear h,
-    apply s_mod_nonneg _ (nat.lt_of_succ_lt w),
-    exact s_mod_lt _ (nat.lt_of_succ_lt w) (p-2) },
+    apply s_mod_nonneg _ w.ne_bot,
+    exact s_mod_lt _ w.ne_bot (p-2) },
   { intro h, rw h, simp, },
 end
 
@@ -413,19 +404,14 @@ export lucas_lehmer (lucas_lehmer_test lucas_lehmer_residue)
 
 open lucas_lehmer
 
-theorem lucas_lehmer_sufficiency (p : ℕ) (w : 1 < p) : lucas_lehmer_test p → (mersenne p).prime :=
+theorem lucas_lehmer_sufficiency (p : ℕ) (hp : 1 < p) : lucas_lehmer_test p → (mersenne p).prime :=
 begin
-  let p' := p - 2,
-  have z : p = p' + 2 := (tsub_eq_iff_eq_add_of_le w.nat_succ_le).mp rfl,
-  have w : 1 < p' + 2 := (nat.lt_of_sub_eq_succ rfl),
+  obtain ⟨p, rfl⟩ : ∃ p', p = p' + 2 := le_iff_exists_add'.mp hp.nat_succ_le,
   contrapose,
   intros a t,
-  rw z at a,
-  rw z at t,
-  have h₁ := order_ineq p' t,
-  have h₂ := nat.min_fac_sq_le_self (mersenne_pos (nat.lt_of_succ_lt w)) a,
-  have h := lt_of_lt_of_le h₁ h₂,
-  exact not_lt_of_ge (nat.sub_le _ _) h,
+  have h₁ := order_ineq p t,
+  have h₂ := nat.min_fac_sq_le_self (mersenne_ne_zero hp.ne_bot) a,
+  exact h₁.not_le (h₂.trans (nat.sub_le _ _))
 end
 
 -- Here we calculate the residue, very inefficiently, using `dec_trivial`. We can do much better.

src/number_theory/multiplicity.lean

@@ -375,21 +375,21 @@ begin
   { exact hn },
   { exact (nat.sub_pos_of_lt hyx).ne' },
   { linarith },
-  { simp only [tsub_pos_iff_lt, pow_lt_pow_of_lt_left hyx (@zero_le' _ y _) hn] }
+  { exact (tsub_pos_of_lt $ nat.pow_lt_pow_of_lt_left hyx hn).ne' }
 end
 
 variables {p : ℕ} [hp : fact p.prime] (hp1 : odd p)
 include hp hp1
 
-lemma pow_sub_pow (hyx : y < x) (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : 0 < n) :
+lemma pow_sub_pow (hyx : y < x) (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : n ≠ 0) :
   padic_val_nat p (x ^ n - y ^ n) = padic_val_nat p (x - y) + padic_val_nat p n :=
 begin
   rw [←part_enat.coe_inj, nat.cast_add],
   iterate 3 { rw [padic_val_nat_def, part_enat.coe_get] },
   { exact multiplicity.nat.pow_sub_pow hp.out hp1 hxy hx n },
   { exact hn },
-  { exact nat.sub_pos_of_lt hyx },
-  { exact nat.sub_pos_of_lt (nat.pow_lt_pow_of_lt_left hyx hn) }
+  { exact (nat.sub_pos_of_lt hyx).ne' },
+  { exact (nat.sub_pos_of_lt (nat.pow_lt_pow_of_lt_left hyx hn)).ne' }
 end
 
 lemma pow_add_pow (hxy : p ∣ x + y) (hx : ¬p ∣ x) {n : ℕ} (hn : odd n) :
@@ -399,10 +399,10 @@ begin
   { have := dvd_zero p, contradiction },
   rw [←part_enat.coe_inj, nat.cast_add],
   iterate 3 { rw [padic_val_nat_def, part_enat.coe_get] },
-  { exact multiplicity.nat.pow_add_pow hp.out hp1 hxy hx hn },
-  { exact (odd.pos hn) },
-  { simp only [add_pos_iff, nat.succ_pos', or_true] },
-  { exact (nat.lt_add_left _ _ _ (pow_pos y.succ_pos _)) }
+  exacts [multiplicity.nat.pow_add_pow hp.out hp1 hxy hx hn,
+    hn.pos.ne',
+    (add_pos_iff.2 (or.inr y.succ_pos)).ne',
+    (nat.lt_add_left _ _ _ (pow_pos y.succ_pos _)).ne']
 end
 
 end padic_val_nat

src/number_theory/padics/padic_numbers.lean

@@ -774,7 +774,7 @@ theorem norm_rat_le_one : ∀ {q : ℚ} (hq : ¬ p ∣ q.denom), ‖(q : ℚ_[p]
       apply inv_le_one,
       { norm_cast,
         apply one_le_pow,
-        exact hp.1.pos }
+        exact hp.1.ne_zero }
     end
 
 theorem norm_int_le_one (z : ℤ) : ‖(z : ℚ_[p])‖ ≤ 1 :=

src/number_theory/padics/padic_val.lean

@@ -459,7 +459,7 @@ begin
   obtain ⟨k, hk, rfl⟩ := ht,
   rw [finset.mem_erase, nat.mem_divisors],
   refine ⟨_, (pow_dvd_pow p $ succ_le_iff.2 hk).trans pow_padic_val_nat_dvd, hn⟩,
-  exact (nat.one_lt_pow _ _ k.succ_pos hp.out.one_lt).ne'
+  exact (nat.one_lt_pow _ _ k.succ_ne_zero hp.out.one_lt).ne'
 end
 
 end padic_val_nat

src/number_theory/pell.lean

@@ -683,25 +683,20 @@ theorem matiyasevic {a k x y} : (∃ a1 : 1 < a, xn a1 k = x ∧ yn a1 k = y) 
   end
 end⟩⟩
 
-lemma eq_pow_of_pell_lem {a y k} (a1 : 1 < a) (ypos : 0 < y) : 0 < k → y^k < a →
+lemma eq_pow_of_pell_lem {a y k} (hy0 : y ≠ 0) (hk0 : k ≠ 0) (hyk : y^k < a) :
   (↑(y^k) : ℤ) < 2*a*y - y*y - 1 :=
-have y < a → a + (y*y + 1) ≤ 2*a*y, begin
-  intro ya, induction y with y IH, exact absurd ypos (lt_irrefl _),
-  cases nat.eq_zero_or_pos y with y0 ypos,
-  { rw y0, simpa [two_mul], },
-  { rw [nat.mul_succ, nat.mul_succ, nat.succ_mul y],
-    have : y + nat.succ y ≤ 2 * a,
-    { change y + y < 2 * a, rw ← two_mul,
-      exact mul_lt_mul_of_pos_left (nat.lt_of_succ_lt ya) dec_trivial },
-    have := add_le_add (IH ypos (nat.lt_of_succ_lt ya)) this,
-    convert this using 1,
-    ring }
-end, λk0 yak,
-lt_of_lt_of_le (int.coe_nat_lt_coe_nat_of_lt yak) $
-by rw sub_sub; apply le_sub_right_of_add_le;
-   apply int.coe_nat_le_coe_nat_of_le;
-   have y1 := nat.pow_le_pow_of_le_right ypos k0; simp at y1;
-   exact this (lt_of_le_of_lt y1 yak)
+have hya : y < a,
+  from pow_one y ▸ ((nat.pow_le_pow_of_le_right hy0 (nat.one_le_iff_ne_zero.2 hk0)).trans_lt hyk),
+calc (↑(y ^ k) : ℤ) < a : nat.cast_lt.2 hyk
+... ≤ a ^ 2 - (a - 1) ^ 2 - 1 :
+  begin
+    rw [sub_sq, mul_one, one_pow, sub_add, sub_sub_cancel, two_mul, sub_sub, ← add_sub,
+      le_add_iff_nonneg_right, ← bit0, sub_nonneg, ← nat.cast_two, nat.cast_le, nat.succ_le_iff],
+    exact (one_le_iff_ne_zero.2 hy0).trans_lt hya
+  end
+... ≤ a ^ 2 - (a - y) ^ 2 - 1 : have _ := hya.le,
+  by { mono*; simpa only [sub_nonneg, nat.cast_le, nat.one_le_cast, nat.one_le_iff_ne_zero] }
+... = 2*a*y - y*y - 1 : by ring
 
 theorem eq_pow_of_pell {m n k} : (n^k = m ↔
 k = 0 ∧ m = 1 ∨ 0 < k ∧
@@ -729,9 +724,9 @@ k = 0 ∧ m = 1 ∨ 0 < k ∧
   let ⟨z, ze⟩ := show w ∣ yn w1 w, from modeq_zero_iff_dvd.1 $
     (yn_modeq_a_sub_one w1 w).trans dvd_rfl.modeq_zero_nat in
   have nt : (↑(n^k) : ℤ) < 2 * a * n - n * n - 1, from
-    eq_pow_of_pell_lem a1 npos kpos $ calc
-      n^k ≤ n^w       : nat.pow_le_pow_of_le_right npos kw
-      ... < (w + 1)^w : nat.pow_lt_pow_of_lt_left (nat.lt_succ_of_le nw) wpos
+    eq_pow_of_pell_lem npos.ne' kpos.ne' $ calc
+      n^k ≤ n^w       : nat.pow_le_pow_of_le_right npos.ne' kw
+      ... < (w + 1)^w : nat.pow_lt_pow_of_lt_left (nat.lt_succ_of_le nw) wpos.ne'
       ... ≤ a         : xn_ge_a_pow w1 w,
   let ⟨t, te⟩ := int.eq_coe_of_zero_le $
     le_trans (int.coe_zero_le _) nt.le in
@@ -779,9 +774,9 @@ k = 0 ∧ m = 1 ∨ 0 < k ∧
     (yn_modeq_a_sub_one w1 j).symm.trans $
     modeq_zero_iff_dvd.2 ⟨z, yj.symm⟩,
   have nt : (↑(n^k) : ℤ) < 2 * a * n - n * n - 1, from
-    eq_pow_of_pell_lem a1 npos kpos $ calc
-      n^k ≤ n^j       : nat.pow_le_pow_of_le_right npos (le_trans kw wj)
-      ... < (w + 1)^j : nat.pow_lt_pow_of_lt_left (nat.lt_succ_of_le nw) jpos
+    eq_pow_of_pell_lem npos.ne' kpos.ne' $ calc
+      n^k ≤ n^j       : nat.pow_le_pow_of_le_right npos.ne' (le_trans kw wj)
+      ... < (w + 1)^j : nat.pow_lt_pow_of_lt_left (nat.lt_succ_of_le nw) jpos.ne'
       ... ≤ xn w1 j   : xn_ge_a_pow w1 j
       ... = a         : xj.symm,
   have na : n ≤ a, by rw xj; exact

src/number_theory/prime_counting.lean

@@ -62,7 +62,7 @@ count_nth_of_infinite _ infinite_set_of_prime _
 nth_mem_of_infinite _ infinite_set_of_prime _
 
 /-- A linear upper bound on the size of the `prime_counting'` function -/
-lemma prime_counting'_add_le {a k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) :
+lemma prime_counting'_add_le {a k : ℕ} (h0 : a ≠ 0) (h1 : a < k) (n : ℕ) :
   π' (k + n) ≤ π' k + nat.totient a * (n / a + 1) :=
 calc π' (k + n)
     ≤ ((range k).filter (prime)).card + ((Ico k (k + n)).filter (prime)).card :