refactor(*): assume ≠0 instead of 0 < _

archive/100-theorems-list/37_solution_of_cubic.lean

@@ -46,7 +46,7 @@ variables {ω p q r s t : K}
 
 lemma cube_root_of_unity_sum (hω : is_primitive_root ω 3) : 1 + ω + ω^2 = 0 :=
 begin
-  convert hω.is_root_cyclotomic (nat.succ_pos _),
+  convert hω.is_root_cyclotomic (nat.succ_ne_zero _),
   simp only [cyclotomic_prime, eval_geom_sum],
   simp [finset.sum_range_succ]
 end

archive/100-theorems-list/70_perfect_numbers.lean

@@ -45,8 +45,7 @@ begin
         (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)),
     sigma_two_pow_eq_mersenne_succ],
   { simp [pr, nat.prime_two, sigma_one_apply] },
-  { apply mul_pos (pow_pos _ k) (mersenne_pos (nat.succ_pos k)),
-    norm_num }
+  { exact mul_pos (pow_pos two_pos k) (mersenne_pos k.succ_ne_zero) }
 end
 
 lemma ne_zero_of_prime_mersenne (k : ℕ) (pr : (mersenne (k + 1)).prime) :
@@ -60,10 +59,10 @@ theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).pr
   even ((2 ^ k) * mersenne (k + 1)) :=
 by simp [ne_zero_of_prime_mersenne k pr] with parity_simps
 
-lemma eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) :
+lemma eq_two_pow_mul_odd {n : ℕ} (hn : n ≠ 0) :
   ∃ (k m : ℕ), n = 2 ^ k * m ∧ ¬ even m :=
 begin
-  have h := (multiplicity.finite_nat_iff.2 ⟨nat.prime_two.ne_one, hpos⟩),
+  have h := (multiplicity.finite_nat_iff.2 ⟨nat.prime_two.ne_one, hn⟩),
   cases multiplicity.pow_multiplicity_dvd h with m hm,
   use [(multiplicity 2 n).get h, m],
   refine ⟨hm, _⟩,
@@ -81,7 +80,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (p
   ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=
 begin
   have hpos := perf.2,
-  rcases eq_two_pow_mul_odd hpos with ⟨k, m, rfl, hm⟩,
+  rcases eq_two_pow_mul_odd hpos.ne' with ⟨k, m, rfl, hm⟩,
   use k,
   rw even_iff_two_dvd at hm,
   rw [perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
@@ -90,7 +89,7 @@ begin
   rcases nat.coprime.dvd_of_dvd_mul_left
     (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (dvd.intro _ perf) with ⟨j, rfl⟩,
   rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf,
-  have h := mul_left_cancel₀ (ne_of_gt (mersenne_pos (nat.succ_pos _))) perf,
+  have h := mul_left_cancel₀ (ne_of_gt (mersenne_pos (nat.succ_ne_zero _))) perf,
   rw [sigma_one_apply, sum_divisors_eq_sum_proper_divisors_add_self, ← succ_mersenne, add_mul,
     one_mul, add_comm] at h,
   have hj := add_left_cancel h,

archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean

@@ -190,7 +190,7 @@ begin
     { calc b < b + 1        : lt_add_one b
       ...    ≤ (m + 1).sqrt : by simpa only [nat.le_sqrt, pow_two] using nat.le_of_dvd hm' hbm
       ...    ≤ x.sqrt       : nat.sqrt_le_sqrt (nat.succ_le_iff.mpr hm.1) },
-    { exact hm.2 p ⟨hp.1, hp.2.trans (nat.dvd_of_pow_dvd one_le_two hbm)⟩ } },
+    { exact hm.2 p ⟨hp.1, hp.2.trans (nat.dvd_of_pow_dvd two_ne_zero hbm)⟩ } },
 
   have h2 : card M₂ ≤ nat.sqrt x,
   { rw ← card_range (nat.sqrt x), apply card_le_of_subset, simp [M₂, M] },

archive/imo/imo1969_q1.lean

@@ -65,7 +65,7 @@ polynomial_not_prime (show 1 < 2+b, by linarith)
 /-- `a_choice` is a strictly monotone function; this is easily proven by chaining together lemmas
 in the `strict_mono` namespace. -/
 lemma a_choice_strict_mono : strict_mono a_choice :=
-((strict_mono_id.const_add 2).nat_pow (dec_trivial : 0 < 4)).const_mul (dec_trivial : 0 < 4)
+((strict_mono_id.const_add 2).nat_pow four_ne_zero).const_mul (dec_trivial : 0 < 4)
 
 /-- We conclude by using the fact that `a_choice` is an injective function from the natural numbers
 to the set `good_nats`. -/

archive/imo/imo2001_q2.lean

@@ -44,7 +44,7 @@ begin
   rw div_le_div_iff hdenom (sqrt_pos.mpr hsqrt),
   conv_lhs { rw [pow_succ', mul_assoc] },
   apply mul_le_mul_of_nonneg_left _ (pow_pos ha 3).le,
-  apply le_of_pow_le_pow _ hdenom.le zero_lt_two,
+  apply le_of_pow_le_pow _ hdenom.le two_ne_zero,
   rw [mul_pow, sq_sqrt hsqrt.le, ← sub_nonneg],
   calc  (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
       = 2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 +

archive/imo/imo2006_q3.lean

@@ -75,7 +75,7 @@ have this : _ :=
           div_le_div_of_le four_pow_four_pos.le $ pow_le_pow_of_le_left
             (add_nonneg (mul_nonneg zero_lt_three.le (sq_nonneg _)) hs)
             (add_le_add_right rhs_ineq _) _,
-le_of_pow_le_pow _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) nat.succ_pos' $
+le_of_pow_le_pow _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) two_ne_zero $
   calc  (32 * |x * y * z * s|) ^ 2
       = 32 * ((2 * s^2) * (16 * x^2 * y^2 * (x + y)^2)) :
           by rw [mul_pow, sq_abs, hz]; ring

archive/imo/imo2008_q4.lean

@@ -24,8 +24,7 @@ The desired theorem is that either `f = λ x, x` or `f = λ x, 1/x`
 open real
 
 lemma abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : |x| = 1 :=
-by rw [← pow_left_inj (abs_nonneg x) zero_le_one (pos_iff_ne_zero.2 hn), one_pow, pow_abs, h,
-  abs_one]
+by rw [← pow_left_inj (abs_nonneg x) zero_le_one hn, one_pow, pow_abs, h, abs_one]
 
 theorem imo2008_q4
   (f : ℝ → ℝ)

archive/imo/imo2013_q1.lean

@@ -30,7 +30,7 @@ open_locale big_operators
 lemma arith_lemma (k n : ℕ) : 0 < 2 * n + 2^k.succ :=
 calc 0 < 2                : zero_lt_two
    ... = 2^1              : (pow_one 2).symm
-   ... ≤ 2^k.succ         : nat.pow_le_pow_of_le_right zero_lt_two (nat.le_add_left 1 k)
+   ... ≤ 2^k.succ         : nat.pow_le_pow_of_le_right two_ne_zero (nat.le_add_left 1 k)
    ... ≤ 2 * n + 2^k.succ : nat.le_add_left _ _
 
 lemma prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+):

src/algebra/associated.lean

@@ -538,18 +538,18 @@ lemma associated.of_mul_right [cancel_comm_monoid_with_zero α] {a b c d : α} :
 by rw [mul_comm a, mul_comm c]; exact associated.of_mul_left
 
 lemma associated.of_pow_associated_of_prime [cancel_comm_monoid_with_zero α] {p₁ p₂ : α}
-  {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) :
+  {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : k₁ ≠ 0) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) :
   p₁ ~ᵤ p₂ :=
 begin
   have : p₁ ∣ p₂ ^ k₂,
   { rw ←h.dvd_iff_dvd_right,
-    apply dvd_pow_self _ hk₁.ne' },
+    apply dvd_pow_self _ hk₁ },
   rw ←hp₁.dvd_prime_iff_associated hp₂,
   exact hp₁.dvd_of_dvd_pow this,
 end
 
 lemma associated.of_pow_associated_of_prime' [cancel_comm_monoid_with_zero α] {p₁ p₂ : α}
-  {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₂ : 0 < k₂) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) :
+  {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₂ : k₂ ≠ 0) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) :
   p₁ ~ᵤ p₂ :=
 (h.symm.of_pow_associated_of_prime hp₂ hp₁ hk₂).symm
 
@@ -579,11 +579,11 @@ section unique_units₀
 
 variables {R : Type*} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ}
 
-lemma eq_of_prime_pow_eq (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ = p₂ ^ k₂) :
+lemma eq_of_prime_pow_eq (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : k₁ ≠ 0) (h : p₁ ^ k₁ = p₂ ^ k₂) :
   p₁ = p₂ :=
 by { rw [←associated_iff_eq] at h ⊢, apply h.of_pow_associated_of_prime hp₁ hp₂ hk₁ }
 
-lemma eq_of_prime_pow_eq' (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :
+lemma eq_of_prime_pow_eq' (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : k₂ ≠ 0) (h : p₁ ^ k₁ = p₂ ^ k₂) :
   p₁ = p₂ :=
 by { rw [←associated_iff_eq] at h ⊢, apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁ }
 

src/algebra/group_power/lemmas.lean

@@ -495,7 +495,7 @@ variables [linear_ordered_ring R] {a : R} {n : ℕ}
 le_iff_le_iff_lt_iff_lt.2 pow_bit1_neg_iff
 
 @[simp] theorem pow_bit1_nonpos_iff : a ^ bit1 n ≤ 0 ↔ a ≤ 0 :=
-by simp only [le_iff_lt_or_eq, pow_bit1_neg_iff, pow_eq_zero_iff (bit1_pos (zero_le n))]
+by simp only [le_iff_lt_or_eq, pow_bit1_neg_iff, pow_eq_zero_iff (bit1_pos (zero_le n)).ne']
 
 @[simp] theorem pow_bit1_pos_iff : 0 < a ^ bit1 n ↔ 0 < a :=
 lt_iff_lt_of_le_iff_le pow_bit1_nonpos_iff
@@ -506,9 +506,9 @@ begin
   cases le_total a 0 with ha ha,
   { cases le_or_lt b 0 with hb hb,
     { rw [← neg_lt_neg_iff, ← neg_pow_bit1, ← neg_pow_bit1],
-      exact pow_lt_pow_of_lt_left (neg_lt_neg hab) (neg_nonneg.2 hb) (bit1_pos (zero_le n)) },
+      exact pow_lt_pow_of_lt_left (neg_lt_neg hab) (neg_nonneg.2 hb) n.bit1_ne_zero },
     { exact (pow_bit1_nonpos_iff.2 ha).trans_lt (pow_bit1_pos_iff.2 hb) } },
-  { exact pow_lt_pow_of_lt_left hab ha (bit1_pos (zero_le n)) }
+  { exact pow_lt_pow_of_lt_left hab ha n.bit1_ne_zero }
 end
 
 /-- Bernoulli's inequality for `n : ℕ`, `-2 ≤ a`. -/

src/algebra/group_power/order.lean

@@ -146,17 +146,17 @@ lemma pow_mono_right (n : ℕ) : monotone (λ a : M, a ^ n) := monotone_id.pow_r
 end covariant_le_swap
 
 @[to_additive left.pow_neg]
-lemma left.pow_lt_one_of_lt [covariant_class M M (*) (<)] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) :
+lemma left.pow_lt_one_of_lt [covariant_class M M (*) (<)] {n : ℕ} {x : M} (hn : n ≠ 0) (h : x < 1) :
   x^n < 1 :=
 nat.le_induction ((pow_one _).trans_lt h) (λ n _ ih, by { rw pow_succ, exact mul_lt_one h ih }) _
-  (nat.succ_le_iff.2 hn)
+  (nat.one_le_iff_ne_zero.2 hn)
 
 @[to_additive right.pow_neg]
 lemma right.pow_lt_one_of_lt [covariant_class M M (swap (*)) (<)] {n : ℕ} {x : M}
-  (hn : 0 < n) (h : x < 1) :
+  (hn : n ≠ 0) (h : x < 1) :
   x^n < 1 :=
 nat.le_induction ((pow_one _).trans_lt h)
-  (λ n _ ih, by { rw pow_succ, exact right.mul_lt_one h ih }) _ (nat.succ_le_iff.2 hn)
+  (λ n _ ih, by { rw pow_succ, exact right.mul_lt_one h ih }) _ (nat.one_le_iff_ne_zero.2 hn)
 
 end preorder
 
@@ -235,12 +235,12 @@ by simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)
 end covariant_lt_swap
 
 @[to_additive left.nsmul_neg_iff]
-lemma left.pow_lt_one_iff [covariant_class M M (*) (<)] {n : ℕ} {x : M} (hn : 0 < n) :
+lemma left.pow_lt_one_iff [covariant_class M M (*) (<)] {n : ℕ} {x : M} (hn : n ≠ 0) :
   x^n < 1 ↔ x < 1 :=
-by { haveI := has_mul.to_covariant_class_left M, exact pow_lt_one_iff hn.ne' }
+by { haveI := has_mul.to_covariant_class_left M, exact pow_lt_one_iff hn }
 
 @[to_additive right.nsmul_neg_iff]
-lemma right.pow_lt_one_iff [covariant_class M M (swap (*)) (<)] {n : ℕ} {x : M} (hn : 0 < n) :
+lemma right.pow_lt_one_iff [covariant_class M M (swap (*)) (<)] {n : ℕ} {x : M} (hn : n ≠ 0) :
   x^n < 1 ↔ x < 1 :=
 ⟨λ H, not_le.mp $ λ k, H.not_le $ by { haveI := has_mul.to_covariant_class_right M,
     exact right.one_le_pow_of_le k }, right.pow_lt_one_of_lt hn⟩
@@ -335,12 +335,12 @@ end ordered_semiring
 section strict_ordered_semiring
 variables [strict_ordered_semiring R] {a x y : R} {n m : ℕ}
 
-lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n
-| 0 hn := hn.false.elim
+lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, n ≠ 0 → x ^ n < y ^ n
+| 0 hn := (hn rfl).elim
 | (n + 1) _ := by simpa only [pow_succ'] using
     mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx
 
-lemma strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
+lemma strict_mono_on_pow (hn : n ≠ 0) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
 λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
 
 lemma pow_strict_mono_right (h : 1 < a) : strict_mono (λ n : ℕ, a ^ n) :=
@@ -429,14 +429,14 @@ one_le_pow_iff_of_nonneg ha (nat.succ_ne_zero _)
 lemma one_lt_sq_iff {a : R} (ha : 0 ≤ a) : 1 < a^2 ↔ 1 < a :=
 one_lt_pow_iff_of_nonneg ha (nat.succ_ne_zero _)
 
-@[simp] theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) :
+@[simp] theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hn : n ≠ 0) :
   x ^ n = y ^ n ↔ x = y :=
-(@strict_mono_on_pow R _ _ Hnpos).eq_iff_eq Hxpos Hypos
+(@strict_mono_on_pow R _ _ Hn).eq_iff_eq Hxpos Hypos
 
 lemma lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
 lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
 
-lemma le_of_pow_le_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (hn : 0 < n) (h : a ^ n ≤ b ^ n) : a ≤ b :=
+lemma le_of_pow_le_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (hn : n ≠ 0) (h : a ^ n ≤ b ^ n) : a ≤ b :=
 le_of_not_lt $ λ h1, not_le_of_lt (pow_lt_pow_of_lt_left h1 hb hn) h
 
 @[simp] lemma sq_eq_sq {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b :=
@@ -494,14 +494,14 @@ by simpa only [sq] using abs_mul_self x
 
 theorem sq_lt_sq : x ^ 2 < y ^ 2 ↔ |x| < |y| :=
 by simpa only [sq_abs]
-  using (@strict_mono_on_pow R _ _ two_pos).lt_iff_lt (abs_nonneg x) (abs_nonneg y)
+  using (@strict_mono_on_pow R _ _ two_ne_zero).lt_iff_lt (abs_nonneg x) (abs_nonneg y)
 
 theorem sq_lt_sq' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 :=
 sq_lt_sq.2 (lt_of_lt_of_le (abs_lt.2 ⟨h1, h2⟩) (le_abs_self _))
 
 theorem sq_le_sq : x ^ 2 ≤ y ^ 2 ↔ |x| ≤ |y| :=
 by simpa only [sq_abs]
-  using (@strict_mono_on_pow R _ _ two_pos).le_iff_le (abs_nonneg x) (abs_nonneg y)
+  using (@strict_mono_on_pow R _ _ two_ne_zero).le_iff_le (abs_nonneg x) (abs_nonneg y)
 
 theorem sq_le_sq' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 :=
 sq_le_sq.2 (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))
@@ -552,7 +552,7 @@ end linear_ordered_comm_ring
 section linear_ordered_comm_monoid_with_zero
 variables [linear_ordered_comm_monoid_with_zero M] [no_zero_divisors M] {a : M} {n : ℕ}
 
-lemma pow_pos_iff (hn : 0 < n) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn]
+lemma pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn]
 
 end linear_ordered_comm_monoid_with_zero
 

src/algebra/group_power/ring.lean

@@ -56,20 +56,20 @@ begin
 end
 
 @[simp] lemma pow_eq_zero_iff [no_zero_divisors M]
-  {a : M} {n : ℕ} (hn : 0 < n) :
+  {a : M} {n : ℕ} (hn : n ≠ 0) :
   a ^ n = 0 ↔ a = 0 :=
 begin
   refine ⟨pow_eq_zero, _⟩,
   rintros rfl,
-  exact zero_pow hn,
+  exact zero_pow' _ hn,
 end
 
 lemma pow_eq_zero_iff' [no_zero_divisors M] [nontrivial M]
   {a : M} {n : ℕ} :
   a ^ n = 0 ↔ a = 0 ∧ n ≠ 0 :=
 by cases (zero_le n).eq_or_gt; simp [*, ne_of_gt]
 
-lemma pow_ne_zero_iff [no_zero_divisors M] {a : M} {n : ℕ} (hn : 0 < n) :
+lemma pow_ne_zero_iff [no_zero_divisors M] {a : M} {n : ℕ} (hn : n ≠ 0) :
   a ^ n ≠ 0 ↔ a ≠ 0 :=
 (pow_eq_zero_iff hn).not
 
@@ -84,7 +84,7 @@ instance ne_zero.pow [no_zero_divisors M] {x : M} [ne_zero x] {n : ℕ} :
   ne_zero (x ^ n) := ⟨pow_ne_zero n ne_zero.out⟩
 
 theorem sq_eq_zero_iff [no_zero_divisors M] {a : M} : a ^ 2 = 0 ↔ a = 0 :=
-pow_eq_zero_iff two_pos
+pow_eq_zero_iff two_ne_zero
 
 @[simp] lemma zero_pow_eq_zero [nontrivial M] {n : ℕ} : (0 : M) ^ n = 0 ↔ 0 < n :=
 begin

src/algebra/is_prime_pow.lean

@@ -75,7 +75,7 @@ begin
   refine iff.symm ⟨λ ⟨p, _, k, _, hp, hk, hn⟩, ⟨p, k, hp, hk, hn⟩, _⟩,
   rintro ⟨p, k, hp, hk, rfl⟩,
   refine ⟨p, _, k, (nat.lt_pow_self hp.one_lt _).le, hp, hk, rfl⟩,
-  simpa using nat.pow_le_pow_of_le_right hp.pos hk,
+  simpa using nat.pow_le_pow_of_le_right hp.ne_zero hk,
 end
 
 instance {n : ℕ} : decidable (is_prime_pow n) :=

src/algebra/order/sub/canonical.lean

@@ -274,6 +274,8 @@ by rw [pos_iff_ne_zero, ne.def, tsub_eq_zero_iff_le]
 
 lemma tsub_pos_of_lt (h : a < b) : 0 < b - a := tsub_pos_iff_not_le.mpr h.not_le
 
+lemma tsub_ne_zero (h : a < b) : b - a ≠ 0 := (tsub_pos_of_lt h).ne'
+
 lemma tsub_lt_of_lt (h : a < b) : a - c < b := lt_of_le_of_lt tsub_le_self h
 
 namespace add_le_cancellable

src/analysis/asymptotics/asymptotics.lean

@@ -1181,7 +1181,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/complex/basic.lean

@@ -143,7 +143,7 @@ subtype.ext $ by simp only [coe_nnnorm, norm_int, int.norm_eq_abs]
 lemma nnnorm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :
   ‖ζ‖₊ = 1 :=
 begin
-  refine (@pow_left_inj nnreal _ _ _ _ zero_le' zero_le' hn.bot_lt).mp _,
+  refine (@pow_left_inj nnreal _ _ _ _ zero_le' zero_le' hn).mp _,
   rw [←nnnorm_pow, h, nnnorm_one, one_pow],
 end
 

src/analysis/complex/roots_of_unity.lean

@@ -55,24 +55,24 @@ begin
   { rintro ⟨i, -, hi, rfl⟩, exact is_primitive_root_exp_of_coprime i n hn hi },
   intro h,
   obtain ⟨i, hi, rfl⟩ :=
-    (is_primitive_root_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one (nat.pos_of_ne_zero hn),
-  refine ⟨i, hi, ((is_primitive_root_exp n hn).pow_iff_coprime (nat.pos_of_ne_zero hn) i).mp h, _⟩,
+    (is_primitive_root_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one hn,
+  refine ⟨i, hi, ((is_primitive_root_exp n hn).pow_iff_coprime hn i).mp h, _⟩,
   rw [← exp_nat_mul],
   congr' 1,
   field_simp [hn0, mul_comm (i : ℂ)]
 end
 
 /-- The complex `n`-th roots of unity are exactly the
 complex numbers of the form `e ^ (2 * real.pi * complex.I * (i / n))` for some `i < n`. -/
-lemma mem_roots_of_unity (n : ℕ+) (x : units ℂ) :
+lemma mem_roots_of_unity (n : ℕ+) (x : ℂˣ) :
   x ∈ roots_of_unity n ℂ ↔ (∃ i < (n : ℕ), exp (2 * π * I * (i / n)) = x) :=
 begin
   rw [mem_roots_of_unity, units.ext_iff, units.coe_pow, units.coe_one],
   have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast (n.ne_zero),
   split,
   { intro h,
     obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x,
-    { simpa only using (is_primitive_root_exp n n.ne_zero).eq_pow_of_pow_eq_one h n.pos },
+    { simpa only using (is_primitive_root_exp n n.ne_zero).eq_pow_of_pow_eq_one h n.ne_zero },
     refine ⟨i, hi, _⟩,
     rw [← H, ← exp_nat_mul],
     congr' 1,

src/analysis/complex/upper_half_plane/metric.lean

@@ -177,7 +177,7 @@ begin
   have hr₀' : 0 ≤ w.im * sinh r, from mul_nonneg w.im_pos.le (sinh_nonneg_iff.2 hr₀),
   have hzw₀ : 0 < 2 * z.im * w.im, from mul_pos (mul_pos two_pos z.im_pos) w.im_pos,
   simp only [← cosh_strict_mono_on.cmp_map_eq dist_nonneg hr₀,
-    ← (@strict_mono_on_pow ℝ _ _ two_pos).cmp_map_eq dist_nonneg hr₀', dist_coe_center_sq],
+    ← (@strict_mono_on_pow ℝ _ _ two_ne_zero).cmp_map_eq dist_nonneg hr₀', dist_coe_center_sq],
   rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add],
 end
 

src/analysis/convex/specific_functions.lean

@@ -79,7 +79,7 @@ begin
   apply strict_mono_on.strict_convex_on_of_deriv (convex_Ici _) (continuous_on_pow _),
   rw [deriv_pow', interior_Ici],
   exact λ x (hx : 0 < x) y hy hxy, mul_lt_mul_of_pos_left (pow_lt_pow_of_lt_left hxy hx.le $
-    nat.sub_pos_of_lt hn) (nat.cast_pos.2 $ zero_lt_two.trans_le hn),
+    (nat.sub_pos_of_lt hn).ne') (nat.cast_pos.2 $ zero_lt_two.trans_le hn),
 end
 
 /-- Specific case of Jensen's inequality for sums of powers -/

src/analysis/normed/field/basic.lean

@@ -493,7 +493,7 @@ lemma norm_map_one_of_pow_eq_one [monoid β] (φ : β →* α) {x : β} {k : ℕ
   ‖φ x‖ = 1 :=
 begin
   rw [← pow_left_inj, ← norm_pow, ← map_pow, h, map_one, norm_one, one_pow],
-  exacts [norm_nonneg _, zero_le_one, k.pos],
+  exacts [norm_nonneg _, zero_le_one, k.ne_zero],
 end
 
 lemma norm_one_of_pow_eq_one {x : α} {k : ℕ+} (h : x ^ (k : ℕ) = 1) :