chore(*): use zero_lt_two/two_ne_zero lemmas more (#13609)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/algebra/group_with_zero/basic.lean

@@ -141,6 +141,8 @@ not_congr mul_eq_zero_comm
 
 lemma mul_self_eq_zero : a * a = 0 ↔ a = 0 := by simp
 lemma zero_eq_mul_self : 0 = a * a ↔ a = 0 := by simp
+lemma mul_self_ne_zero : a * a ≠ 0 ↔ a ≠ 0 := not_congr mul_self_eq_zero
+lemma zero_ne_mul_self : 0 ≠ a * a ↔ a ≠ 0 := not_congr zero_eq_mul_self
 
 end
 

src/analysis/normed_space/star/spectrum.lean

@@ -68,7 +68,7 @@ end
 lemma spectral_radius_eq_nnnorm_of_star_normal [norm_one_class A] (a : A) [is_star_normal a] :
   spectral_radius ℂ a = ∥a∥₊ :=
 begin
-  refine (ennreal.pow_strict_mono (by linarith : 2 ≠ 0)).injective _,
+  refine (ennreal.pow_strict_mono two_ne_zero).injective _,
   have ha : a⋆ * a ∈ self_adjoint A,
     from self_adjoint.mem_iff.mpr (by simpa only [star_star] using (star_mul a⋆ a)),
   have heq : (λ n : ℕ, ((∥(a⋆ * a) ^ n∥₊ ^ (1 / n : ℝ)) : ℝ≥0∞))

src/data/nat/modeq.lean

@@ -405,7 +405,7 @@ lemma odd_mul_odd_div_two {m n : ℕ} (hm1 : m % 2 = 1) (hn1 : n % 2 = 1) :
   (m * n) / 2 = m * (n / 2) + m / 2 :=
 have hm0 : 0 < m := nat.pos_of_ne_zero (λ h, by simp * at *),
 have hn0 : 0 < n := nat.pos_of_ne_zero (λ h, by simp * at *),
-(nat.mul_right_inj (show 0 < 2, from dec_trivial)).1 $
+(nat.mul_right_inj zero_lt_two).1 $
 by rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
   two_mul_odd_div_two (nat.odd_mul_odd hm1 hn1), mul_tsub, mul_one,
   ← add_tsub_assoc_of_le (succ_le_of_lt hm0),

src/data/nat/sqrt.lean

@@ -79,9 +79,8 @@ private lemma sqrt_aux_is_sqrt_lemma (m r n : ℕ)
     is_sqrt n (sqrt_aux m' ((r + 2^m) * 2^m) (n - (r + 2^m) * (r + 2^m)))) :
   is_sqrt n (sqrt_aux (2^m * 2^m) ((2*r)*2^m) (n - r*r)) :=
 begin
-  have b0 :=
-    have b0:_, from ne_of_gt (pow_pos (show 0 < 2, from dec_trivial) m),
-    nat.mul_ne_zero b0 b0,
+  have b0 : 2 ^ m * 2 ^ m ≠ 0,
+    from mul_self_ne_zero.2 (pow_ne_zero m two_ne_zero),
   have lb : n - r * r < 2 * r * 2^m + 2^m * 2^m ↔
             n < (r+2^m)*(r+2^m),
   { rw [tsub_lt_iff_right h₁],

src/number_theory/fermat4.lean

@@ -46,7 +46,7 @@ end
 
 lemma ne_zero {a b c : ℤ} (h : fermat_42 a b c) : c ≠ 0 :=
 begin
-  apply ne_zero_pow (dec_trivial : 2 ≠ 0), apply ne_of_gt,
+  apply ne_zero_pow two_ne_zero _, apply ne_of_gt,
   rw [← h.2.2, (by ring : a ^ 4 + b ^ 4 = (a ^ 2) ^ 2 + (b ^ 2) ^ 2)],
   exact add_pos (sq_pos_of_ne_zero _ (pow_ne_zero 2 h.1))
       (sq_pos_of_ne_zero _ (pow_ne_zero 2 h.2.1))
@@ -85,15 +85,14 @@ begin
   obtain ⟨a1, rfl⟩ := (int.coe_nat_dvd_left.mpr hpa),
   obtain ⟨b1, rfl⟩ := (int.coe_nat_dvd_left.mpr hpb),
   have hpc : (p : ℤ) ^ 2 ∣ c,
-  { apply (int.pow_dvd_pow_iff (dec_trivial : 0 < 2)).mp,
-    rw ← h.1.2.2,
+  { rw [←int.pow_dvd_pow_iff zero_lt_two, ←h.1.2.2],
     apply dvd.intro (a1 ^ 4 + b1 ^ 4), ring },
   obtain ⟨c1, rfl⟩ := hpc,
   have hf : fermat_42 a1 b1 c1,
     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 _ _ (show 0 < 2, from dec_trivial) (nat.prime.one_lt hp) },
+  { exact nat.one_lt_pow _ _ zero_lt_two (nat.prime.one_lt hp) },
   { exact (nat.pos_of_ne_zero (int.nat_abs_ne_zero_of_ne_zero (ne_zero hf))) },
 end
 
@@ -217,7 +216,7 @@ begin
     revert hb20, rw [ht2, htt2, mul_assoc, @mul_assoc _ _ _ r s, hrsz],
     simp },
   have h2b0 : b' ≠ 0,
-  { apply ne_zero_pow (dec_trivial : 2 ≠ 0),
+  { apply ne_zero_pow two_ne_zero,
     rw hs, apply mul_ne_zero, { exact ne_of_gt h4}, { exact hrsz } },
   obtain ⟨i, hi⟩ := int.sq_of_gcd_eq_one hcp hs.symm,
   -- use m is positive to exclude m = - i ^ 2
@@ -244,14 +243,14 @@ begin
   -- r = +/- j ^ 2
   obtain ⟨j, hj⟩ := int.sq_of_gcd_eq_one htt4 hd,
   have hj0 : j ≠ 0,
-  { intro h0, rw [h0, zero_pow (dec_trivial : 0 < 2), neg_zero, or_self] at hj,
+  { intro h0, rw [h0, zero_pow zero_lt_two, neg_zero, or_self] at hj,
     apply left_ne_zero_of_mul hrsz hj },
   rw mul_comm at hd,
   rw [int.gcd_comm] at htt4,
   -- s = +/- k ^ 2
   obtain ⟨k, hk⟩ := int.sq_of_gcd_eq_one htt4 hd,
   have hk0 : k ≠ 0,
-  { intro h0, rw [h0, zero_pow (dec_trivial : 0 < 2), neg_zero, or_self] at hk,
+  { intro h0, rw [h0, zero_pow zero_lt_two, neg_zero, or_self] at hk,
     apply right_ne_zero_of_mul hrsz hk },
   have hj2 : r ^ 2 = j ^ 4, { cases hj with hjp hjp; { rw hjp, ring } },
   have hk2 : s ^ 2 = k ^ 4, { cases hk with hkp hkp; { rw hkp, ring } },

src/number_theory/lucas_lehmer.lean

@@ -510,7 +510,7 @@ begin
   conv in k { rw ← nat.div_add_mod k (2^n) },
   refine nat.modeq.add_right _ _,
   conv { congr, skip, skip, rw ← one_mul (k/2^n) },
-  exact (nat.modeq_sub $ pow_pos (by norm_num : 0 < 2) _).mul_right _,
+  exact (nat.modeq_sub $ nat.succ_le_of_lt $ pow_pos zero_lt_two _).mul_right _,
 end
 
 -- It's hard to know what the limiting factor for large Mersenne primes would be.

src/number_theory/pythagorean_triples.lean

@@ -153,7 +153,7 @@ begin
     ∃ (k : ℕ) x0 y0, 0 < k ∧ int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
     int.exists_gcd_one' (nat.pos_of_ne_zero h0),
   rw [int.gcd_mul_right, h2, int.nat_abs_of_nat, one_mul],
-  rw [← int.pow_dvd_pow_iff (dec_trivial : 0 < 2), sq z, ← h.eq],
+  rw [← int.pow_dvd_pow_iff zero_lt_two, sq z, ← h.eq],
   rw (by ring : x0 * k * (x0 * k) + y0 * k * (y0 * k) = k ^ 2 * (x0 * x0 + y0 * y0)),
   exact dvd_mul_right _ _
 end