chore(NumberTheory/Zsqrtd): use @[ext] (#9299)

Added `@[ext]` to definition `structure Zsqrtd (d : ℤ)`. (also added lemma `sub_re`, `sub_im`)

Mathlib/NumberTheory/Pell.lean

@@ -140,7 +140,7 @@ theorem prop_y (a : Solution₁ d) : d * a.y ^ 2 = a.x ^ 2 - 1 := by rw [← a.p
 /-- Two solutions are equal if their `x` and `y` components are equal. -/
 @[ext]
 theorem ext {a b : Solution₁ d} (hx : a.x = b.x) (hy : a.y = b.y) : a = b :=
-  Subtype.ext <| ext.mpr ⟨hx, hy⟩
+  Subtype.ext <| Zsqrtd.ext _ _ hx hy
 #align pell.solution₁.ext Pell.Solution₁.ext
 
 /-- Construct a solution from `x`, `y` and a proof that the equation is satisfied. -/
@@ -161,7 +161,7 @@ theorem y_mk (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) : (mk x y prop).y = y :=
 
 @[simp]
 theorem coe_mk (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) : (↑(mk x y prop) : ℤ√d) = ⟨x, y⟩ :=
-  Zsqrtd.ext.mpr ⟨x_mk x y prop, y_mk x y prop⟩
+  Zsqrtd.ext _ _ (x_mk x y prop) (y_mk x y prop)
 #align pell.solution₁.coe_mk Pell.Solution₁.coe_mk
 
 @[simp]

Mathlib/NumberTheory/PellMatiyasevic.lean

@@ -67,7 +67,7 @@ def IsPell : ℤ√d → Prop
 #align pell.is_pell Pell.IsPell
 
 theorem isPell_norm : ∀ {b : ℤ√d}, IsPell b ↔ b * star b = 1
-  | ⟨x, y⟩ => by simp [Zsqrtd.ext, IsPell, mul_comm]; ring_nf
+  | ⟨x, y⟩ => by simp [Zsqrtd.ext_iff, IsPell, mul_comm]; ring_nf
 #align pell.is_pell_norm Pell.isPell_norm
 
 theorem isPell_iff_mem_unitary : ∀ {b : ℤ√d}, IsPell b ↔ b ∈ unitary (ℤ√d)
@@ -217,7 +217,7 @@ theorem isPell_nat {x y : ℕ} : IsPell (⟨x, y⟩ : ℤ√(d a1)) ↔ x * x -
 #align pell.is_pell_nat Pell.isPell_nat
 
 @[simp]
-theorem pellZd_succ (n : ℕ) : pellZd a1 (n + 1) = pellZd a1 n * ⟨a, 1⟩ := by simp [Zsqrtd.ext]
+theorem pellZd_succ (n : ℕ) : pellZd a1 (n + 1) = pellZd a1 n * ⟨a, 1⟩ := by ext <;> simp
 #align pell.pell_zd_succ Pell.pellZd_succ
 
 theorem isPell_one : IsPell (⟨a, 1⟩ : ℤ√(d a1)) :=
@@ -511,9 +511,7 @@ theorem pellZd_succ_succ (n) :
     change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩
     rw [dz_val]
     dsimp [az]
-    rw [Zsqrtd.ext]
-    dsimp
-    constructor <;> ring_nf
+    ext <;> dsimp <;> ring_nf
   simpa [mul_add, mul_comm, mul_left_comm, add_comm] using congr_arg (· * pellZd a1 n) this
 #align pell.pell_zd_succ_succ Pell.pellZd_succ_succ
 

Mathlib/NumberTheory/Zsqrtd/Basic.lean

@@ -26,11 +26,13 @@ to choices of square roots of `d` in `R`.
 /-- The ring of integers adjoined with a square root of `d`.
   These have the form `a + b √d` where `a b : ℤ`. The components
   are called `re` and `im` by analogy to the negative `d` case. -/
+@[ext]
 structure Zsqrtd (d : ℤ) where
   re : ℤ
   im : ℤ
   deriving DecidableEq
 #align zsqrtd Zsqrtd
+#align zsqrtd.ext Zsqrtd.ext_iff
 
 prefix:100 "ℤ√" => Zsqrtd
 
@@ -40,12 +42,6 @@ section
 
 variable {d : ℤ}
 
-theorem ext : ∀ {z w : ℤ√d}, z = w ↔ z.re = w.re ∧ z.im = w.im
-  | ⟨x, y⟩, ⟨x', y'⟩ =>
-    ⟨fun h => by injection h; constructor <;> assumption,
-     fun ⟨h₁, h₂⟩ => by congr⟩
-#align zsqrtd.ext Zsqrtd.ext
-
 /-- Convert an integer to a `ℤ√d` -/
 def ofInt (n : ℤ) : ℤ√d :=
   ⟨n, 0⟩
@@ -190,7 +186,16 @@ instance addCommGroup : AddCommGroup (ℤ√d) := by
     add_left_neg := ?_
     add_comm := ?_ } <;>
   intros <;>
-  simp [ext, add_comm, add_left_comm]
+  ext <;>
+  simp [add_comm, add_left_comm]
+
+@[simp]
+theorem sub_re (z w : ℤ√d) : (z - w).re = z.re - w.re :=
+  rfl
+
+@[simp]
+theorem sub_im (z w : ℤ√d) : (z - w).im = z.im - w.im :=
+  rfl
 
 instance addGroupWithOne : AddGroupWithOne (ℤ√d) :=
   { Zsqrtd.addCommGroup with
@@ -213,7 +218,7 @@ instance commRing : CommRing (ℤ√d) := by
     mul_one := ?_
     mul_comm := ?_ } <;>
   intros <;>
-  refine ext.mpr ⟨?_, ?_⟩ <;>
+  ext <;>
   simp <;>
   ring
 
@@ -259,13 +264,13 @@ theorem star_im (z : ℤ√d) : (star z).im = -z.im :=
 #align zsqrtd.star_im Zsqrtd.star_im
 
 instance : StarRing (ℤ√d) where
-  star_involutive x := ext.mpr ⟨rfl, neg_neg _⟩
-  star_mul a b := ext.mpr ⟨by simp; ring, by simp; ring⟩
-  star_add a b := ext.mpr ⟨rfl, neg_add _ _⟩
+  star_involutive x := Zsqrtd.ext _ _ rfl (neg_neg _)
+  star_mul a b := by ext <;> simp <;> ring
+  star_add a b := Zsqrtd.ext _ _ rfl (neg_add _ _)
 
 -- Porting note: proof was `by decide`
 instance nontrivial : Nontrivial (ℤ√d) :=
-  ⟨⟨0, 1, ext.not.mpr <| by simp⟩⟩
+  ⟨⟨0, 1, (Zsqrtd.ext_iff 0 1).not.mpr (by simp)⟩⟩
 
 @[simp]
 theorem coe_nat_re (n : ℕ) : (n : ℤ√d).re = n :=
@@ -297,17 +302,17 @@ theorem coe_int_re (n : ℤ) : (n : ℤ√d).re = n := by cases n <;> rfl
 theorem coe_int_im (n : ℤ) : (n : ℤ√d).im = 0 := by cases n <;> rfl
 #align zsqrtd.coe_int_im Zsqrtd.coe_int_im
 
-theorem coe_int_val (n : ℤ) : (n : ℤ√d) = ⟨n, 0⟩ := by simp [ext]
+theorem coe_int_val (n : ℤ) : (n : ℤ√d) = ⟨n, 0⟩ := by ext <;> simp
 #align zsqrtd.coe_int_val Zsqrtd.coe_int_val
 
-instance : CharZero (ℤ√d) where cast_injective m n := by simp [ext]
+instance : CharZero (ℤ√d) where cast_injective m n := by simp [Zsqrtd.ext_iff]
 
 @[simp]
-theorem ofInt_eq_coe (n : ℤ) : (ofInt n : ℤ√d) = n := by simp [ext, ofInt_re, ofInt_im]
+theorem ofInt_eq_coe (n : ℤ) : (ofInt n : ℤ√d) = n := by ext <;> simp [ofInt_re, ofInt_im]
 #align zsqrtd.of_int_eq_coe Zsqrtd.ofInt_eq_coe
 
 @[simp]
-theorem smul_val (n x y : ℤ) : (n : ℤ√d) * ⟨x, y⟩ = ⟨n * x, n * y⟩ := by simp [ext]
+theorem smul_val (n x y : ℤ) : (n : ℤ√d) * ⟨x, y⟩ = ⟨n * x, n * y⟩ := by ext <;> simp
 #align zsqrtd.smul_val Zsqrtd.smul_val
 
 theorem smul_re (a : ℤ) (b : ℤ√d) : (↑a * b).re = a * b.re := by simp
@@ -317,34 +322,34 @@ theorem smul_im (a : ℤ) (b : ℤ√d) : (↑a * b).im = a * b.im := by simp
 #align zsqrtd.smul_im Zsqrtd.smul_im
 
 @[simp]
-theorem muld_val (x y : ℤ) : sqrtd (d := d) * ⟨x, y⟩ = ⟨d * y, x⟩ := by simp [ext]
+theorem muld_val (x y : ℤ) : sqrtd (d := d) * ⟨x, y⟩ = ⟨d * y, x⟩ := by ext <;> simp
 #align zsqrtd.muld_val Zsqrtd.muld_val
 
 @[simp]
-theorem dmuld : sqrtd (d := d) * sqrtd (d := d) = d := by simp [ext]
+theorem dmuld : sqrtd (d := d) * sqrtd (d := d) = d := by ext <;> simp
 #align zsqrtd.dmuld Zsqrtd.dmuld
 
 @[simp]
-theorem smuld_val (n x y : ℤ) : sqrtd * (n : ℤ√d) * ⟨x, y⟩ = ⟨d * n * y, n * x⟩ := by simp [ext]
+theorem smuld_val (n x y : ℤ) : sqrtd * (n : ℤ√d) * ⟨x, y⟩ = ⟨d * n * y, n * x⟩ := by ext <;> simp
 #align zsqrtd.smuld_val Zsqrtd.smuld_val
 
-theorem decompose {x y : ℤ} : (⟨x, y⟩ : ℤ√d) = x + sqrtd (d := d) * y := by simp [ext]
+theorem decompose {x y : ℤ} : (⟨x, y⟩ : ℤ√d) = x + sqrtd (d := d) * y := by ext <;> simp
 #align zsqrtd.decompose Zsqrtd.decompose
 
 theorem mul_star {x y : ℤ} : (⟨x, y⟩ * star ⟨x, y⟩ : ℤ√d) = x * x - d * y * y := by
-  simp [ext, sub_eq_add_neg, mul_comm]
+  ext <;> simp [sub_eq_add_neg, mul_comm]
 #align zsqrtd.mul_star Zsqrtd.mul_star
 
 protected theorem coe_int_add (m n : ℤ) : (↑(m + n) : ℤ√d) = ↑m + ↑n :=
-  (Int.castRingHom _).map_add _ _
+  Int.cast_add m n
 #align zsqrtd.coe_int_add Zsqrtd.coe_int_add
 
 protected theorem coe_int_sub (m n : ℤ) : (↑(m - n) : ℤ√d) = ↑m - ↑n :=
-  (Int.castRingHom _).map_sub _ _
+  Int.cast_sub m n
 #align zsqrtd.coe_int_sub Zsqrtd.coe_int_sub
 
 protected theorem coe_int_mul (m n : ℤ) : (↑(m * n) : ℤ√d) = ↑m * ↑n :=
-  (Int.castRingHom _).map_mul _ _
+  Int.cast_mul m n
 #align zsqrtd.coe_int_mul Zsqrtd.coe_int_mul
 
 protected theorem coe_int_inj {m n : ℤ} (h : (↑m : ℤ√d) = ↑n) : m = n := by
@@ -358,7 +363,7 @@ theorem coe_int_dvd_iff (z : ℤ) (a : ℤ√d) : ↑z ∣ a ↔ z ∣ a.re ∧
       mul_re, mul_zero, coe_int_im]
   · rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
     use ⟨r, i⟩
-    rw [smul_val, ext]
+    rw [smul_val, Zsqrtd.ext_iff]
     exact ⟨hr, hi⟩
 #align zsqrtd.coe_int_dvd_iff Zsqrtd.coe_int_dvd_iff
 
@@ -374,14 +379,14 @@ theorem coe_int_dvd_coe_int (a b : ℤ) : (a : ℤ√d) ∣ b ↔ a ∣ b := by
 
 protected theorem eq_of_smul_eq_smul_left {a : ℤ} {b c : ℤ√d} (ha : a ≠ 0) (h : ↑a * b = a * c) :
     b = c := by
-  rw [ext] at h ⊢
+  rw [Zsqrtd.ext_iff] at h ⊢
   apply And.imp _ _ h <;> simpa only [smul_re, smul_im] using mul_left_cancel₀ ha
 #align zsqrtd.eq_of_smul_eq_smul_left Zsqrtd.eq_of_smul_eq_smul_left
 
 section Gcd
 
 theorem gcd_eq_zero_iff (a : ℤ√d) : Int.gcd a.re a.im = 0 ↔ a = 0 := by
-  simp only [Int.gcd_eq_zero_iff, ext, eq_self_iff_true, zero_im, zero_re]
+  simp only [Int.gcd_eq_zero_iff, Zsqrtd.ext_iff, eq_self_iff_true, zero_im, zero_re]
 #align zsqrtd.gcd_eq_zero_iff Zsqrtd.gcd_eq_zero_iff
 
 theorem gcd_pos_iff (a : ℤ√d) : 0 < Int.gcd a.re a.im ↔ a ≠ 0 :=
@@ -392,8 +397,7 @@ theorem coprime_of_dvd_coprime {a b : ℤ√d} (hcoprime : IsCoprime a.re a.im)
     IsCoprime b.re b.im := by
   apply isCoprime_of_dvd
   · rintro ⟨hre, him⟩
-    obtain rfl : b = 0 := by
-      simp only [ext, hre, eq_self_iff_true, zero_im, him, and_self_iff, zero_re]
+    obtain rfl : b = 0 := Zsqrtd.ext b 0 hre him
     rw [zero_dvd_iff] at hdvd
     simp [hdvd, zero_im, zero_re, not_isCoprime_zero_zero] at hcoprime
   · rintro z hz - hzdvdu hzdvdv
@@ -411,8 +415,7 @@ theorem exists_coprime_of_gcd_pos {a : ℤ√d} (hgcd : 0 < Int.gcd a.re a.im) :
   obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd
   rw [mul_comm] at Hre Him
   refine' ⟨⟨re, im⟩, _, _⟩
-  · rw [smul_val, ext, ← Hre, ← Him]
-    constructor <;> rfl
+  · rw [smul_val, ← Hre, ← Him]
   · rw [← Int.gcd_eq_one_iff_coprime, H1]
 #align zsqrtd.exists_coprime_of_gcd_pos Zsqrtd.exists_coprime_of_gcd_pos
 
@@ -551,8 +554,7 @@ def normMonoidHom : ℤ√d →* ℤ where
 #align zsqrtd.norm_monoid_hom Zsqrtd.normMonoidHom
 
 theorem norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * star n := by
-  cases n
-  simp [norm, star, Zsqrtd.ext, mul_comm, sub_eq_add_neg]
+  ext <;> simp [norm, star, mul_comm, sub_eq_add_neg]
 #align zsqrtd.norm_eq_mul_conj Zsqrtd.norm_eq_mul_conj
 
 @[simp]
@@ -607,12 +609,11 @@ theorem norm_eq_one_iff' {d : ℤ} (hd : d ≤ 0) (z : ℤ√d) : z.norm = 1 ↔
 theorem norm_eq_zero_iff {d : ℤ} (hd : d < 0) (z : ℤ√d) : z.norm = 0 ↔ z = 0 := by
   constructor
   · intro h
-    rw [ext, zero_re, zero_im]
     rw [norm_def, sub_eq_add_neg, mul_assoc] at h
     have left := mul_self_nonneg z.re
     have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))
     obtain ⟨ha, hb⟩ := (add_eq_zero_iff' left right).mp h
-    constructor <;> apply eq_zero_of_mul_self_eq_zero
+    ext <;> apply eq_zero_of_mul_self_eq_zero
     · exact ha
     · rw [neg_eq_zero, mul_eq_zero] at hb
       exact hb.resolve_left hd.ne
@@ -1005,7 +1006,7 @@ instance : OrderedRing (ℤ√d) := by infer_instance
 end
 
 theorem norm_eq_zero {d : ℤ} (h_nonsquare : ∀ n : ℤ, d ≠ n * n) (a : ℤ√d) : norm a = 0 ↔ a = 0 := by
-  refine' ⟨fun ha => ext.mpr _, fun h => by rw [h, norm_zero]⟩
+  refine' ⟨fun ha => (Zsqrtd.ext_iff _ _).mpr _, fun h => by rw [h, norm_zero]⟩
   dsimp only [norm] at ha
   rw [sub_eq_zero] at ha
   by_cases h : 0 ≤ d

Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean

@@ -46,13 +46,13 @@ theorem mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : Fact p.Prime]
         revert this hp3 hp1
         generalize p % 4 = m
         intros; interval_cases m <;> simp_all -- Porting note: was `decide!`
-      let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 <| by rw [hp41]; exact by decide
+      let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 <| by rw [hp41]; decide
       obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (_ : k' < p), (k' : ZMod p) = k := by
         refine' ⟨k.val, k.val_lt, ZMod.nat_cast_zmod_val k⟩
       have hpk : p ∣ k ^ 2 + 1 := by
         rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one,
           ← hk, add_left_neg]
-      have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by simp [sq, Zsqrtd.ext]
+      have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by ext <;> simp [sq]
       have hkltp : 1 + k * k < p * p :=
         calc
           1 + k * k ≤ k + k * k := by