fix: fix Q-smul diamond in Complex (#5341)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
leanprover-community · Jun 23, 2023 · 4003b56 · 4003b56
1 parent e0d8134
commit 4003b56
Show file tree

Hide file tree

Showing 2 changed files with 83 additions and 70 deletions.
diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean
@@ -365,22 +365,47 @@ defined in `Data.Complex.Module`. -/
 instance : Nontrivial ℂ :=
   pullback_nonzero re rfl rfl
 
+-- porting note: moved from `Module/Data/Complex/Basic.lean`
+section SMul
+
+variable {R : Type _} [SMul R ℝ]
+
+/- The useless `0` multiplication in `smul` is to make sure that
+`RestrictScalars.module ℝ ℂ ℂ = Complex.module` definitionally. -/
+instance : SMul R ℂ where
+  smul r x := ⟨r • x.re - 0 * x.im, r • x.im + 0 * x.re⟩
+
+theorem smul_re (r : R) (z : ℂ) : (r • z).re = r • z.re := by simp [(· • ·), SMul.smul]
+#align complex.smul_re Complex.smul_re
+
+theorem smul_im (r : R) (z : ℂ) : (r • z).im = r • z.im := by simp [(· • ·), SMul.smul]
+#align complex.smul_im Complex.smul_im
+
+@[simp]
+theorem real_smul {x : ℝ} {z : ℂ} : x • z = x * z :=
+  rfl
+#align complex.real_smul Complex.real_smul
+
+end SMul
+
 -- Porting note: proof needed modifications and rewritten fields
 instance addCommGroup : AddCommGroup ℂ :=
   { zero := (0 : ℂ)
     add := (· + ·)
     neg := Neg.neg
     sub := Sub.sub
-    nsmul := fun n z => ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩
-    zsmul := fun n z => ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩
-    zsmul_zero' := by intros; ext <;> simp
-    nsmul_zero := by intros; ext <;> simp
+    nsmul := fun n z => n • z
+    zsmul := fun n z => n • z
+    zsmul_zero' := by intros; ext <;> simp [smul_re, smul_im]
+    nsmul_zero := by intros; ext <;> simp [smul_re, smul_im]
     nsmul_succ := by
-      intros; ext <;> simp [AddMonoid.nsmul_succ, add_mul, add_comm]
+      intros; ext <;> simp [AddMonoid.nsmul_succ, add_mul, add_comm,
+        smul_re, smul_im]
     zsmul_succ' := by
-      intros; ext <;> simp [SubNegMonoid.zsmul_succ', add_mul, add_comm]
+      intros; ext <;> simp [SubNegMonoid.zsmul_succ', add_mul, add_comm,
+        smul_re, smul_im]
     zsmul_neg' := by
-      intros; ext <;> simp [zsmul_neg', add_mul]
+      intros; ext <;> simp [zsmul_neg', add_mul, smul_re, smul_im]
     add_assoc := by intros; ext <;> simp [add_assoc]
     zero_add := by intros; ext <;> simp
     add_zero := by intros; ext <;> simp
@@ -757,11 +782,57 @@ protected theorem mul_inv_cancel {z : ℂ} (h : z ≠ 0) : z * z⁻¹ = 1 := by
     ofReal_one]
 #align complex.mul_inv_cancel Complex.mul_inv_cancel
 
-/-! ### Field instance and lemmas -/
+noncomputable instance : RatCast ℂ where
+  ratCast := Rat.castRec
+
+/-! ### Cast lemmas -/
+
+@[simp, norm_cast]
+theorem ofReal_nat_cast (n : ℕ) : ((n : ℝ) : ℂ) = n :=
+  map_natCast ofReal n
+#align complex.of_real_nat_cast Complex.ofReal_nat_cast
+
+@[simp, norm_cast]
+theorem nat_cast_re (n : ℕ) : (n : ℂ).re = n := by rw [← ofReal_nat_cast, ofReal_re]
+#align complex.nat_cast_re Complex.nat_cast_re
+
+@[simp, norm_cast]
+theorem nat_cast_im (n : ℕ) : (n : ℂ).im = 0 := by rw [← ofReal_nat_cast, ofReal_im]
+#align complex.nat_cast_im Complex.nat_cast_im
+
+@[simp, norm_cast]
+theorem ofReal_int_cast (n : ℤ) : ((n : ℝ) : ℂ) = n :=
+  map_intCast ofReal n
+#align complex.of_real_int_cast Complex.ofReal_int_cast
+
+@[simp, norm_cast]
+theorem int_cast_re (n : ℤ) : (n : ℂ).re = n := by rw [← ofReal_int_cast, ofReal_re]
+#align complex.int_cast_re Complex.int_cast_re
+
+@[simp, norm_cast]
+theorem int_cast_im (n : ℤ) : (n : ℂ).im = 0 := by rw [← ofReal_int_cast, ofReal_im]
+#align complex.int_cast_im Complex.int_cast_im
+
+@[simp, norm_cast]
+theorem rat_cast_im (q : ℚ) : (q : ℂ).im = 0 := by
+  show (Rat.castRec q : ℂ).im = 0
+  cases q
+  simp [Rat.castRec]
+#align complex.rat_cast_im Complex.rat_cast_im
 
+@[simp, norm_cast]
+theorem rat_cast_re (q : ℚ) : (q : ℂ).re = (q : ℝ) := by
+  show (Rat.castRec q : ℂ).re = _
+  cases q
+  simp [Rat.castRec, normSq, Rat.mk_eq_divInt, Rat.mkRat_eq_div, div_eq_mul_inv, *]
+#align complex.rat_cast_re Complex.rat_cast_re
+
+/-! ### Field instance and lemmas -/
 
 noncomputable instance instField : Field ℂ :=
-{ inv := Inv.inv
+{ qsmul := fun n z => n • z
+  qsmul_eq_mul' := fun n z => ext_iff.2 <| by simp [Rat.smul_def, smul_re, smul_im]
+  inv := Inv.inv
   mul_inv_cancel := @Complex.mul_inv_cancel
   inv_zero := Complex.inv_zero }
 #align complex.field Complex.instField
@@ -828,51 +899,11 @@ theorem normSq_div (z w : ℂ) : normSq (z / w) = normSq z / normSq w :=
   map_div₀ normSq z w
 #align complex.norm_sq_div Complex.normSq_div
 
-/-! ### Cast lemmas -/
-
-
-@[simp, norm_cast]
-theorem ofReal_nat_cast (n : ℕ) : ((n : ℝ) : ℂ) = n :=
-  map_natCast ofReal n
-#align complex.of_real_nat_cast Complex.ofReal_nat_cast
-
-@[simp, norm_cast]
-theorem nat_cast_re (n : ℕ) : (n : ℂ).re = n := by rw [← ofReal_nat_cast, ofReal_re]
-#align complex.nat_cast_re Complex.nat_cast_re
-
-@[simp, norm_cast]
-theorem nat_cast_im (n : ℕ) : (n : ℂ).im = 0 := by rw [← ofReal_nat_cast, ofReal_im]
-#align complex.nat_cast_im Complex.nat_cast_im
-
-@[simp, norm_cast]
-theorem ofReal_int_cast (n : ℤ) : ((n : ℝ) : ℂ) = n :=
-  map_intCast ofReal n
-#align complex.of_real_int_cast Complex.ofReal_int_cast
-
-@[simp, norm_cast]
-theorem int_cast_re (n : ℤ) : (n : ℂ).re = n := by rw [← ofReal_int_cast, ofReal_re]
-#align complex.int_cast_re Complex.int_cast_re
-
-@[simp, norm_cast]
-theorem int_cast_im (n : ℤ) : (n : ℂ).im = 0 := by rw [← ofReal_int_cast, ofReal_im]
-#align complex.int_cast_im Complex.int_cast_im
-
 @[simp, norm_cast]
 theorem ofReal_rat_cast (n : ℚ) : ((n : ℝ) : ℂ) = (n : ℂ) :=
   map_ratCast ofReal n
 #align complex.of_real_rat_cast Complex.ofReal_rat_cast
 
--- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
-@[simp]
-theorem rat_cast_re (q : ℚ) : (q : ℂ).re = (q : ℂ) := by
- rw [← ofReal_rat_cast, ofReal_re]
-#align complex.rat_cast_re Complex.rat_cast_re
-
--- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
-@[simp]
-theorem rat_cast_im (q : ℚ) : (q : ℂ).im = 0 := by
- rw [← ofReal_rat_cast, ofReal_im]
-#align complex.rat_cast_im Complex.rat_cast_im
 
 /-! ### Characteristic zero -/
 
@@ -882,6 +913,9 @@ instance charZero : CharZero ℂ :=
     rwa [← ofReal_nat_cast, ofReal_eq_zero, Nat.cast_eq_zero] at h
 #align complex.char_zero_complex Complex.charZero
 
+-- Test if the `ℚ` smul instance is correct.
+example : (Complex.instSMulComplex : SMul ℚ ℂ) = (Algebra.toSMul : SMul ℚ ℂ) := rfl
+
 /-- A complex number `z` plus its conjugate `conj z` is `2` times its real part. -/
 theorem re_eq_add_conj (z : ℂ) : (z.re : ℂ) = (z + conj z) / 2 := by
   have : (↑(↑2 : ℝ) : ℂ)  = (2 : ℂ) := by rfl

diff --git a/Mathlib/Data/Complex/Module.lean b/Mathlib/Data/Complex/Module.lean
@@ -53,27 +53,6 @@ open ComplexConjugate
 
 variable {R : Type _} {S : Type _}
 
-section
-
-variable [SMul R ℝ]
-
-/- The useless `0` multiplication in `smul` is to make sure that
-`RestrictScalars.module ℝ ℂ ℂ = Complex.module` definitionally. -/
-instance : SMul R ℂ where smul r x := ⟨r • x.re - 0 * x.im, r • x.im + 0 * x.re⟩
-
-theorem smul_re (r : R) (z : ℂ) : (r • z).re = r • z.re := by simp [(· • ·), SMul.smul]
-#align complex.smul_re Complex.smul_re
-
-theorem smul_im (r : R) (z : ℂ) : (r • z).im = r • z.im := by simp [(· • ·), SMul.smul]
-#align complex.smul_im Complex.smul_im
-
-@[simp]
-theorem real_smul {x : ℝ} {z : ℂ} : x • z = x * z :=
-  rfl
-#align complex.real_smul Complex.real_smul
-
-end
-
 instance [SMul R ℝ] [SMul S ℝ] [SMulCommClass R S ℝ] : SMulCommClass R S ℂ where
   smul_comm r s x := by ext <;> simp [smul_re, smul_im, smul_comm]