Fix

Author: urkud

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,26 +79,24 @@ 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 -/
 lemma real.pow_sum_div_card_le_sum_pow {α : Type*} {s : finset α} {f : α → ℝ} (n : ℕ)
   (hf : ∀ a ∈ s, 0 ≤ f a) : (∑ x in s, f x) ^ (n + 1) / s.card ^ n ≤ ∑ x in s, (f x) ^ (n + 1) :=
 begin
-  by_cases hs0 : s = ∅,
-  { simp_rw [hs0, finset.sum_empty, zero_pow' _ (nat.succ_ne_zero n), zero_div] },
-  { have hs : s.card ≠ 0 := hs0 ∘ finset.card_eq_zero.1,
-    have hs' : (s.card : ℝ) ≠ 0 := (nat.cast_ne_zero.2 hs),
-    have hs'' : 0 < (s.card : ℝ) := nat.cast_pos.2 (nat.pos_of_ne_zero hs),
+  rcases s.eq_empty_or_nonempty with rfl | hs,
+  { simp_rw [finset.sum_empty, zero_pow' _ (nat.succ_ne_zero n), zero_div] },
+  { have hs0 : 0 < (s.card : ℝ) := nat.cast_pos.2 hs.card_pos,
     suffices : (∑ x in s, f x / s.card) ^ (n + 1) ≤ ∑ x in s, (f x ^ (n + 1) / s.card),
     by rwa [← finset.sum_div, ← finset.sum_div, div_pow, pow_succ' (s.card : ℝ),
-        ← div_div, div_le_iff hs'', div_mul, div_self hs', div_one] at this,
+        ← div_div, div_le_iff hs0, div_mul, div_self hs0.ne', div_one] at this,
     have := @convex_on.map_sum_le ℝ ℝ ℝ α _ _ _ _ _ _ (set.Ici 0) (λ x, x ^ (n + 1)) s
       (λ _, 1 / s.card) (coe ∘ f) (convex_on_pow (n + 1)) _ _ (λ i hi, set.mem_Ici.2 (hf i hi)),
     { simpa only [inv_mul_eq_div, one_div, algebra.id.smul_eq_mul] using this },
     { simp only [one_div, inv_nonneg, nat.cast_nonneg, implies_true_iff] },
-    { simpa only [one_div, finset.sum_const, nsmul_eq_mul] using mul_inv_cancel hs' }}
+    { simpa only [one_div, finset.sum_const, nsmul_eq_mul] using mul_inv_cancel hs0.ne' } }
 end
 
 lemma nnreal.pow_sum_div_card_le_sum_pow {α : Type*} (s : finset α) (f : α → ℝ≥0) (n : ℕ) :

src/analysis/p_series.lean

@@ -48,7 +48,7 @@ begin
   suffices : (∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k) ≤ (2 ^ n) • f (2 ^ n),
   { rw [sum_range_succ, ← sum_Ico_consecutive],
     exact add_le_add ihn this,
-    exacts [n.one_le_two_pow, nat.pow_le_pow_of_le_right zero_lt_two n.le_succ] },
+    exacts [n.one_le_two_pow, nat.pow_le_pow_of_le_right two_ne_zero n.le_succ] },
   have : ∀ k ∈ Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ f (2 ^ n) :=
     λ k hk, hf (pow_pos zero_lt_two _) (mem_Ico.mp hk).1,
   convert sum_le_sum this,
@@ -70,7 +70,7 @@ begin
   { rw [sum_range_succ, ← sum_Ico_consecutive],
     exact add_le_add ihn this,
     exacts [add_le_add_right n.one_le_two_pow _,
-      add_le_add_right (nat.pow_le_pow_of_le_right zero_lt_two n.le_succ) _] },
+      add_le_add_right (nat.pow_le_pow_of_le_right two_ne_zero n.le_succ) _] },
   have : ∀ k ∈ Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f (2 ^ (n + 1)) ≤ f k :=
     λ k hk, hf (n.one_le_two_pow.trans_lt $ (nat.lt_succ_of_le le_rfl).trans_le (mem_Ico.mp hk).1)
       (nat.le_of_lt_succ $ (mem_Ico.mp hk).2),

src/analysis/special_functions/trigonometric/bounds.lean

@@ -107,8 +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_ne_zero]
-        using (sin_pos hy).ne' },
+      simpa only [ne.def, sub_eq_self, pow_eq_zero_iff two_ne_zero] using (sin_pos hy).ne' },
     rwa [lt_inv, inv_one],
     { exact zero_lt_one },
     simpa only [sq, mul_self_pos] using this.ne' },

src/combinatorics/simple_graph/regularity/bound.lean

@@ -45,7 +45,7 @@ local notation `a` := (card α/P.parts.card - m * 4^P.parts.card : ℕ)
 
 lemma m_pos [nonempty α] (hPα : P.parts.card * 16^P.parts.card ≤ card α) : 0 < m :=
 nat.div_pos ((nat.mul_le_mul_left _ $ nat.pow_le_pow_of_le_left (by norm_num) _).trans hPα) $
-  step_bound_pos (P.parts_nonempty $ univ_nonempty.ne_empty).card_pos
+  (step_bound_pos (P.parts_nonempty $ univ_nonempty.ne_empty).card_pos).ne'
 
 lemma m_coe_pos [nonempty α] (hPα : P.parts.card * 16^P.parts.card ≤ card α) : (0 : ℝ) < m :=
 nat.cast_pos.2 $ m_pos hPα

src/data/nat/pow.lean

@@ -32,6 +32,10 @@ pow_lt_pow H h
 lemma pow_lt_pow_succ {p : ℕ} (h : 1 < p) (n : ℕ) : p^n < p^(n+1) :=
 pow_lt_pow_of_lt_right h n.lt_succ_self
 
+lemma le_self_pow {n : ℕ} (hn : n ≠ 0) : ∀ m : ℕ, m ≤ m ^ n
+| 0 := zero_le _
+| (m + 1) := _root_.le_self_pow dec_trivial hn
+
 lemma lt_pow_self {p : ℕ} (h : 1 < p) : ∀ n : ℕ, n < p ^ n
 | 0 := by simp [zero_lt_one]
 | (n+1) := calc

src/field_theory/separable_degree.lean

@@ -111,9 +111,9 @@ theorem contraction_degree_eq_or_insep
 begin
   wlog hm : m ≤ m' := le_total m m' using [m m' g g', m' m g' g],
   obtain ⟨s, rfl⟩ := exists_add_of_le hm,
-  rw [pow_add, expand_mul, expand_inj (pow_pos (ne_zero.pos q) m)] at h_expand,
+  rw [pow_add, expand_mul, expand_inj (pow_ne_zero _ (ne_zero.ne q))] at h_expand,
   subst h_expand,
-  rcases is_unit_or_eq_zero_of_separable_expand q s (ne_zero.pos q) hg with h | rfl,
+  rcases is_unit_or_eq_zero_of_separable_expand q s (ne_zero.ne q) hg with h | rfl,
   { rw [nat_degree_expand, nat_degree_eq_zero_of_is_unit h, zero_mul] },
   { rw [nat_degree_expand, pow_zero, mul_one] },
 end

src/number_theory/bertrand.lean

@@ -145,8 +145,7 @@ lemma central_binom_le_of_no_bertrand_prime (n : ℕ) (n_big : 2 < n)
   (no_prime : ¬∃ (p : ℕ), nat.prime p ∧ n < p ∧ p ≤ 2 * n) :
   central_binom n ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
 begin
-  have n_pos : 0 < n := (nat.zero_le _).trans_lt n_big,
-  have n2_pos : 1 ≤ 2 * n := mul_pos (zero_lt_two' ℕ) n_pos,
+  have hn20 : 2 * n ≠ 0 := mul_ne_zero two_ne_zero n_big.ne_bot,
   let S := (finset.range (2 * n / 3 + 1)).filter nat.prime,
   let f := λ x, x ^ n.central_binom.factorization x,
   have : ∏ (x : ℕ) in S, f x = ∏ (x : ℕ) in finset.range (2 * n / 3 + 1), f x,
@@ -157,11 +156,11 @@ begin
     ← finset.prod_filter_mul_prod_filter_not S (≤ sqrt (2 * n))],
   apply mul_le_mul',
   { refine (finset.prod_le_prod'' (λ p hp, (_ : f p ≤ 2 * n))).trans _,
-    { exact pow_factorization_choose_le (mul_pos two_pos n_pos) },
+    { exact pow_factorization_choose_le hn20 },
     have : (finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n),
     { rw [card_Icc, nat.add_sub_cancel] },
     rw finset.prod_const,
-    refine pow_le_pow n2_pos ((finset.card_le_of_subset (λ x hx, _)).trans this.le),
+    refine nat.pow_le_pow_of_le_right hn20 ((finset.card_le_of_subset (λ x hx, _)).trans_eq this),
     obtain ⟨h1, h2⟩ := finset.mem_filter.1 hx,
     exact finset.mem_Icc.mpr ⟨(finset.mem_filter.1 h1).2.one_lt.le, h2⟩ },
   { refine le_trans _ (primorial_le_4_pow (2 * n / 3)),

src/number_theory/liouville/basic.lean

@@ -65,7 +65,7 @@ begin
   rw [← int.coe_nat_mul, ← int.coe_nat_pow, ← int.coe_nat_mul, int.coe_nat_lt] at a1,
   -- Recall this is by contradiction: we obtained the inequality `b * q ≤ x * q ^ (b + 1)`, so
   -- we are done.
-  exact not_le.mpr a1 (nat.mul_lt_mul_pow_succ (int.coe_nat_pos.mp ap) (int.coe_nat_lt.mp q1)).le,
+  exact a1.not_le (nat.mul_lt_mul_pow_succ (nat.cast_pos.1 ap).ne' (nat.cast_lt.1 q1)).le,
 end
 
 open polynomial metric set real ring_hom

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -351,9 +351,9 @@ lemma nat_degree_cyclotomic (n : ℕ) (R : Type*) [ring R] [nontrivial R] :
 by rw [nat_degree, degree_cyclotomic, with_bot.unbot'_coe]
 
 /-- The degree of `cyclotomic n R` is positive. -/
-lemma degree_cyclotomic_pos (n : ℕ) (R : Type*) (hpos : 0 < n) [ring R] [nontrivial R] :
-  0 < (cyclotomic n R).degree := by
-{ rw degree_cyclotomic n R, exact_mod_cast (nat.totient_pos hpos) }
+lemma degree_cyclotomic_pos (n : ℕ) (R : Type*) (h0 : n ≠ 0) [ring R] [nontrivial R] :
+  0 < (cyclotomic n R).degree :=
+by rwa [degree_cyclotomic n R, with_bot.coe_pos, nat.totient_pos]
 
 open finset
 
@@ -640,11 +640,9 @@ begin
   intros n m hnm,
   simp only at hnm,
   rcases eq_or_ne n 0 with rfl | hzero,
-  { rw [cyclotomic_zero] at hnm,
-    replace hnm := congr_arg nat_degree hnm,
-    rw [nat_degree_one, nat_degree_cyclotomic] at hnm,
-    by_contra,
-    exact (nat.totient_pos (zero_lt_iff.2 (ne.symm h))).ne hnm },
+  { apply_fun nat_degree at hnm,
+    rwa [cyclotomic_zero, nat_degree_one, nat_degree_cyclotomic, eq_comm,
+      nat.totient_eq_zero, eq_comm] at hnm },
   { haveI := ne_zero.mk hzero,
     rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm,
     replace hnm := map_injective (int.cast_ring_hom R) int.cast_injective hnm,
@@ -873,7 +871,7 @@ begin
       ((cyclotomic.monic n ℤ).expand hp.ne_zero).is_primitive).2 _,
     rw [polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int],
     refine is_coprime.mul_dvd (cyclotomic.is_coprime_rat (λ h, _)) _ _,
-    { exact hp.ne_one (mul_left_cancel₀ hn h) },
+    { exact hn (eq_zero_of_mul_eq_self_right hp.ne_one h) },
     { have h0 : n * p ≠ 0 := mul_ne_zero hn hp.ne_zero,
       have hprim := complex.is_primitive_root_exp _ h0,
       rw [cyclotomic_eq_minpoly_rat hprim h0],

src/ring_theory/polynomial/cyclotomic/eval.lean

@@ -171,7 +171,7 @@ begin
   rw [finset.prod_singleton, ht, mul_left_comm, mul_comm, ←mul_assoc, mul_assoc] at this,
   have : (p ^ (padic_val_nat p n) * p : ℤ) ∣ n := ⟨_, this⟩,
   simp only [←pow_succ', ←int.nat_abs_dvd_iff_dvd, int.nat_abs_of_nat, int.nat_abs_pow] at this,
-  exact pow_succ_padic_val_nat_not_dvd hn'.ne' this,
+  exact pow_succ_padic_val_nat_not_dvd hn' this,
   { rintro x - y - hxy,
     apply nat.succ_injective,
     exact nat.pow_right_injective hp.two_le hxy }
@@ -230,7 +230,13 @@ begin
     simpa only [hq'.le, real.coe_to_nnreal', max_eq_left, sub_nonneg] using hex },
 end
 
-lemma cyclotomic_eval_lt_sub_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ n) (hq' : 1 < q) :
+lemma sub_one_pow_totient_le_cyclotomic_eval {q : ℝ} (hq' : 1 < q) :
+  ∀ n, (q - 1) ^ totient n ≤ (cyclotomic n ℝ).eval q
+| 0 := by simp only [totient_zero, pow_zero, cyclotomic_zero, eval_one]
+| 1 := by simp only [totient_one, pow_one, cyclotomic_one, eval_sub, eval_X, eval_one]
+| (n + 2) := (sub_one_pow_totient_lt_cyclotomic_eval dec_trivial hq').le
+
+lemma cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ n) (hq' : 1 < q) :
   (cyclotomic n ℝ).eval q < (q + 1) ^ totient n :=
 begin
   have hn : 0 < n := pos_of_gt hn',
@@ -259,9 +265,9 @@ begin
       rintro rfl,
       exact hn.ne' (hζ.unique is_primitive_root.zero) },
     have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne _, h.2⟩,
-    rw [←complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this,
-    rw this at hζ,
-    linarith [hζ.unique $ is_primitive_root.neg_one 0 two_ne_zero.symm],
+    { rw [←complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this,
+      rw this at hζ,
+      linarith [hζ.unique $ is_primitive_root.neg_one 0 two_ne_zero.symm] },
     { contrapose! hζ₀,
       ext; simp [hζ₀, h.2] } },
   have : ¬eval ↑q (cyclotomic n ℂ) = 0,
@@ -295,33 +301,28 @@ begin
     exact ⟨ζ, hζ, by simp [hhζ]⟩ },
 end
 
-lemma sub_one_lt_nat_abs_cyclotomic_eval {n : ℕ} {q : ℕ} (hn' : 1 < n) (hq' : q ≠ 1) :
-  q - 1 < ((cyclotomic n ℤ).eval ↑q).nat_abs :=
+lemma cyclotomic_eval_le_add_one_pow_totient {q : ℝ} (hq' : 1 < q) :
+  ∀ n, (cyclotomic n ℝ).eval q ≤ (q + 1) ^ totient n
+| 0 := by simp
+| 1 := by simp [add_assoc, add_nonneg, zero_le_one]
+| 2 := by simp
+| (n + 3) := (cyclotomic_eval_lt_add_one_pow_totient dec_trivial hq').le
+
+lemma sub_one_pow_totient_lt_nat_abs_cyclotomic_eval {n : ℕ} {q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) :
+  (q - 1) ^ totient n < ((cyclotomic n ℤ).eval ↑q).nat_abs :=
 begin
-  rcases q with _ | _ | q,
-  iterate 2
-  { rw [pos_iff_ne_zero, ne.def, int.nat_abs_eq_zero],
-    intro h,
-    have := degree_eq_one_of_irreducible_of_root (cyclotomic.irreducible hn'.ne_bot) h,
-    rw [degree_cyclotomic, with_top.coe_eq_one, totient_eq_one_iff] at this,
-    rcases this with rfl|rfl; simpa using h },
-  suffices : (q.succ : ℝ) < (eval (↑q + 1 + 1) (cyclotomic n ℤ)).nat_abs,
-  { exact_mod_cast this },
-  calc _ ≤ ((q + 2 - 1) ^ n.totient : ℝ) : _
-    ...  < _ : _,
-  { norm_num,
-    convert pow_mono (by simp : 1 ≤ (q : ℝ) + 1) (totient_pos (pos_of_gt hn') : 1 ≤ n.totient),
-    { simp },
-    { ring }, },
-  convert sub_one_pow_totient_lt_cyclotomic_eval (show 2 ≤ n, by linarith)
-                          (show (1 : ℝ) < q + 2, by {norm_cast, linarith}),
-  norm_cast,
-  erw cyclotomic.eval_apply (q + 2 : ℤ) n (algebra_map ℤ ℝ),
-  simp only [int.coe_nat_succ, eq_int_cast],
-  norm_cast,
-  rw [int.coe_nat_abs_eq_normalize, int.normalize_of_nonneg],
-  simp only [int.coe_nat_succ],
-  exact cyclotomic_nonneg n (by linarith),
+  rcases hq.lt_or_lt.imp_left nat.lt_one_iff.mp with rfl | hq',
+  { rw [zero_tsub, zero_pow (nat.totient_pos.2 hn'.ne_bot), pos_iff_ne_zero, int.nat_abs_ne_zero,
+      nat.cast_zero, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hn'],
+    exact one_ne_zero },
+  rw [← @nat.cast_lt ℝ, nat.cast_pow, nat.cast_sub hq'.le, nat.cast_one, int.cast_nat_abs],
+  refine (sub_one_pow_totient_lt_cyclotomic_eval hn' (nat.one_lt_cast.2 hq')).trans_le _,
+  exact (cyclotomic.eval_apply (q : ℤ) n (algebra_map ℤ ℝ)).trans_le (le_abs_self _)
 end
 
+lemma sub_one_lt_nat_abs_cyclotomic_eval {n : ℕ} {q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) :
+  q - 1 < ((cyclotomic n ℤ).eval ↑q).nat_abs :=
+calc q - 1 ≤ (q - 1) ^ totient n : nat.le_self_pow (nat.totient_ne_zero.2 hn'.ne_bot) _
+... < ((cyclotomic n ℤ).eval ↑q).nat_abs : sub_one_pow_totient_lt_nat_abs_cyclotomic_eval hn' hq
+
 end polynomial

src/topology/instances/add_circle.lean

@@ -256,9 +256,10 @@ lemma exists_gcd_eq_one_of_is_of_fin_add_order {u : add_circle p} (h : is_of_fin
 begin
   rcases eq_or_ne u 0 with rfl | hu, { exact ⟨0, by simp⟩, },
   set n := add_order_of u,
-  have hn : n ≠ 0 := (add_order_of_pos' h).ne',
+  have hn : 0 < n := add_order_of_pos' h,
+  have hn' : n ≠ 0 := hn.ne',
   have hn₀ : (n : 𝕜) ≠ 0, by assumption_mod_cast,
-  let x := (equiv_Ico p u : 𝕜),
+  let x := (equiv_Ico p 0 u : 𝕜),
   have hxu : (x : add_circle p) = u := (equiv_Ico p 0).symm_apply_apply u,
   have hx₀ : 0 < (add_order_of (x : add_circle p)), { rw ← hxu at h, exact add_order_of_pos' h, },
   have hx₁ : 0 < x,
@@ -271,8 +272,8 @@ begin
   have hux : ↑(↑m / ↑n * p) = u,
   { rw [← hxu, ← mul_div_right_comm, hm, mul_comm _ x, mul_div_cancel x hn₀], },
   refine ⟨m, (_ : gcd m n = 1), (_ : m < n), hux⟩,
-  { have := gcd_mul_add_order_of_div_eq p m hn,
-    rwa [hux, nat.mul_left_eq_self_iff hn] at this, },
+  { have := gcd_mul_add_order_of_div_eq p m hn',
+    rwa [hux, nat.mul_left_eq_self_iff hn'] at this, },
   { have : n • x < n • p := smul_lt_smul_of_pos _ hn,
     rwa [nsmul_eq_mul, nsmul_eq_mul, ← hm, mul_lt_mul_right hp.out, nat.cast_lt] at this,
     simpa [zero_add] using (equiv_Ico p 0 u).2.2, },