chore: make argument to sq_pos_of_ne_zero/sq_pos_iff implicit (#12288)

This matches our general policy and zpow_two_pos_of_ne_zero.

Also define sq_pos_of_ne_zero as an alias.

Mathlib/Algebra/GroupPower/Order.lean

@@ -455,14 +455,6 @@ theorem pow_bit0_pos {a : R} (h : a ≠ 0) (n : ℕ) : 0 < a ^ bit0 n :=
   (pow_bit0_nonneg a n).lt_of_ne (pow_ne_zero _ h).symm
 #align pow_bit0_pos pow_bit0_pos
 
-theorem sq_pos_of_ne_zero {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R]
-    (a : R) (h : a ≠ 0) : 0 < a ^ 2 := by
-  rwa [(sq_nonneg a).lt_iff_ne, ne_comm, pow_ne_zero_iff two_ne_zero]
-#align sq_pos_of_ne_zero sq_pos_of_ne_zero
-
-alias pow_two_pos_of_ne_zero := sq_pos_of_ne_zero
-#align pow_two_pos_of_ne_zero pow_two_pos_of_ne_zero
-
 theorem pow_bit0_pos_iff (a : R) {n : ℕ} (hn : n ≠ 0) : 0 < a ^ bit0 n ↔ a ≠ 0 := by
   refine' ⟨fun h => _, fun h => pow_bit0_pos h n⟩
   rintro rfl
@@ -500,11 +492,17 @@ lemma strictMono_pow_bit1 (n : ℕ) : StrictMono (· ^ bit1 n : R → R) := by
 
 end deprecated
 
-lemma sq_pos_iff {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] (a : R) :
+lemma sq_pos_iff {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} :
     0 < a ^ 2 ↔ a ≠ 0 := by
   rw [← pow_ne_zero_iff two_ne_zero, (sq_nonneg a).lt_iff_ne, ne_comm]
 #align sq_pos_iff sq_pos_iff
 
+alias ⟨_, sq_pos_of_ne_zero⟩ := sq_pos_iff
+#align sq_pos_of_ne_zero sq_pos_of_ne_zero
+
+alias pow_two_pos_of_ne_zero := sq_pos_of_ne_zero
+#align pow_two_pos_of_ne_zero pow_two_pos_of_ne_zero
+
 lemma pow_four_le_pow_two_of_pow_two_le (h : a ^ 2 ≤ b) : a ^ 4 ≤ b ^ 2 :=
   (pow_mul a 2 2).symm ▸ pow_le_pow_left (sq_nonneg a) h 2
 #align pow_four_le_pow_two_of_pow_two_le pow_four_le_pow_two_of_pow_two_le

Mathlib/Algebra/Order/Chebyshev.lean

@@ -156,7 +156,7 @@ theorem sum_div_card_sq_le_sum_sq_div_card :
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   rw [← card_pos, ← @Nat.cast_pos α] at hs
-  rw [div_pow, div_le_div_iff (sq_pos_of_ne_zero _ hs.ne') hs, sq (s.card : α), mul_left_comm, ←
+  rw [div_pow, div_le_div_iff (sq_pos_of_ne_zero hs.ne') hs, sq (s.card : α), mul_left_comm, ←
     mul_assoc]
   exact mul_le_mul_of_nonneg_right sq_sum_le_card_mul_sum_sq hs.le
 #align sum_div_card_sq_le_sum_sq_div_card sum_div_card_sq_le_sum_sq_div_card

Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

@@ -49,8 +49,8 @@ def polarCoord : PartialHomeomorph (ℝ × ℝ) (ℝ × ℝ) where
       true_and_iff, Complex.arg_lt_pi_iff]
     constructor
     · cases' hxy with hxy hxy
-      · dsimp at hxy; linarith [sq_pos_of_ne_zero _ hxy.ne', sq_nonneg y]
-      · linarith [sq_nonneg x, sq_pos_of_ne_zero _ hxy]
+      · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y]
+      · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy]
     · cases' hxy with hxy hxy
       · exact Or.inl (le_of_lt hxy)
       · exact Or.inr hxy

Mathlib/Combinatorics/Additive/Behrend.lean

@@ -322,7 +322,7 @@ theorem le_sqrt_log (hN : 4096 ≤ N) : log (2 / (1 - 2 / exp 1)) * (69 / 50) 
   apply mul_le_mul_of_nonneg_right _ (log_nonneg one_le_two)
   rw [← le_div_iff']
   · exact log_two_lt_d9.le.trans (by norm_num1)
-  exact sq_pos_of_ne_zero _ (by norm_num1)
+  exact sq_pos_of_ne_zero (by norm_num1)
 #align behrend.le_sqrt_log Behrend.le_sqrt_log
 
 theorem exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : exp (-2 * x) < exp (2 - ⌈x⌉₊) / ⌈x⌉₊ := by

Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

@@ -110,7 +110,7 @@ theorem lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj [LinearOrderedFi
     · refine ⟨i, mem_univ _, sum_pos' (fun k _ ↦ ?_) ⟨j, mem_univ _, ?_⟩⟩
       · exact ite_nonneg (sq_nonneg _) le_rfl
       · simpa only [hn, ite_true, gt_iff_lt, sub_pos] using
-          sq_pos_of_ne_zero _ (sub_ne_zero.mpr hn.2)
+          sq_pos_of_ne_zero (sub_ne_zero.mpr hn.2)
   · intro h
     rw [lapMatrix_toLinearMap₂', div_eq_zero_iff]
     refine Or.inl <| sum_eq_zero fun i _ ↦ (sum_eq_zero fun j _ ↦ ?_)

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -254,12 +254,12 @@ theorem add_div_le_sum_sq_div_card (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜)
   apply (add_le_add_left h₃ _).trans
   -- Porting note: was
   -- `simp [← mul_div_right_comm _ (t.card : 𝕜), sub_div' _ _ _ htcard.ne', ← sum_div, ← add_div,`
-  -- `  mul_pow, div_le_iff (sq_pos_of_ne_zero _ htcard.ne'), sub_sq, sum_add_distrib, ← sum_mul,`
+  -- `  mul_pow, div_le_iff (sq_pos_of_ne_zero htcard.ne'), sub_sq, sum_add_distrib, ← sum_mul,`
   -- `  ← mul_sum]`
   simp_rw [sub_div' _ _ _ htcard.ne']
   conv_lhs => enter [2, 2, x]; rw [div_pow]
   rw [div_pow, ← sum_div, ← mul_div_right_comm _ (t.card : 𝕜), ← add_div,
-    div_le_iff (sq_pos_of_ne_zero _ htcard.ne')]
+    div_le_iff (sq_pos_of_ne_zero htcard.ne')]
   simp_rw [sub_sq, sum_add_distrib, sum_const, nsmul_eq_mul, sum_sub_distrib, mul_pow, ← sum_mul,
     ← mul_sum, ← sum_mul]
   ring_nf; rfl

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -142,7 +142,7 @@ private theorem one_sub_eps_mul_card_nonuniformWitness_le_card_star (hV : V ∈
       _ ≤ ↑2 ^ P.parts.card * ε ^ 2 / 10 := by
         refine' (one_le_sq_iff <| by positivity).1 _
         rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε,
-          one_le_div (sq_pos_of_ne_zero (10 : ℝ) <| by norm_num)]
+          one_le_div (sq_pos_of_ne_zero <| by norm_num)]
         calc
           (↑10 ^ 2) = 100 := by norm_num
           _ ≤ ↑4 ^ P.parts.card * ε ^ 5 := hPε

Mathlib/NumberTheory/FLT/Four.lean

@@ -59,7 +59,7 @@ theorem ne_zero {a b c : ℤ} (h : Fermat42 a b c) : c ≠ 0 := by
   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))
+    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))
 #align fermat_42.ne_zero Fermat42.ne_zero
 
 /-- We say a solution to `a ^ 4 + b ^ 4 = c ^ 2` is minimal if there is no other solution with
@@ -286,7 +286,7 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0
     apply gt_of_gt_of_ge _ (Int.natAbs_le_self_sq i)
     rw [← hi, ht3]
     apply gt_of_gt_of_ge _ (Int.le_self_sq m)
-    exact lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero n hn)
+    exact lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero hn)
   have hic' : Int.natAbs c ≤ Int.natAbs i := by
     apply h.2 j k i
     exact ⟨hj0, hk0, hh.symm⟩

Mathlib/NumberTheory/Modular.lean

@@ -490,7 +490,7 @@ theorem abs_c_le_one (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : |(↑ₘg
       linarith
   intro hc
   replace hc : 0 < c ^ 4 := by
-    change 0 < c ^ (2 * 2); rw [pow_mul]; apply sq_pos_of_pos (sq_pos_of_ne_zero _ hc)
+    change 0 < c ^ (2 * 2); rw [pow_mul]; apply sq_pos_of_pos (sq_pos_of_ne_zero hc)
   have h₁ :=
     mul_lt_mul_of_pos_right
       (mul_lt_mul'' (three_lt_four_mul_im_sq_of_mem_fdo hg) (three_lt_four_mul_im_sq_of_mem_fdo hz)

Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean

@@ -142,7 +142,7 @@ lemma isBigO_atTop_F_nat_zero_sub {a : ℝ} (ha : 0 ≤ a) : ∃ p, 0 < p ∧
       apply Eventually.isBigO
       filter_upwards [eventually_gt_atTop 0] with t ht
       exact F_nat_zero_le ha ht
-    refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero _ h), this.trans ?_⟩
+    refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩
     simpa only [neg_mul π (a ^ 2), mul_one] using (isBigO_refl _ _).mul isBigO_one_aux
 
 end k_eq_zero

Mathlib/NumberTheory/Pell.lean

@@ -209,8 +209,8 @@ theorem y_neg (a : Solution₁ d) : (-a).y = -a.y :=
 theorem eq_zero_of_d_neg (h₀ : d < 0) (a : Solution₁ d) : a.x = 0 ∨ a.y = 0 := by
   have h := a.prop
   contrapose! h
-  have h1 := sq_pos_of_ne_zero a.x h.1
-  have h2 := sq_pos_of_ne_zero a.y h.2
+  have h1 := sq_pos_of_ne_zero h.1
+  have h2 := sq_pos_of_ne_zero h.2
   nlinarith
 #align pell.solution₁.eq_zero_of_d_neg Pell.Solution₁.eq_zero_of_d_neg
 
@@ -462,7 +462,7 @@ theorem exists_pos_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) :
   obtain ⟨x, y, h, hy⟩ := exists_of_not_isSquare h₀ hd
   refine' ⟨mk |x| |y| (by rwa [sq_abs, sq_abs]), _, abs_pos.mpr hy⟩
   rw [x_mk, ← one_lt_sq_iff_one_lt_abs, eq_add_of_sub_eq h, lt_add_iff_pos_right]
-  exact mul_pos h₀ (sq_pos_of_ne_zero y hy)
+  exact mul_pos h₀ (sq_pos_of_ne_zero hy)
 #align pell.solution₁.exists_pos_of_not_is_square Pell.Solution₁.exists_pos_of_not_isSquare
 
 end Solution₁

Mathlib/NumberTheory/PythagoreanTriples.lean

@@ -233,8 +233,8 @@ theorem ne_zero_of_coprime (hc : Int.gcd x y = 1) : z ≠ 0 := by
     rw [hc]
     exact one_ne_zero
   cases' Int.ne_zero_of_gcd hc' with hxz hyz
-  · apply lt_add_of_pos_of_le (sq_pos_of_ne_zero x hxz) (sq_nonneg y)
-  · apply lt_add_of_le_of_pos (sq_nonneg x) (sq_pos_of_ne_zero y hyz)
+  · apply lt_add_of_pos_of_le (sq_pos_of_ne_zero hxz) (sq_nonneg y)
+  · apply lt_add_of_le_of_pos (sq_nonneg x) (sq_pos_of_ne_zero hyz)
 #align pythagorean_triple.ne_zero_of_coprime PythagoreanTriple.ne_zero_of_coprime
 
 theorem isPrimitiveClassified_of_coprime_of_zero_left (hc : Int.gcd x y = 1) (hx : x = 0) :

Mathlib/Probability/Variance.lean

@@ -279,7 +279,7 @@ theorem meas_ge_le_evariance_div_sq {X : Ω → ℝ} (hX : AEStronglyMeasurable
 from its expectation in terms of the variance. -/
 theorem meas_ge_le_variance_div_sq [@IsFiniteMeasure Ω _ ℙ] {X : Ω → ℝ} (hX : Memℒp X 2) {c : ℝ}
     (hc : 0 < c) : ℙ {ω | c ≤ |X ω - 𝔼[X]|} ≤ ENNReal.ofReal (Var[X] / c ^ 2) := by
-  rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero _ hc.ne.symm), hX.ofReal_variance_eq]
+  rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero hc.ne.symm), hX.ofReal_variance_eq]
   convert @meas_ge_le_evariance_div_sq _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1
   · simp only [Real.coe_toNNReal', max_le_iff, abs_nonneg, and_true_iff]
   · rw [ENNReal.ofReal_pow hc.le]