From fe3b04878ed85953099daea56068341f9e3c98ef Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Fri, 25 Oct 2024 15:19:51 +0200
Subject: [PATCH 1/8] 1st commit

---
 .../NumberField/CanonicalEmbedding/Basic.lean | 243 ++++++++++++++++++
 .../CanonicalEmbedding/ConvexBody.lean        |   9 -
 Mathlib/Topology/Algebra/Module/Basic.lean    |  60 ++++-
 3 files changed, 296 insertions(+), 16 deletions(-)

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index f119b3f3072eb..a710e51ddd407 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.Algebra.Module.ZLattice.Basic
+import Mathlib.MeasureTheory.Measure.Haar.Unique
 import Mathlib.NumberTheory.NumberField.FractionalIdeal
 import Mathlib.NumberTheory.NumberField.Units.Basic
 
@@ -182,6 +183,26 @@ open NumberField.InfinitePlace Module Finset
 abbrev mixedSpace :=
   ({w : InfinitePlace K // IsReal w} → ℝ) × ({w : InfinitePlace K // IsComplex w} → ℂ)
 
+section Measure
+
+open MeasureTheory.Measure MeasureTheory
+
+variable [NumberField K]
+
+open Classical in
+instance : IsAddHaarMeasure (volume : Measure (mixedSpace K)) :=
+  prod.instIsAddHaarMeasure volume volume
+
+open Classical in
+instance : NoAtoms (volume : Measure (mixedSpace K)) := by
+  obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
+  by_cases hw : IsReal w
+  · exact @prod.instNoAtoms_fst _ _ _ _ volume volume _ (pi_noAtoms ⟨w, hw⟩)
+  · exact @prod.instNoAtoms_snd _ _ _ _ volume volume _
+      (pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩)
+
+end Measure
+
 /-- The mixed embedding of a number field `K` into the mixed space of `K`. -/
 noncomputable def _root_.NumberField.mixedEmbedding : K →+* (mixedSpace K) :=
   RingHom.prod (Pi.ringHom fun w => embedding_of_isReal w.prop)
@@ -746,4 +767,226 @@ theorem fundamentalDomain_idealLattice :
 
 end integerLattice
 
+noncomputable section plusPart
+
+variable {K}
+
+open Classical in
+/-- Let `s` be a set of real places, define the continuous linear equiv of the mixed space that
+changes sign at places in `s` and leaves the rest unchanged. -/
+def negAt (s : Set {w : InfinitePlace K // IsReal w}) :
+    (mixedSpace K) ≃L[ℝ] (mixedSpace K) :=
+  (ContinuousLinearEquiv.piCongrRight
+    fun w ↦ if w ∈ s then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prod
+      (ContinuousLinearEquiv.refl ℝ _)
+
+@[simp]
+theorem negAt_apply_of_isReal_and_mem  {s : Set {w // IsReal w}} (x : mixedSpace K)
+    {w : {w // IsReal w}} (hw : w ∈ s) :
+    (negAt s x).1 w = - x.1 w := by
+  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
+    if_pos hw, ContinuousLinearEquiv.neg_apply]
+
+@[simp]
+theorem negAt_apply_of_isReal_and_not_mem {s : Set {w // IsReal w}} (x : mixedSpace K)
+    {w : {w // IsReal w}} (hw : w ∉ s) :
+    (negAt s x).1 w = x.1 w := by
+  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
+    if_neg hw, ContinuousLinearEquiv.refl_apply]
+
+@[simp]
+theorem negAt_apply_abs_of_isReal {s : Set {w // IsReal w}} (x : mixedSpace K)
+    (w : {w // IsReal w}) :
+    |(negAt s x).1 w| = |x.1 w| := by
+  by_cases hw : w ∈ s
+  · rw [negAt_apply_of_isReal_and_mem _ hw, abs_neg]
+  · rw [negAt_apply_of_isReal_and_not_mem _ hw]
+
+@[simp]
+theorem negAt_apply_snd (s : Set {w // IsReal w}) (x : mixedSpace K) :
+    (negAt s x).2 = x.2 := rfl
+
+open MeasureTheory Classical in
+/-- `negAt` preserves the volume . -/
+theorem volume_preserving_negAt [NumberField K] (s : Set {w : InfinitePlace K // IsReal w}) :
+    MeasurePreserving (negAt s) := by
+  refine MeasurePreserving.prod (volume_preserving_pi fun w ↦ ?_) (MeasurePreserving.id _)
+  by_cases hw : w ∈ s
+  · simp_rw [if_pos hw]
+    exact Measure.measurePreserving_neg _
+  · simp_rw [if_neg hw]
+    exact MeasurePreserving.id _
+
+/-- `negAt` preserves `normAtPlace`. -/
+@[simp]
+theorem normAtPlace_negAt (s : Set {w // IsReal w}) (x : mixedSpace K) (w : InfinitePlace K) :
+    normAtPlace w (negAt s x) = normAtPlace w x := by
+  obtain hw | hw := isReal_or_isComplex w
+  · simp_rw [normAtPlace_apply_isReal hw, Real.norm_eq_abs, negAt_apply_abs_of_isReal]
+  · simp_rw [normAtPlace_apply_isComplex hw, congr_fun (negAt_apply_snd s x) ⟨w, hw⟩]
+
+/-- `negAt` preserves the `norm`. -/
+@[simp]
+theorem norm_negAt [NumberField K] (s : Set {w // IsReal w}) (x : mixedSpace K) :
+    mixedEmbedding.norm (negAt s x) = mixedEmbedding.norm x :=
+  norm_eq_of_normAtPlace_eq (fun w ↦ normAtPlace_negAt _ _ w)
+
+open ContinuousLinearEquiv in
+/-- `negAt` is equal to its inverse. -/
+theorem negAt_symm (s : Set {w : InfinitePlace K // IsReal w}) :
+    (negAt s).symm = negAt s := by
+  ext x w
+  · by_cases hw : w ∈ s
+    · simp_rw [negAt_apply_of_isReal_and_mem _ hw, negAt, prod_symm,
+        ContinuousLinearEquiv.prod_apply, piCongrRight_symm_apply, if_pos hw, symm_neg, neg_apply]
+    · simp_rw [negAt_apply_of_isReal_and_not_mem _ hw, negAt, prod_symm,
+        ContinuousLinearEquiv.prod_apply, piCongrRight_symm_apply, if_neg hw, refl_symm, refl_apply]
+  · rfl
+
+variable (A : Set (mixedSpace K))
+
+/-- `negAt s A` is also equal to the preimage of `A` by `negAt s`. This fact can be useful to
+simplify some proofs. -/
+theorem negAt_preimage (s : Set {w // IsReal w} ) :
+    negAt s ⁻¹' A = negAt s '' A := by
+  rw [ContinuousLinearEquiv.image_eq_preimage, negAt_symm]
+
+/-- The `Plus` part of a subset `A` of the `mixedSpace` is the set of points in `A` that are
+positive at all real places. -/
+abbrev plusPart : Set (mixedSpace K) := A ∩ {x | ∀ w, 0 < x.1 w}
+
+/-- Let `s` be a set of real places. `negAtPlusPart A s` is the image of `plusPart A` by `negAt s`,
+thus it is equal to the set of elements of `A` that are negative at real places in `s` and
+positive at real places not in `s`. -/
+abbrev negAtPlusPart (s : Set {w : InfinitePlace K // IsReal w}) : Set (mixedSpace K) :=
+    negAt s '' (plusPart A)
+
+theorem negAtPlusPart_neg_of_mem {s : Set {w // IsReal w}} {x : mixedSpace K}
+    (hx : x ∈ negAtPlusPart A s) {w : {w // IsReal w}} (hw : w ∈ s) :
+    x.1 w < 0 := by
+  obtain ⟨y, hy, rfl⟩ := hx
+  rw [negAt_apply_of_isReal_and_mem _ hw, neg_lt_zero]
+  exact hy.2 w
+
+theorem negAtPlusPart_pos_of_not_mem {s : Set {w // IsReal w}} {x : mixedSpace K}
+    (hx : x ∈ negAtPlusPart A s) {w : {w // IsReal w}} (hw : w ∉ s) :
+    0 < x.1 w := by
+  obtain ⟨y, hy, rfl⟩ := hx
+  rw [negAt_apply_of_isReal_and_not_mem _ hw]
+  exact hy.2 w
+
+open Classical in
+theorem mem_negAtPlusPart_of_mem (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A)
+    (s : Set {w // IsReal w}) {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ : ∀ w, x.1 w ≠ 0) :
+    x ∈ negAtPlusPart A s ↔ (∀ w, w ∈ s → x.1 w < 0) ∧ (∀ w, w ∉ s → x.1 w > 0) := by
+  refine ⟨fun hx ↦ ⟨fun _ hw ↦ negAtPlusPart_neg_of_mem A hx hw,
+      fun _ hw ↦ negAtPlusPart_pos_of_not_mem A hx hw⟩,
+      fun ⟨h₁, h₂⟩ ↦ ⟨(fun w ↦ |x.1 w|, x.2), ⟨(hA x).mp hx₁, fun w ↦ abs_pos.mpr (hx₂ w)⟩, ?_⟩⟩
+  ext w
+  · by_cases hw : w ∈ s
+    · simp_rw [negAt_apply_of_isReal_and_mem _ hw, abs_of_neg (h₁ w hw), neg_neg]
+    · simp_rw [negAt_apply_of_isReal_and_not_mem _ hw, abs_of_pos (h₂ w hw)]
+  · rfl
+
+/-- The sets `negAtPlusPart` are pairwise disjoint. -/
+theorem disjoint_negAtPlusPart : Pairwise (Disjoint on (negAtPlusPart A)) := by
+  classical
+  intro s t hst
+  refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_
+  obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := by
+    exact Set.symmDiff_nonempty.mpr hst
+  · exact lt_irrefl _ <|
+      (negAtPlusPart_neg_of_mem A hx hw.1).trans (negAtPlusPart_pos_of_not_mem A hx' hw.2)
+  · exact lt_irrefl _ <|
+      (negAtPlusPart_neg_of_mem A hx' hw.1).trans (negAtPlusPart_pos_of_not_mem A hx hw.2)
+
+/-- For `x : mixedSpace K`, the set `signSet x` is the set of real places `w` s.t. `x w ≤ 0`. -/
+def signSet (x : mixedSpace K) : Set {w : InfinitePlace K // IsReal w} := {w | x.1 w ≤ 0}
+
+@[simp]
+theorem negAt_signSet_apply_of_isReal (x : mixedSpace K) (w : {w // IsReal w}) :
+    (negAt (signSet x) x).1 w = |x.1 w| := by
+  by_cases hw : x.1 w ≤ 0
+  · rw [negAt_apply_of_isReal_and_mem _ hw, abs_of_nonpos hw]
+  · rw [negAt_apply_of_isReal_and_not_mem _ hw, abs_of_pos (lt_of_not_ge hw)]
+
+@[simp]
+theorem negAt_signSet_apply_of_isComplex (x : mixedSpace K) (w : {w // IsComplex w}) :
+    (negAt (signSet x) x).2 w = x.2 w := rfl
+
+/-- Assume that the images of `plusPart A` under `negAt` are all subset of `A`. Then, the union of
+all the `negPlusPart` and the set of elements of `A` that are zero at at least one real place is
+equal to `A`. -/
+theorem iUnion_negAtPlusPart_union (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A) :
+    (⋃ s, negAtPlusPart A s) ∪ (A ∩ (⋃ w, {x | x.1 w = 0})) = A := by
+  ext x
+  rw [Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iUnion]
+  refine ⟨?_, fun h ↦ ?_⟩
+  · rintro (⟨s, ⟨x, ⟨hx, _⟩, rfl⟩⟩ | h)
+    · simp_rw (config := {singlePass := true}) [hA, negAt_apply_abs_of_isReal, negAt_apply_snd]
+      rwa [← hA]
+    · exact h.left
+  · obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)
+    · exact Or.inr ⟨h, hx⟩
+    · refine Or.inl ⟨signSet x,
+        (mem_negAtPlusPart_of_mem A hA _ h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
+      · exact lt_of_le_of_ne hw (hx w)
+      · exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))
+
+open MeasureTheory
+
+variable [NumberField K]
+
+open Classical in
+/-- The set of points in the mixedSpace that are equal to `0` at a fixed (real) place has
+volume zero. -/
+theorem volume_eq_zero (w : {w // IsReal w}) :
+    volume ({x : mixedSpace K | x.1 w = 0}) = 0 := by
+  let A : AffineSubspace ℝ (mixedSpace K) :=
+    Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x.1 w = 0}, by aesop⟩, rfl⟩ (by aesop))
+  convert Measure.addHaar_affineSubspace volume A fun h ↦ ?_
+  have : 1 ∈ A := h ▸ Set.mem_univ _
+  simp [A] at this
+
+open Classical in
+theorem iUnion_negAtPart_ae (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A) :
+    ⋃ s, negAtPlusPart A s =ᵐ[volume] A := by
+  nth_rewrite 2 [← iUnion_negAtPlusPart_union A hA]
+  refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm
+  exact measure_mono_null Set.inter_subset_right
+    (measure_iUnion_null_iff.mpr fun _ ↦ volume_eq_zero _)
+
+variable {A} in
+theorem measurableSet_plusPart (hm : MeasurableSet A) :
+    MeasurableSet (plusPart A) := by
+  convert_to MeasurableSet (A ∩ (⋂ w, {x | 0 < x.1 w}))
+  · ext; simp
+  · refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)
+    exact measurableSet_lt measurable_const ((measurable_pi_apply _).comp' measurable_fst)
+
+theorem measurableSet_negAtPlusPart (s : Set {w : InfinitePlace K // IsReal w})
+    (hm : MeasurableSet A) :
+    MeasurableSet (negAtPlusPart A s) := by
+  rw [negAtPlusPart, ← negAt_preimage]
+  exact (measurableSet_plusPart hm).preimage (negAt s).continuous.measurable
+
+open Classical in
+theorem volume_negAtPlusPart (hm : MeasurableSet A) (s : Set {w // IsReal w}) :
+    volume (negAtPlusPart A s) = volume (plusPart A) := by
+  rw [negAtPlusPart, ← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
+    (volume_preserving_negAt s).measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]
+
+open Classical in
+/-- If a subset `A` of the `mixedSpace` is symmetric at real places, then its volume is
+`2^r₁` times the volume of its `plusPart` where `r₁` is the number of real places. -/
+theorem volume_eq_two_pow_mul_volume_plusPart (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A)
+    (hm : MeasurableSet A) :
+    volume A = 2 ^ NrRealPlaces K * volume (plusPart A) := by
+  simp_rw [← measure_congr (iUnion_negAtPart_ae A hA), measure_iUnion (disjoint_negAtPlusPart A)
+    (fun _ ↦ measurableSet_negAtPlusPart A _ hm), volume_negAtPlusPart _ hm, tsum_fintype,
+    Finset.sum_const, Finset.card_univ, NrRealPlaces, nsmul_eq_mul, Fintype.card_set, Nat.cast_pow,
+    Nat.cast_ofNat]
+
+end plusPart
+
 end NumberField.mixedEmbedding
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
index 36a06aabe738b..371beddf0d6db 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
@@ -77,15 +77,6 @@ open scoped Classical
 
 variable [NumberField K]
 
-instance : IsAddHaarMeasure (volume : Measure (mixedSpace K)) := prod.instIsAddHaarMeasure _ _
-
-instance : NoAtoms (volume : Measure (mixedSpace K)) := by
-  obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
-  by_cases hw : IsReal w
-  · exact @prod.instNoAtoms_fst _ _ _ _ volume volume _ (pi_noAtoms ⟨w, hw⟩)
-  · exact @prod.instNoAtoms_snd _ _ _ _ volume volume _
-      (pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩)
-
 /-- The fudge factor that appears in the formula for the volume of `convexBodyLT`. -/
 noncomputable abbrev convexBodyLTFactor : ℝ≥0 :=
   (2 : ℝ≥0) ^ NrRealPlaces K * NNReal.pi ^ NrComplexPlaces K
diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
index c2feb47fccf1a..5ae3cb3b14650 100644
--- a/Mathlib/Topology/Algebra/Module/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -4,15 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis,
   Heather Macbeth
 -/
+import Mathlib.Algebra.Module.Opposites
+import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.LinearAlgebra.Projection
 import Mathlib.Topology.Algebra.Ring.Basic
-import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Algebra.UniformGroup
-import Mathlib.Topology.UniformSpace.UniformEmbedding
-import Mathlib.Algebra.Algebra.Defs
-import Mathlib.LinearAlgebra.Projection
-import Mathlib.LinearAlgebra.Pi
-import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.Algebra.Module.Opposites
 
 /-!
 # Theory of topological modules and continuous linear maps.
@@ -1733,6 +1729,10 @@ protected def refl : M₁ ≃L[R₁] M₁ :=
 
 end
 
+@[simp]
+theorem refl_apply (x : M₁) :
+    ContinuousLinearEquiv.refl R₁ M₁ x = x := rfl
+
 @[simp, norm_cast]
 theorem coe_refl : ↑(ContinuousLinearEquiv.refl R₁ M₁) = ContinuousLinearMap.id R₁ M₁ :=
   rfl
@@ -2001,6 +2001,32 @@ def arrowCongrEquiv (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[
     ContinuousLinearMap.ext fun x => by
       simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]
 
+/-- Combine a family of continuous linear equivalences into a continuous linear equivalence of
+pi-types. -/
+def piCongrRight {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)]
+    [∀ i, AddCommMonoid (M i)] [∀ i, Module R₁ (M i)] {N : ι → Type*} [∀ i, TopologicalSpace (N i)]
+    [∀ i, AddCommMonoid (N i)] [∀ i, Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i) :
+    ((i : ι) → M i) ≃L[R₁] (i : ι) → N i :=
+  { LinearEquiv.piCongrRight fun i ↦ f i with
+    continuous_toFun := by
+      exact continuous_pi fun i ↦ (f i).continuous_toFun.comp (continuous_apply i)
+    continuous_invFun := by
+      exact continuous_pi fun i => (f i).continuous_invFun.comp (continuous_apply i) }
+
+@[simp]
+theorem piCongrRight_apply {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)]
+    [∀ i, AddCommMonoid (M i)] [∀ i, Module R₁ (M i)] {N : ι → Type*} [∀ i, TopologicalSpace (N i)]
+    [∀ i, AddCommMonoid (N i)] [∀ i, Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i)
+    (m : (i : ι) → M i) (i : ι) :
+    piCongrRight f m i = (f i) (m i) := rfl
+
+@[simp]
+theorem piCongrRight_symm_apply {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)]
+    [∀ i, AddCommMonoid (M i)] [∀ i, Module R₁ (M i)] {N : ι → Type*} [∀ i, TopologicalSpace (N i)]
+    [∀ i, AddCommMonoid (N i)] [∀ i, Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i)
+    (n : (i : ι) → N i) (i : ι) :
+    (piCongrRight f).symm n i = (f i).symm (n i) := rfl
+
 end AddCommMonoid
 
 section AddCommGroup
@@ -2036,6 +2062,26 @@ theorem skewProd_symm_apply (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M
     (e.skewProd e' f).symm x = (e.symm x.1, e'.symm (x.2 - f (e.symm x.1))) :=
   rfl
 
+variable (R) in
+/-- The negation map as a continuous linear equivalence. -/
+def neg [ContinuousNeg M] :
+    M ≃L[R] M :=
+  { LinearEquiv.neg R with
+    continuous_toFun := continuous_neg
+    continuous_invFun := continuous_neg }
+
+@[simp]
+theorem coe_neg [ContinuousNeg M] :
+    (neg R : M → M) = -id := rfl
+
+@[simp]
+theorem neg_apply [ContinuousNeg M] (x : M) :
+    neg R x = -x := by simp
+
+@[simp]
+theorem symm_neg [ContinuousNeg M] :
+    (neg R : M ≃L[R] M).symm = neg R := rfl
+
 end AddCommGroup
 
 section Ring

From 2aa88ad8714c4f56befa70f4622ed9376f0ba3f7 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Fri, 25 Oct 2024 16:09:56 +0200
Subject: [PATCH 2/8] Clean up

---
 .../NumberField/CanonicalEmbedding/Basic.lean | 118 +++++++++---------
 1 file changed, 62 insertions(+), 56 deletions(-)

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index a710e51ddd407..267265b87dc8a 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -769,43 +769,44 @@ end integerLattice
 
 noncomputable section plusPart
 
-variable {K}
+variable {K} (s : Set {w : InfinitePlace K // IsReal w})
 
 open Classical in
 /-- Let `s` be a set of real places, define the continuous linear equiv of the mixed space that
 changes sign at places in `s` and leaves the rest unchanged. -/
-def negAt (s : Set {w : InfinitePlace K // IsReal w}) :
+def negAt :
     (mixedSpace K) ≃L[ℝ] (mixedSpace K) :=
   (ContinuousLinearEquiv.piCongrRight
     fun w ↦ if w ∈ s then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prod
       (ContinuousLinearEquiv.refl ℝ _)
 
+variable {s}
+
 @[simp]
-theorem negAt_apply_of_isReal_and_mem  {s : Set {w // IsReal w}} (x : mixedSpace K)
-    {w : {w // IsReal w}} (hw : w ∈ s) :
+theorem negAt_apply_of_isReal_and_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∈ s) :
     (negAt s x).1 w = - x.1 w := by
   simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
     if_pos hw, ContinuousLinearEquiv.neg_apply]
 
 @[simp]
-theorem negAt_apply_of_isReal_and_not_mem {s : Set {w // IsReal w}} (x : mixedSpace K)
-    {w : {w // IsReal w}} (hw : w ∉ s) :
+theorem negAt_apply_of_isReal_and_not_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∉ s) :
     (negAt s x).1 w = x.1 w := by
   simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
     if_neg hw, ContinuousLinearEquiv.refl_apply]
 
 @[simp]
-theorem negAt_apply_abs_of_isReal {s : Set {w // IsReal w}} (x : mixedSpace K)
-    (w : {w // IsReal w}) :
-    |(negAt s x).1 w| = |x.1 w| := by
-  by_cases hw : w ∈ s
-  · rw [negAt_apply_of_isReal_and_mem _ hw, abs_neg]
-  · rw [negAt_apply_of_isReal_and_not_mem _ hw]
+theorem negAt_apply_of_isComplex (x : mixedSpace K) (w : {w // IsComplex w}) :
+    (negAt s x).2 w = x.2 w := rfl
 
 @[simp]
-theorem negAt_apply_snd (s : Set {w // IsReal w}) (x : mixedSpace K) :
+theorem negAt_apply_snd (x : mixedSpace K) :
     (negAt s x).2 = x.2 := rfl
 
+@[simp]
+theorem negAt_apply_abs_of_isReal (x : mixedSpace K) (w : {w // IsReal w}) :
+    |(negAt s x).1 w| = |x.1 w| := by
+  by_cases hw : w ∈ s <;> simp [hw]
+
 open MeasureTheory Classical in
 /-- `negAt` preserves the volume . -/
 theorem volume_preserving_negAt [NumberField K] (s : Set {w : InfinitePlace K // IsReal w}) :
@@ -823,7 +824,7 @@ theorem normAtPlace_negAt (s : Set {w // IsReal w}) (x : mixedSpace K) (w : Infi
     normAtPlace w (negAt s x) = normAtPlace w x := by
   obtain hw | hw := isReal_or_isComplex w
   · simp_rw [normAtPlace_apply_isReal hw, Real.norm_eq_abs, negAt_apply_abs_of_isReal]
-  · simp_rw [normAtPlace_apply_isComplex hw, congr_fun (negAt_apply_snd s x) ⟨w, hw⟩]
+  · simp_rw [normAtPlace_apply_isComplex hw, negAt_apply_of_isComplex]
 
 /-- `negAt` preserves the `norm`. -/
 @[simp]
@@ -845,51 +846,38 @@ theorem negAt_symm (s : Set {w : InfinitePlace K // IsReal w}) :
 
 variable (A : Set (mixedSpace K))
 
-/-- `negAt s A` is also equal to the preimage of `A` by `negAt s`. This fact can be useful to
-simplify some proofs. -/
-theorem negAt_preimage (s : Set {w // IsReal w} ) :
+variable (s) in
+/-- `negAt s A` is also equal to the preimage of `A` by `negAt s`. This fact is used to simplify
+some proofs. -/
+theorem negAt_preimage :
     negAt s ⁻¹' A = negAt s '' A := by
   rw [ContinuousLinearEquiv.image_eq_preimage, negAt_symm]
 
-/-- The `Plus` part of a subset `A` of the `mixedSpace` is the set of points in `A` that are
+/-- The `plusPart` of a subset `A` of the `mixedSpace` is the set of points in `A` that are
 positive at all real places. -/
 abbrev plusPart : Set (mixedSpace K) := A ∩ {x | ∀ w, 0 < x.1 w}
 
-/-- Let `s` be a set of real places. `negAtPlusPart A s` is the image of `plusPart A` by `negAt s`,
-thus it is equal to the set of elements of `A` that are negative at real places in `s` and
-positive at real places not in `s`. -/
-abbrev negAtPlusPart (s : Set {w : InfinitePlace K // IsReal w}) : Set (mixedSpace K) :=
+variable (s) in
+/-- For `s` a set of real places, `negAtPlusPart A s` is the image of `plusPart A` by `negAt s`. -/
+abbrev negAtPlusPart : Set (mixedSpace K) :=
     negAt s '' (plusPart A)
 
-theorem negAtPlusPart_neg_of_mem {s : Set {w // IsReal w}} {x : mixedSpace K}
-    (hx : x ∈ negAtPlusPart A s) {w : {w // IsReal w}} (hw : w ∈ s) :
+theorem negAtPlusPart_neg_of_mem {x : mixedSpace K} (hx : x ∈ negAtPlusPart s A )
+    {w : {w // IsReal w}} (hw : w ∈ s) :
     x.1 w < 0 := by
   obtain ⟨y, hy, rfl⟩ := hx
   rw [negAt_apply_of_isReal_and_mem _ hw, neg_lt_zero]
   exact hy.2 w
 
-theorem negAtPlusPart_pos_of_not_mem {s : Set {w // IsReal w}} {x : mixedSpace K}
-    (hx : x ∈ negAtPlusPart A s) {w : {w // IsReal w}} (hw : w ∉ s) :
+theorem negAtPlusPart_pos_of_not_mem {x : mixedSpace K} (hx : x ∈ negAtPlusPart s A)
+    {w : {w // IsReal w}} (hw : w ∉ s) :
     0 < x.1 w := by
   obtain ⟨y, hy, rfl⟩ := hx
   rw [negAt_apply_of_isReal_and_not_mem _ hw]
   exact hy.2 w
 
-open Classical in
-theorem mem_negAtPlusPart_of_mem (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A)
-    (s : Set {w // IsReal w}) {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ : ∀ w, x.1 w ≠ 0) :
-    x ∈ negAtPlusPart A s ↔ (∀ w, w ∈ s → x.1 w < 0) ∧ (∀ w, w ∉ s → x.1 w > 0) := by
-  refine ⟨fun hx ↦ ⟨fun _ hw ↦ negAtPlusPart_neg_of_mem A hx hw,
-      fun _ hw ↦ negAtPlusPart_pos_of_not_mem A hx hw⟩,
-      fun ⟨h₁, h₂⟩ ↦ ⟨(fun w ↦ |x.1 w|, x.2), ⟨(hA x).mp hx₁, fun w ↦ abs_pos.mpr (hx₂ w)⟩, ?_⟩⟩
-  ext w
-  · by_cases hw : w ∈ s
-    · simp_rw [negAt_apply_of_isReal_and_mem _ hw, abs_of_neg (h₁ w hw), neg_neg]
-    · simp_rw [negAt_apply_of_isReal_and_not_mem _ hw, abs_of_pos (h₂ w hw)]
-  · rfl
-
 /-- The sets `negAtPlusPart` are pairwise disjoint. -/
-theorem disjoint_negAtPlusPart : Pairwise (Disjoint on (negAtPlusPart A)) := by
+theorem disjoint_negAtPlusPart : Pairwise (Disjoint on (fun s ↦ negAtPlusPart s A)) := by
   classical
   intro s t hst
   refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_
@@ -914,11 +902,27 @@ theorem negAt_signSet_apply_of_isReal (x : mixedSpace K) (w : {w // IsReal w}) :
 theorem negAt_signSet_apply_of_isComplex (x : mixedSpace K) (w : {w // IsComplex w}) :
     (negAt (signSet x) x).2 w = x.2 w := rfl
 
-/-- Assume that the images of `plusPart A` under `negAt` are all subset of `A`. Then, the union of
-all the `negPlusPart` and the set of elements of `A` that are zero at at least one real place is
-equal to `A`. -/
-theorem iUnion_negAtPlusPart_union (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A) :
-    (⋃ s, negAtPlusPart A s) ∪ (A ∩ (⋃ w, {x | x.1 w = 0})) = A := by
+-- We will assume from now that `A` is symmetric at real places
+variable (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A)
+
+open Classical in
+include hA in
+theorem mem_negAtPlusPart_of_mem {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ : ∀ w, x.1 w ≠ 0) :
+    x ∈ negAtPlusPart s A ↔ (∀ w, w ∈ s → x.1 w < 0) ∧ (∀ w, w ∉ s → x.1 w > 0) := by
+  refine ⟨fun hx ↦ ⟨fun _ hw ↦ negAtPlusPart_neg_of_mem A hx hw,
+      fun _ hw ↦ negAtPlusPart_pos_of_not_mem A hx hw⟩,
+      fun ⟨h₁, h₂⟩ ↦ ⟨(fun w ↦ |x.1 w|, x.2), ⟨(hA x).mp hx₁, fun w ↦ abs_pos.mpr (hx₂ w)⟩, ?_⟩⟩
+  ext w
+  · by_cases hw : w ∈ s
+    · simp_rw [negAt_apply_of_isReal_and_mem _ hw, abs_of_neg (h₁ w hw), neg_neg]
+    · simp_rw [negAt_apply_of_isReal_and_not_mem _ hw, abs_of_pos (h₂ w hw)]
+  · rfl
+
+include hA in
+/-- Assume that `A`  is symmetric at real places then, the union of all the `negPlusPart`
+and of the set of elements of `A` that are zero at at least one real place is equal to `A`. -/
+theorem iUnion_negAtPlusPart_union :
+    (⋃ s, negAtPlusPart s A) ∪ (A ∩ (⋃ w, {x | x.1 w = 0})) = A := by
   ext x
   rw [Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iUnion]
   refine ⟨?_, fun h ↦ ?_⟩
@@ -929,7 +933,7 @@ theorem iUnion_negAtPlusPart_union (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|,
   · obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)
     · exact Or.inr ⟨h, hx⟩
     · refine Or.inl ⟨signSet x,
-        (mem_negAtPlusPart_of_mem A hA _ h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
+        (mem_negAtPlusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
       · exact lt_of_le_of_ne hw (hx w)
       · exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))
 
@@ -948,9 +952,10 @@ theorem volume_eq_zero (w : {w // IsReal w}) :
   have : 1 ∈ A := h ▸ Set.mem_univ _
   simp [A] at this
 
+include hA in
 open Classical in
-theorem iUnion_negAtPart_ae (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A) :
-    ⋃ s, negAtPlusPart A s =ᵐ[volume] A := by
+theorem iUnion_negAtPart_ae :
+    ⋃ s, negAtPlusPart s A =ᵐ[volume] A := by
   nth_rewrite 2 [← iUnion_negAtPlusPart_union A hA]
   refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm
   exact measure_mono_null Set.inter_subset_right
@@ -964,26 +969,27 @@ theorem measurableSet_plusPart (hm : MeasurableSet A) :
   · refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)
     exact measurableSet_lt measurable_const ((measurable_pi_apply _).comp' measurable_fst)
 
-theorem measurableSet_negAtPlusPart (s : Set {w : InfinitePlace K // IsReal w})
-    (hm : MeasurableSet A) :
-    MeasurableSet (negAtPlusPart A s) := by
+variable (s) in
+theorem measurableSet_negAtPlusPart (hm : MeasurableSet A) :
+    MeasurableSet (negAtPlusPart s A) := by
   rw [negAtPlusPart, ← negAt_preimage]
   exact (measurableSet_plusPart hm).preimage (negAt s).continuous.measurable
 
 open Classical in
-theorem volume_negAtPlusPart (hm : MeasurableSet A) (s : Set {w // IsReal w}) :
-    volume (negAtPlusPart A s) = volume (plusPart A) := by
+/-- The image of the `plusPart` of `A` by `negAt` have all the same volume as `plusPart A`. -/
+theorem volume_negAtPlusPart (hm : MeasurableSet A) :
+    volume (negAtPlusPart s A) = volume (plusPart A) := by
   rw [negAtPlusPart, ← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
     (volume_preserving_negAt s).measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]
 
+include hA in
 open Classical in
 /-- If a subset `A` of the `mixedSpace` is symmetric at real places, then its volume is
 `2^r₁` times the volume of its `plusPart` where `r₁` is the number of real places. -/
-theorem volume_eq_two_pow_mul_volume_plusPart (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A)
-    (hm : MeasurableSet A) :
+theorem volume_eq_two_pow_mul_volume_plusPart (hm : MeasurableSet A) :
     volume A = 2 ^ NrRealPlaces K * volume (plusPart A) := by
   simp_rw [← measure_congr (iUnion_negAtPart_ae A hA), measure_iUnion (disjoint_negAtPlusPart A)
-    (fun _ ↦ measurableSet_negAtPlusPart A _ hm), volume_negAtPlusPart _ hm, tsum_fintype,
+    (fun _ ↦ measurableSet_negAtPlusPart _ A hm), volume_negAtPlusPart _ hm, tsum_fintype,
     Finset.sum_const, Finset.card_univ, NrRealPlaces, nsmul_eq_mul, Fintype.card_set, Nat.cast_pow,
     Nat.cast_ofNat]
 

From c9e4a3b8d0a6779c605751cbb35f6fb6b87f4b8c Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Fri, 25 Oct 2024 16:35:33 +0200
Subject: [PATCH 3/8] Fix after merge

---
 .../NumberTheory/NumberField/CanonicalEmbedding/Basic.lean    | 4 ++--
 Mathlib/Topology/Algebra/Module/Basic.lean                    | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 6d5c003a4fa57..4308e84d667f0 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -987,10 +987,10 @@ open Classical in
 /-- If a subset `A` of the `mixedSpace` is symmetric at real places, then its volume is
 `2^r₁` times the volume of its `plusPart` where `r₁` is the number of real places. -/
 theorem volume_eq_two_pow_mul_volume_plusPart (hm : MeasurableSet A) :
-    volume A = 2 ^ NrRealPlaces K * volume (plusPart A) := by
+    volume A = 2 ^ nrRealPlaces K * volume (plusPart A) := by
   simp_rw [← measure_congr (iUnion_negAtPart_ae A hA), measure_iUnion (disjoint_negAtPlusPart A)
     (fun _ ↦ measurableSet_negAtPlusPart _ A hm), volume_negAtPlusPart _ hm, tsum_fintype,
-    Finset.sum_const, Finset.card_univ, NrRealPlaces, nsmul_eq_mul, Fintype.card_set, Nat.cast_pow,
+    Finset.sum_const, Finset.card_univ, nrRealPlaces, nsmul_eq_mul, Fintype.card_set, Nat.cast_pow,
     Nat.cast_ofNat]
 
 end plusPart
diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
index ec347d662d183..59680b74a36a2 100644
--- a/Mathlib/Topology/Algebra/Module/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis,
   Heather Macbeth
 -/
-import Mathlib.Algebra.Module.Opposites
+import Mathlib.Algebra.Module.Opposite
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.Projection
 import Mathlib.Topology.Algebra.Ring.Basic

From bddd91b1092a59cb17fec26125a35a6829de36cb Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Sat, 26 Oct 2024 09:01:19 +0200
Subject: [PATCH 4/8] remove negAtPlusPlart

---
 .../NumberField/CanonicalEmbedding/Basic.lean | 64 +++++++++----------
 1 file changed, 30 insertions(+), 34 deletions(-)

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 4308e84d667f0..e7cfd61b77e75 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -857,36 +857,31 @@ theorem negAt_preimage :
 positive at all real places. -/
 abbrev plusPart : Set (mixedSpace K) := A ∩ {x | ∀ w, 0 < x.1 w}
 
-variable (s) in
-/-- For `s` a set of real places, `negAtPlusPart A s` is the image of `plusPart A` by `negAt s`. -/
-abbrev negAtPlusPart : Set (mixedSpace K) :=
-    negAt s '' (plusPart A)
-
-theorem negAtPlusPart_neg_of_mem {x : mixedSpace K} (hx : x ∈ negAtPlusPart s A )
+theorem neg_of_mem_negA_plusPart {x : mixedSpace K} (hx : x ∈ negAt s '' (plusPart A))
     {w : {w // IsReal w}} (hw : w ∈ s) :
     x.1 w < 0 := by
   obtain ⟨y, hy, rfl⟩ := hx
   rw [negAt_apply_of_isReal_and_mem _ hw, neg_lt_zero]
   exact hy.2 w
 
-theorem negAtPlusPart_pos_of_not_mem {x : mixedSpace K} (hx : x ∈ negAtPlusPart s A)
+theorem pos_of_not_mem_negAt_plusPart {x : mixedSpace K} (hx : x ∈ negAt s '' (plusPart A))
     {w : {w // IsReal w}} (hw : w ∉ s) :
     0 < x.1 w := by
   obtain ⟨y, hy, rfl⟩ := hx
   rw [negAt_apply_of_isReal_and_not_mem _ hw]
   exact hy.2 w
 
-/-- The sets `negAtPlusPart` are pairwise disjoint. -/
-theorem disjoint_negAtPlusPart : Pairwise (Disjoint on (fun s ↦ negAtPlusPart s A)) := by
+/-- The images of `plusPart` by `negAt` are pairwise disjoint. -/
+theorem disjoint_negAt_plusPart : Pairwise (Disjoint on (fun s ↦ negAt s '' (plusPart A))) := by
   classical
   intro s t hst
   refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_
   obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := by
     exact Set.symmDiff_nonempty.mpr hst
   · exact lt_irrefl _ <|
-      (negAtPlusPart_neg_of_mem A hx hw.1).trans (negAtPlusPart_pos_of_not_mem A hx' hw.2)
+      (neg_of_mem_negA_plusPart A hx hw.1).trans (pos_of_not_mem_negAt_plusPart A hx' hw.2)
   · exact lt_irrefl _ <|
-      (negAtPlusPart_neg_of_mem A hx' hw.1).trans (negAtPlusPart_pos_of_not_mem A hx hw.2)
+      (neg_of_mem_negA_plusPart A hx' hw.1).trans (pos_of_not_mem_negAt_plusPart A hx hw.2)
 
 /-- For `x : mixedSpace K`, the set `signSet x` is the set of real places `w` s.t. `x w ≤ 0`. -/
 def signSet (x : mixedSpace K) : Set {w : InfinitePlace K // IsReal w} := {w | x.1 w ≤ 0}
@@ -907,10 +902,10 @@ variable (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A)
 
 open Classical in
 include hA in
-theorem mem_negAtPlusPart_of_mem {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ : ∀ w, x.1 w ≠ 0) :
-    x ∈ negAtPlusPart s A ↔ (∀ w, w ∈ s → x.1 w < 0) ∧ (∀ w, w ∉ s → x.1 w > 0) := by
-  refine ⟨fun hx ↦ ⟨fun _ hw ↦ negAtPlusPart_neg_of_mem A hx hw,
-      fun _ hw ↦ negAtPlusPart_pos_of_not_mem A hx hw⟩,
+theorem mem_negAt_plusPart_of_mem {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ : ∀ w, x.1 w ≠ 0) :
+    x ∈ negAt s '' (plusPart A) ↔ (∀ w, w ∈ s → x.1 w < 0) ∧ (∀ w, w ∉ s → x.1 w > 0) := by
+  refine ⟨fun hx ↦ ⟨fun _ hw ↦ neg_of_mem_negA_plusPart A hx hw,
+      fun _ hw ↦ pos_of_not_mem_negAt_plusPart A hx hw⟩,
       fun ⟨h₁, h₂⟩ ↦ ⟨(fun w ↦ |x.1 w|, x.2), ⟨(hA x).mp hx₁, fun w ↦ abs_pos.mpr (hx₂ w)⟩, ?_⟩⟩
   ext w
   · by_cases hw : w ∈ s
@@ -919,10 +914,11 @@ theorem mem_negAtPlusPart_of_mem {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ : 
   · rfl
 
 include hA in
-/-- Assume that `A`  is symmetric at real places then, the union of all the `negPlusPart`
-and of the set of elements of `A` that are zero at at least one real place is equal to `A`. -/
-theorem iUnion_negAtPlusPart_union :
-    (⋃ s, negAtPlusPart s A) ∪ (A ∩ (⋃ w, {x | x.1 w = 0})) = A := by
+/-- Assume that `A`  is symmetric at real places then, the union of the images of `plusPart`
+by `negAt` and of the set of elements of `A` that are zero at at least one real place
+is equal to `A`. -/
+theorem iUnion_negAt_plusPart_union :
+    (⋃ s, negAt s '' (plusPart A)) ∪ (A ∩ (⋃ w, {x | x.1 w = 0})) = A := by
   ext x
   rw [Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iUnion]
   refine ⟨?_, fun h ↦ ?_⟩
@@ -933,7 +929,7 @@ theorem iUnion_negAtPlusPart_union :
   · obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)
     · exact Or.inr ⟨h, hx⟩
     · refine Or.inl ⟨signSet x,
-        (mem_negAtPlusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
+        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
       · exact lt_of_le_of_ne hw (hx w)
       · exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))
 
@@ -954,9 +950,9 @@ theorem volume_eq_zero (w : {w // IsReal w}) :
 
 include hA in
 open Classical in
-theorem iUnion_negAtPart_ae :
-    ⋃ s, negAtPlusPart s A =ᵐ[volume] A := by
-  nth_rewrite 2 [← iUnion_negAtPlusPart_union A hA]
+theorem iUnion_negAt_plusPart_ae :
+    ⋃ s, negAt s '' (plusPart A) =ᵐ[volume] A := by
+  nth_rewrite 2 [← iUnion_negAt_plusPart_union A hA]
   refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm
   exact measure_mono_null Set.inter_subset_right
     (measure_iUnion_null_iff.mpr fun _ ↦ volume_eq_zero _)
@@ -970,28 +966,28 @@ theorem measurableSet_plusPart (hm : MeasurableSet A) :
     exact measurableSet_lt measurable_const ((measurable_pi_apply _).comp' measurable_fst)
 
 variable (s) in
-theorem measurableSet_negAtPlusPart (hm : MeasurableSet A) :
-    MeasurableSet (negAtPlusPart s A) := by
-  rw [negAtPlusPart, ← negAt_preimage]
+theorem measurableSet_negAt_plusPart (hm : MeasurableSet A) :
+    MeasurableSet (negAt s '' (plusPart A)) := by
+  rw [← negAt_preimage]
   exact (measurableSet_plusPart hm).preimage (negAt s).continuous.measurable
 
 open Classical in
 /-- The image of the `plusPart` of `A` by `negAt` have all the same volume as `plusPart A`. -/
-theorem volume_negAtPlusPart (hm : MeasurableSet A) :
-    volume (negAtPlusPart s A) = volume (plusPart A) := by
-  rw [negAtPlusPart, ← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
+theorem volume_negAt_plusPart (hm : MeasurableSet A) :
+    volume (negAt s '' (plusPart A)) = volume (plusPart A) := by
+  rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
     (volume_preserving_negAt s).measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]
 
 include hA in
 open Classical in
 /-- If a subset `A` of the `mixedSpace` is symmetric at real places, then its volume is
-`2^r₁` times the volume of its `plusPart` where `r₁` is the number of real places. -/
+`2^ nrRealPlaces K` times the volume of its `plusPart`. -/
 theorem volume_eq_two_pow_mul_volume_plusPart (hm : MeasurableSet A) :
     volume A = 2 ^ nrRealPlaces K * volume (plusPart A) := by
-  simp_rw [← measure_congr (iUnion_negAtPart_ae A hA), measure_iUnion (disjoint_negAtPlusPart A)
-    (fun _ ↦ measurableSet_negAtPlusPart _ A hm), volume_negAtPlusPart _ hm, tsum_fintype,
-    Finset.sum_const, Finset.card_univ, nrRealPlaces, nsmul_eq_mul, Fintype.card_set, Nat.cast_pow,
-    Nat.cast_ofNat]
+  simp_rw [← measure_congr (iUnion_negAt_plusPart_ae A hA), measure_iUnion
+    (disjoint_negAt_plusPart A) (fun _ ↦ measurableSet_negAt_plusPart _ A hm),
+    volume_negAt_plusPart _ hm, tsum_fintype, Finset.sum_const, Finset.card_univ, nrRealPlaces,
+    nsmul_eq_mul, Fintype.card_set, Nat.cast_pow, Nat.cast_ofNat]
 
 end plusPart
 

From 590a8642bf52d904263653de540dfa431eb5cb58 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Mon, 28 Oct 2024 10:56:47 +0100
Subject: [PATCH 5/8] Review

---
 .../NumberField/CanonicalEmbedding/Basic.lean | 51 ++++++++++---------
 Mathlib/Topology/Algebra/Module/Basic.lean    | 23 ++++-----
 2 files changed, 39 insertions(+), 35 deletions(-)

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index e7cfd61b77e75..677af9427ae27 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -197,9 +197,11 @@ open Classical in
 instance : NoAtoms (volume : Measure (mixedSpace K)) := by
   obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
   by_cases hw : IsReal w
-  · exact @prod.instNoAtoms_fst _ _ _ _ volume volume _ (pi_noAtoms ⟨w, hw⟩)
-  · exact @prod.instNoAtoms_snd _ _ _ _ volume volume _
-      (pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩)
+  · have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsReal w} → ℝ)) := pi_noAtoms ⟨w, hw⟩
+    exact prod.instNoAtoms_fst
+  · have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsComplex w} → ℂ)) :=
+      pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩
+    exact prod.instNoAtoms_snd
 
 end Measure
 
@@ -769,6 +771,8 @@ end integerLattice
 
 noncomputable section plusPart
 
+open ContinuousLinearEquiv
+
 variable {K} (s : Set {w : InfinitePlace K // IsReal w})
 
 open Classical in
@@ -776,8 +780,8 @@ open Classical in
 changes sign at places in `s` and leaves the rest unchanged. -/
 def negAt :
     (mixedSpace K) ≃L[ℝ] (mixedSpace K) :=
-  (ContinuousLinearEquiv.piCongrRight
-    fun w ↦ if w ∈ s then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prod
+  (piCongrRight
+    fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prod
       (ContinuousLinearEquiv.refl ℝ _)
 
 variable {s}
@@ -785,14 +789,13 @@ variable {s}
 @[simp]
 theorem negAt_apply_of_isReal_and_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∈ s) :
     (negAt s x).1 w = - x.1 w := by
-  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
-    if_pos hw, ContinuousLinearEquiv.neg_apply]
+  simp only [negAt, ContinuousLinearEquiv.prod_apply, refl_apply, piCongrRight_apply, if_pos hw,
+    neg_apply]
 
 @[simp]
 theorem negAt_apply_of_isReal_and_not_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∉ s) :
     (negAt s x).1 w = x.1 w := by
-  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
-    if_neg hw, ContinuousLinearEquiv.refl_apply]
+  simp only [negAt, ContinuousLinearEquiv.prod_apply, refl_apply, piCongrRight_apply, if_neg hw]
 
 @[simp]
 theorem negAt_apply_of_isComplex (x : mixedSpace K) (w : {w // IsComplex w}) :
@@ -813,9 +816,9 @@ theorem volume_preserving_negAt [NumberField K] (s : Set {w : InfinitePlace K //
     MeasurePreserving (negAt s) := by
   refine MeasurePreserving.prod (volume_preserving_pi fun w ↦ ?_) (MeasurePreserving.id _)
   by_cases hw : w ∈ s
-  · simp_rw [if_pos hw]
+  · simp only [if_pos hw]
     exact Measure.measurePreserving_neg _
-  · simp_rw [if_neg hw]
+  · simp only [if_neg hw]
     exact MeasurePreserving.id _
 
 /-- `negAt` preserves `normAtPlace`. -/
@@ -823,8 +826,8 @@ theorem volume_preserving_negAt [NumberField K] (s : Set {w : InfinitePlace K //
 theorem normAtPlace_negAt (s : Set {w // IsReal w}) (x : mixedSpace K) (w : InfinitePlace K) :
     normAtPlace w (negAt s x) = normAtPlace w x := by
   obtain hw | hw := isReal_or_isComplex w
-  · simp_rw [normAtPlace_apply_isReal hw, Real.norm_eq_abs, negAt_apply_abs_of_isReal]
-  · simp_rw [normAtPlace_apply_isComplex hw, negAt_apply_of_isComplex]
+  · simp only [normAtPlace_apply_isReal hw, Real.norm_eq_abs, negAt_apply_abs_of_isReal]
+  · simp only [normAtPlace_apply_isComplex hw, negAt_apply_of_isComplex, Complex.norm_eq_abs]
 
 /-- `negAt` preserves the `norm`. -/
 @[simp]
@@ -832,16 +835,18 @@ theorem norm_negAt [NumberField K] (s : Set {w // IsReal w}) (x : mixedSpace K)
     mixedEmbedding.norm (negAt s x) = mixedEmbedding.norm x :=
   norm_eq_of_normAtPlace_eq (fun w ↦ normAtPlace_negAt _ _ w)
 
+
 open ContinuousLinearEquiv in
 /-- `negAt` is equal to its inverse. -/
+@[simp]
 theorem negAt_symm (s : Set {w : InfinitePlace K // IsReal w}) :
     (negAt s).symm = negAt s := by
   ext x w
   · by_cases hw : w ∈ s
-    · simp_rw [negAt_apply_of_isReal_and_mem _ hw, negAt, prod_symm,
-        ContinuousLinearEquiv.prod_apply, piCongrRight_symm_apply, if_pos hw, symm_neg, neg_apply]
-    · simp_rw [negAt_apply_of_isReal_and_not_mem _ hw, negAt, prod_symm,
-        ContinuousLinearEquiv.prod_apply, piCongrRight_symm_apply, if_neg hw, refl_symm, refl_apply]
+    · simp only [negAt, prod_symm, refl_symm, ContinuousLinearEquiv.prod_apply, refl_apply,
+        piCongrRight_symm_apply, if_pos hw, symm_neg, neg_apply, piCongrRight_apply]
+    · simp only [negAt, prod_symm, refl_symm, ContinuousLinearEquiv.prod_apply, refl_apply,
+        piCongrRight_symm_apply, if_neg hw, piCongrRight_apply]
   · rfl
 
 variable (A : Set (mixedSpace K))
@@ -909,8 +914,8 @@ theorem mem_negAt_plusPart_of_mem {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ :
       fun ⟨h₁, h₂⟩ ↦ ⟨(fun w ↦ |x.1 w|, x.2), ⟨(hA x).mp hx₁, fun w ↦ abs_pos.mpr (hx₂ w)⟩, ?_⟩⟩
   ext w
   · by_cases hw : w ∈ s
-    · simp_rw [negAt_apply_of_isReal_and_mem _ hw, abs_of_neg (h₁ w hw), neg_neg]
-    · simp_rw [negAt_apply_of_isReal_and_not_mem _ hw, abs_of_pos (h₂ w hw)]
+    · simp only [negAt_apply_of_isReal_and_mem _ hw, abs_of_neg (h₁ w hw), neg_neg]
+    · simp only [negAt_apply_of_isReal_and_not_mem _ hw, abs_of_pos (h₂ w hw)]
   · rfl
 
 include hA in
@@ -984,10 +989,10 @@ open Classical in
 `2^ nrRealPlaces K` times the volume of its `plusPart`. -/
 theorem volume_eq_two_pow_mul_volume_plusPart (hm : MeasurableSet A) :
     volume A = 2 ^ nrRealPlaces K * volume (plusPart A) := by
-  simp_rw [← measure_congr (iUnion_negAt_plusPart_ae A hA), measure_iUnion
-    (disjoint_negAt_plusPart A) (fun _ ↦ measurableSet_negAt_plusPart _ A hm),
-    volume_negAt_plusPart _ hm, tsum_fintype, Finset.sum_const, Finset.card_univ, nrRealPlaces,
-    nsmul_eq_mul, Fintype.card_set, Nat.cast_pow, Nat.cast_ofNat]
+  simp only [← measure_congr (iUnion_negAt_plusPart_ae A hA),
+    measure_iUnion (disjoint_negAt_plusPart A) (fun _ ↦ measurableSet_negAt_plusPart _ A hm),
+    volume_negAt_plusPart _ hm, tsum_fintype, sum_const, card_univ, Fintype.card_set, nsmul_eq_mul,
+    Nat.cast_pow, Nat.cast_ofNat, nrRealPlaces]
 
 end plusPart
 
diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
index 2c49846744a4f..76ec2db962eb5 100644
--- a/Mathlib/Topology/Algebra/Module/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -2013,12 +2013,15 @@ def arrowCongrEquiv (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[
     ContinuousLinearMap.ext fun x => by
       simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]
 
+section piCongrRight
+
+variable {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)] [∀ i, AddCommMonoid (M i)]
+  [∀ i, Module R₁ (M i)] {N : ι → Type*} [∀ i, TopologicalSpace (N i)] [∀ i, AddCommMonoid (N i)]
+  [∀ i, Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i)
+
 /-- Combine a family of continuous linear equivalences into a continuous linear equivalence of
 pi-types. -/
-def piCongrRight {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)]
-    [∀ i, AddCommMonoid (M i)] [∀ i, Module R₁ (M i)] {N : ι → Type*} [∀ i, TopologicalSpace (N i)]
-    [∀ i, AddCommMonoid (N i)] [∀ i, Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i) :
-    ((i : ι) → M i) ≃L[R₁] (i : ι) → N i :=
+def piCongrRight : ((i : ι) → M i) ≃L[R₁] (i : ι) → N i :=
   { LinearEquiv.piCongrRight fun i ↦ f i with
     continuous_toFun := by
       exact continuous_pi fun i ↦ (f i).continuous_toFun.comp (continuous_apply i)
@@ -2026,19 +2029,15 @@ def piCongrRight {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)]
       exact continuous_pi fun i => (f i).continuous_invFun.comp (continuous_apply i) }
 
 @[simp]
-theorem piCongrRight_apply {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)]
-    [∀ i, AddCommMonoid (M i)] [∀ i, Module R₁ (M i)] {N : ι → Type*} [∀ i, TopologicalSpace (N i)]
-    [∀ i, AddCommMonoid (N i)] [∀ i, Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i)
-    (m : (i : ι) → M i) (i : ι) :
+theorem piCongrRight_apply (m : (i : ι) → M i) (i : ι) :
     piCongrRight f m i = (f i) (m i) := rfl
 
 @[simp]
-theorem piCongrRight_symm_apply {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)]
-    [∀ i, AddCommMonoid (M i)] [∀ i, Module R₁ (M i)] {N : ι → Type*} [∀ i, TopologicalSpace (N i)]
-    [∀ i, AddCommMonoid (N i)] [∀ i, Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i)
-    (n : (i : ι) → N i) (i : ι) :
+theorem piCongrRight_symm_apply (n : (i : ι) → N i) (i : ι) :
     (piCongrRight f).symm n i = (f i).symm (n i) := rfl
 
+end piCongrRight
+
 end AddCommMonoid
 
 section AddCommGroup

From 69aabc22483ed1f7c3ce80cae592dcf32dce7688 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Mon, 28 Oct 2024 18:31:06 +0100
Subject: [PATCH 6/8] Clean after merge

---
 Mathlib/Topology/Algebra/Module/Basic.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
index 3d1e4f56c020d..d2a18b9da1c14 100644
--- a/Mathlib/Topology/Algebra/Module/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -1745,10 +1745,6 @@ theorem refl_apply (x : M₁) :
 
 end
 
-@[simp]
-theorem refl_apply (x : M₁) :
-    ContinuousLinearEquiv.refl R₁ M₁ x = x := rfl
-
 @[simp, norm_cast]
 theorem coe_refl : ↑(ContinuousLinearEquiv.refl R₁ M₁) = ContinuousLinearMap.id R₁ M₁ :=
   rfl

From 8682a78d7f6ab75f4e248eb84899acffc8a0407b Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Mon, 28 Oct 2024 18:36:09 +0100
Subject: [PATCH 7/8] Typo

---
 Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 673e8d71b62a1..9100a0ecf6df6 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -811,7 +811,7 @@ variable {K} (s : Set {w : InfinitePlace K // IsReal w})
 
 open Classical in
 /-- Let `s` be a set of real places, define the continuous linear equiv of the mixed space that
-changes sign at places in `s` and leaves the rest unchanged. -/
+swaps sign at places in `s` and leaves the rest unchanged. -/
 def negAt :
     (mixedSpace K) ≃L[ℝ] (mixedSpace K) :=
   (piCongrRight fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prod

From 6e3bb1f310057e7f1ec54a5c2811f599ad6d2203 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Mon, 28 Oct 2024 18:37:44 +0100
Subject: [PATCH 8/8] More clean up

---
 .../NumberField/CanonicalEmbedding/Basic.lean | 46 +++++--------------
 1 file changed, 12 insertions(+), 34 deletions(-)

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 9100a0ecf6df6..9c27b582cb5d9 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -183,40 +183,6 @@ open NumberField.InfinitePlace Module Finset
 abbrev mixedSpace :=
   ({w : InfinitePlace K // IsReal w} → ℝ) × ({w : InfinitePlace K // IsComplex w} → ℂ)
 
-section Measure
-
-open MeasureTheory.Measure MeasureTheory
-
-variable [NumberField K]
-
-open Classical in
-instance : IsAddHaarMeasure (volume : Measure (mixedSpace K)) :=
-  prod.instIsAddHaarMeasure volume volume
-
-open Classical in
-instance : NoAtoms (volume : Measure (mixedSpace K)) := by
-  obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
-  by_cases hw : IsReal w
-  · have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsReal w} → ℝ)) := pi_noAtoms ⟨w, hw⟩
-    exact prod.instNoAtoms_fst
-  · have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsComplex w} → ℂ)) :=
-      pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩
-    exact prod.instNoAtoms_snd
-
-variable {K} in
-open Classical in
-/-- The set of points in the mixedSpace that are equal to `0` at a fixed (real) place has
-volume zero. -/
-theorem volume_eq_zero (w : {w // IsReal w}) :
-    volume ({x : mixedSpace K | x.1 w = 0}) = 0 := by
-  let A : AffineSubspace ℝ (mixedSpace K) :=
-    Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x.1 w = 0}, by aesop⟩, rfl⟩ (by aesop))
-  convert Measure.addHaar_affineSubspace volume A fun h ↦ ?_
-  have : 1 ∈ A := h ▸ Set.mem_univ _
-  simp [A] at this
-
-end Measure
-
 /-- The mixed embedding of a number field `K` into the mixed space of `K`. -/
 noncomputable def _root_.NumberField.mixedEmbedding : K →+* (mixedSpace K) :=
   RingHom.prod (Pi.ringHom fun w => embedding_of_isReal w.prop)
@@ -271,6 +237,18 @@ instance : NoAtoms (volume : Measure (mixedSpace K)) := by
       pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩
     exact prod.instNoAtoms_snd
 
+variable {K} in
+open Classical in
+/-- The set of points in the mixedSpace that are equal to `0` at a fixed (real) place has
+volume zero. -/
+theorem volume_eq_zero (w : {w // IsReal w}) :
+    volume ({x : mixedSpace K | x.1 w = 0}) = 0 := by
+  let A : AffineSubspace ℝ (mixedSpace K) :=
+    Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x.1 w = 0}, by aesop⟩, rfl⟩ (by aesop))
+  convert Measure.addHaar_affineSubspace volume A fun h ↦ ?_
+  have : 1 ∈ A := h ▸ Set.mem_univ _
+  simp [A] at this
+
 end Measure
 
 section commMap