Snapshot

Author: urkud

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