feat(Data/*/Sqrt): decidability of IsSquare (#7935)

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20Case.20checking.20in.20combinatorics/near/398517440)

Author: eric-wieser

Mathlib/Algebra/Parity.lean

@@ -58,13 +58,44 @@ theorem isSquare_mul_self (m : α) : IsSquare (m * m) :=
 #align even_add_self even_add_self
 
 @[to_additive]
-theorem isSquare_op_iff (a : α) : IsSquare (op a) ↔ IsSquare a :=
-  ⟨fun ⟨c, hc⟩ => ⟨unop c, by rw [← unop_mul, ← hc, unop_op]⟩, fun ⟨c, hc⟩ => by simp [hc]⟩
+theorem isSquare_op_iff {a : α} : IsSquare (op a) ↔ IsSquare a :=
+  ⟨fun ⟨c, hc⟩ => ⟨unop c, congr_arg unop hc⟩, fun ⟨c, hc⟩ => ⟨op c, congr_arg op hc⟩⟩
 #align is_square_op_iff isSquare_op_iff
 #align even_op_iff even_op_iff
 
+@[to_additive]
+theorem isSquare_unop_iff {a : αᵐᵒᵖ} : IsSquare (unop a) ↔ IsSquare a := isSquare_op_iff.symm
+
+@[to_additive]
+instance [DecidablePred (IsSquare : α → Prop)] : DecidablePred (IsSquare : αᵐᵒᵖ → Prop) :=
+  fun _ => decidable_of_iff _ isSquare_unop_iff
+
+@[simp]
+theorem even_ofMul_iff {a : α} : Even (Additive.ofMul a) ↔ IsSquare a := Iff.rfl
+
+@[simp]
+theorem isSquare_toMul_iff {a : Additive α} : IsSquare (Additive.toMul a) ↔ Even a := Iff.rfl
+
+instance [DecidablePred (IsSquare : α → Prop)] : DecidablePred (Even : Additive α → Prop) :=
+  fun _ => decidable_of_iff _ isSquare_toMul_iff
+
 end Mul
 
+section Add
+variable [Add α]
+
+@[simp]
+theorem isSquare_ofAdd_iff {a : α} : IsSquare (Multiplicative.ofAdd a) ↔ Even a := Iff.rfl
+
+@[simp]
+theorem even_toAdd_iff {a : Multiplicative α} :
+    Even (Multiplicative.toAdd a) ↔ IsSquare a := Iff.rfl
+
+instance [DecidablePred (Even : α → Prop)] : DecidablePred (IsSquare : Multiplicative α → Prop) :=
+  fun _ => decidable_of_iff _ even_toAdd_iff
+
+end Add
+
 @[to_additive (attr := simp)]
 theorem isSquare_one [MulOneClass α] : IsSquare (1 : α) :=
   ⟨1, (mul_one _).symm⟩
@@ -165,7 +196,7 @@ theorem isSquare_inv : IsSquare a⁻¹ ↔ IsSquare a := by
   refine' ⟨fun h => _, fun h => _⟩
   · rw [← isSquare_op_iff, ← inv_inv a]
     exact h.map (MulEquiv.inv' α)
-  · exact ((isSquare_op_iff a).mpr h).map (MulEquiv.inv' α).symm
+  · exact (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm
 #align is_square_inv isSquare_inv
 #align even_neg even_neg
 

Mathlib/Data/Int/Sqrt.lean

@@ -37,4 +37,9 @@ theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n :=
   coe_nat_nonneg _
 #align int.sqrt_nonneg Int.sqrt_nonneg
 
+/-- `IsSquare` can be decided on `ℤ` by checking against the square root. -/
+instance : DecidablePred (IsSquare : ℤ → Prop) :=
+  fun m => decidable_of_iff' (sqrt m * sqrt m = m) <| by
+    simp_rw [←exists_mul_self m, IsSquare, eq_comm]
+
 end Int

Mathlib/Data/Nat/Sqrt.lean

@@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
+import Mathlib.Algebra.Parity
 import Mathlib.Data.Int.Order.Basic
 import Mathlib.Data.Nat.Size
 import Mathlib.Data.Nat.ForSqrt
@@ -176,6 +177,11 @@ theorem exists_mul_self' (x : ℕ) : (∃ n, n ^ 2 = x) ↔ sqrt x ^ 2 = x := by
   simpa only [pow_two] using exists_mul_self x
 #align nat.exists_mul_self' Nat.exists_mul_self'
 
+/-- `IsSquare` can be decided on `ℕ` by checking against the square root. -/
+instance : DecidablePred (IsSquare : ℕ → Prop) :=
+  fun m => decidable_of_iff' (Nat.sqrt m * Nat.sqrt m = m) <| by
+    simp_rw [←Nat.exists_mul_self m, IsSquare, eq_comm]
+
 theorem sqrt_mul_sqrt_lt_succ (n : ℕ) : sqrt n * sqrt n < n + 1 :=
   lt_succ_iff.mpr (sqrt_le _)
 #align nat.sqrt_mul_sqrt_lt_succ Nat.sqrt_mul_sqrt_lt_succ

Mathlib/Data/Rat/Sqrt.lean

@@ -42,4 +42,9 @@ theorem sqrt_nonneg (q : ℚ) : 0 ≤ Rat.sqrt q :=
       Int.coe_nat_nonneg _
 #align rat.sqrt_nonneg Rat.sqrt_nonneg
 
+/-- `IsSquare` can be decided on `ℚ` by checking against the square root. -/
+instance : DecidablePred (IsSquare : ℚ → Prop) :=
+  fun m => decidable_of_iff' (sqrt m * sqrt m = m) <| by
+    simp_rw [←exists_mul_self m, IsSquare, eq_comm]
+
 end Rat