chore: make Complex.ext only a local ext lemma (#9010)

In accordance with this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Complex.2Eext/near/393560116), this remove `Complex.ext` from the global `ext` attribute list and only enables it locally in certain files.
leanprover-community · Dec 12, 2023 · 3cfc8ef · 3cfc8ef
1 parent 27afdd8
commit 3cfc8ef
Show file tree

Hide file tree

Showing 10 changed files with 14 additions and 9 deletions.
diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
@@ -526,7 +526,7 @@ theorem kahler_neg_orientation (x y : E) : (-o).kahler x y = conj (o.kahler x y)
 
 theorem kahler_mul (a x y : E) : o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y := by
   trans ((‖a‖ ^ 2 :) : ℂ) * o.kahler x y
-  · ext
+  · apply Complex.ext
     · simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
         Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
       rw [real_inner_comm a x, o.areaForm_swap x a]
@@ -622,7 +622,7 @@ protected theorem rightAngleRotation (z : ℂ) :
 @[simp]
 protected theorem kahler (w z : ℂ) : Complex.orientation.kahler w z = conj w * z := by
   rw [Orientation.kahler_apply_apply]
-  ext1 <;> simp
+  apply Complex.ext <;> simp
 #align complex.kahler Complex.kahler
 
 end Complex

diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@@ -58,7 +58,7 @@ theorem abs_mul_exp_arg_mul_I (x : ℂ) : ↑(abs x) * exp (arg x * I) = x := by
   rcases eq_or_ne x 0 with (rfl | hx)
   · simp
   · have : abs x ≠ 0 := abs.ne_zero hx
-    ext <;> field_simp [sin_arg, cos_arg hx, this, mul_comm (abs x)]
+    apply Complex.ext <;> field_simp [sin_arg, cos_arg hx, this, mul_comm (abs x)]
 set_option linter.uppercaseLean3 false in
 #align complex.abs_mul_exp_arg_mul_I Complex.abs_mul_exp_arg_mul_I
 

diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean
@@ -51,11 +51,13 @@ theorem eta : ∀ z : ℂ, Complex.mk z.re z.im = z
   | ⟨_, _⟩ => rfl
 #align complex.eta Complex.eta
 
-@[ext]
+-- We only mark this lemma with `ext` *locally* to avoid it applying whenever terms of `ℂ` appear.
 theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
   | ⟨_, _⟩, ⟨_, _⟩, rfl, rfl => rfl
 #align complex.ext Complex.ext
 
+attribute [local ext] Complex.ext
+
 theorem ext_iff {z w : ℂ} : z = w ↔ z.re = w.re ∧ z.im = w.im :=
   ⟨fun H => by simp [H], fun h => ext h.1 h.2⟩
 #align complex.ext_iff Complex.ext_iff

diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -839,7 +839,7 @@ theorem sin_mul_I : sin (x * I) = sinh x * I := by
     ring_nf
     simp
   rw [← neg_neg (sinh x), ← h]
-  ext <;> simp
+  apply Complex.ext <;> simp
 set_option linter.uppercaseLean3 false in
 #align complex.sin_mul_I Complex.sin_mul_I
 

diff --git a/Mathlib/Data/Complex/Module.lean b/Mathlib/Data/Complex/Module.lean
@@ -50,6 +50,8 @@ open ComplexConjugate
 
 variable {R : Type*} {S : Type*}
 
+attribute [local ext] Complex.ext
+
 -- Test that the `SMul ℚ ℂ` instance is correct.
 example : (Complex.instSMulRealComplex : SMul ℚ ℂ) = (Algebra.toSMul : SMul ℚ ℂ) := rfl
 

diff --git a/Mathlib/Data/Complex/Order.lean b/Mathlib/Data/Complex/Order.lean
@@ -97,7 +97,7 @@ theorem not_lt_zero_iff {z : ℂ} : ¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0 :=
 #align complex.not_lt_zero_iff Complex.not_lt_zero_iff
 
 theorem eq_re_of_ofReal_le {r : ℝ} {z : ℂ} (hz : (r : ℂ) ≤ z) : z = z.re := by
-  ext
+  apply Complex.ext
   rfl
   simp only [← (Complex.le_def.1 hz).2, Complex.zero_im, Complex.ofReal_im]
 #align complex.eq_re_of_real_le Complex.eq_re_of_ofReal_le

diff --git a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean
@@ -432,6 +432,7 @@ theorem splits_ℚ_ℂ {p : ℚ[X]} : Fact (p.Splits (algebraMap ℚ ℂ)) :=
 #align polynomial.gal.splits_ℚ_ℂ Polynomial.Gal.splits_ℚ_ℂ
 
 attribute [local instance] splits_ℚ_ℂ
+attribute [local ext] Complex.ext
 
 /-- The number of complex roots equals the number of real roots plus
     the number of roots not fixed by complex conjugation (i.e. with some imaginary component). -/

diff --git a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
@@ -508,7 +508,7 @@ theorem singularPart_add_withDensity_rnDeriv_eq [c.HaveLebesgueDecomposition μ]
   conv_rhs => rw [← c.toComplexMeasure_to_signedMeasure]
   ext i hi : 1
   rw [VectorMeasure.add_apply, SignedMeasure.toComplexMeasure_apply]
-  ext
+  apply Complex.ext
   · rw [Complex.add_re, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← IsROrC.re_eq_complex_re,
       ← integral_re (c.integrable_rnDeriv μ).integrableOn, IsROrC.re_eq_complex_re,
       ← withDensityᵥ_apply _ hi]

diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean
@@ -197,7 +197,7 @@ def IsReal.embedding {φ : K →+* ℂ} (hφ : IsReal φ) : K →+* ℝ where
 @[simp]
 theorem IsReal.coe_embedding_apply {φ : K →+* ℂ} (hφ : IsReal φ) (x : K) :
     (hφ.embedding x : ℂ) = φ x := by
-  ext
+  apply Complex.ext
   · rfl
   · rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]
     exact RingHom.congr_fun hφ x

diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
@@ -264,7 +264,7 @@ theorem cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤
     rw [this] at hζ
     linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm]
     · contrapose! hζ₀
-      ext <;> simp [hζ₀, h.2]
+      apply Complex.ext <;> simp [hζ₀, h.2]
   have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by
     erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ)]
     simp only [Complex.coe_algebraMap, Complex.ofReal_eq_zero]