feat: norm_cast lemmas about IsSquare and {Int,Rat}.sqrt (#13788)

Author: eric-wieser

Mathlib/Algebra/Ring/Int.lean

@@ -256,4 +256,16 @@ lemma two_mul_ediv_two_of_odd (h : Odd n) : 2 * (n / 2) = n - 1 :=
   eq_sub_of_add_eq (two_mul_ediv_two_add_one_of_odd h)
 #align int.two_mul_div_two_of_odd Int.two_mul_ediv_two_of_odd
 
+@[norm_cast, simp]
+theorem isSquare_natCast_iff {n : ℕ} : IsSquare (n : ℤ) ↔ IsSquare n := by
+  constructor <;> rintro ⟨x, h⟩
+  · exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩
+  · exact ⟨x, mod_cast h⟩
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem isSquare_ofNat_iff {n : ℕ} :
+    IsSquare (no_index (OfNat.ofNat n) : ℤ) ↔ IsSquare (OfNat.ofNat n : ℕ) :=
+  isSquare_natCast_iff
+
 end Int

Mathlib/Data/Int/Sqrt.lean

@@ -39,4 +39,12 @@ theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n :=
   natCast_nonneg _
 #align int.sqrt_nonneg Int.sqrt_nonneg
 
+@[simp, norm_cast]
+theorem sqrt_natCast (n : ℕ) : Int.sqrt (n : ℤ) = Nat.sqrt n := by rw [sqrt, toNat_ofNat]
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem sqrt_ofNat (n : ℕ) : Int.sqrt (no_index (OfNat.ofNat n) : ℤ) = Nat.sqrt (OfNat.ofNat n) :=
+  sqrt_natCast _
+
 end Int

Mathlib/Data/Rat/Lemmas.lean

@@ -119,6 +119,30 @@ theorem add_num_den (q r : ℚ) :
   rw [mul_comm r.num q.den]
 #align rat.add_num_denom Rat.add_num_den
 
+
+theorem isSquare_iff {q : ℚ} : IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den := by
+  constructor
+  · rintro ⟨qr, rfl⟩
+    rw [Rat.mul_self_num, mul_self_den]
+    simp only [isSquare_mul_self, and_self]
+  · rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩
+    refine ⟨nr / dr, ?_⟩
+    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
+
+@[norm_cast, simp]
+theorem isSquare_natCast_iff {n : ℕ} : IsSquare (n : ℚ) ↔ IsSquare n := by
+  simp_rw [isSquare_iff, num_natCast, den_natCast, isSquare_one, and_true, Int.isSquare_natCast_iff]
+
+@[norm_cast, simp]
+theorem isSquare_intCast_iff {z : ℤ} : IsSquare (z : ℚ) ↔ IsSquare z := by
+  simp_rw [isSquare_iff, intCast_num, intCast_den, isSquare_one, and_true]
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem isSquare_ofNat_iff {n : ℕ} :
+    IsSquare (no_index (OfNat.ofNat n) : ℚ) ↔ IsSquare (OfNat.ofNat n : ℕ) :=
+  isSquare_natCast_iff
+
 section Casts
 
 theorem exists_eq_mul_div_num_and_eq_mul_div_den (n : ℤ) {d : ℤ} (d_ne_zero : d ≠ 0) :

Mathlib/Data/Rat/Sqrt.lean

@@ -43,4 +43,17 @@ instance : DecidablePred (IsSquare : ℚ → Prop) :=
   fun m => decidable_of_iff' (sqrt m * sqrt m = m) <| by
     simp_rw [← exists_mul_self m, IsSquare, eq_comm]
 
+@[simp, norm_cast]
+theorem sqrt_intCast (z : ℤ) : Rat.sqrt (z : ℚ) = Int.sqrt z := by
+  simp only [sqrt, num_intCast, den_intCast, Nat.sqrt_one, mkRat_one]
+
+@[simp, norm_cast]
+theorem sqrt_natCast (n : ℕ) : Rat.sqrt (n : ℚ) = Nat.sqrt n := by
+  rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem sqrt_ofNat (n : ℕ) : Rat.sqrt (no_index (OfNat.ofNat n) : ℚ) = Nat.sqrt (OfNat.ofNat n) :=
+  sqrt_natCast _
+
 end Rat