Merge branch 'main' into kill_for_mathlib

FLT/FLT_files.lean

@@ -10,25 +10,28 @@ import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
-import FLT.HIMExperiments.flatness
-import FLT.HaarMeasure.DistribHaarChar
+import FLT.HaarMeasure.DistribHaarChar.Basic
+import FLT.HaarMeasure.DistribHaarChar.Padic
+import FLT.HaarMeasure.DistribHaarChar.RealComplex
+import FLT.HaarMeasure.DistribHaarCharStuff
 import FLT.HaarMeasure.DomMulActMeasure
+import FLT.HaarMeasure.MeasurableSpacePadics
 import FLT.Hard.Results
+import FLT.HIMExperiments.flatness
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
 import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
 import FLT.Mathlib.Algebra.BigOperators.Finprod
+import FLT.Mathlib.Algebra.Group.Subgroup.Defs
+import FLT.Mathlib.Algebra.Group.Subgroup.Pointwise
+import FLT.Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import FLT.Mathlib.Algebra.Module.Equiv.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
+import FLT.Mathlib.Analysis.Complex.Basic
+import FLT.Mathlib.Data.Complex.Basic
 import FLT.Mathlib.Data.ENNReal.Inv
-import FLT.Mathlib.RingTheory.Norm.Defs
-import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
-import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
-import FLT.Mathlib.Topology.Algebra.Monoid
-import FLT.Mathlib.Topology.Constructions
-import FLT.Mathlib.Topology.Homeomorph
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct
@@ -38,7 +41,20 @@ import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
+import FLT.Mathlib.GroupTheory.Complement
+import FLT.Mathlib.GroupTheory.Index
+import FLT.Mathlib.LinearAlgebra.Determinant
+import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.RingTheory.Norm.Defs
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+import FLT.Mathlib.Topology.Algebra.Module.Basic
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
+import FLT.Mathlib.Topology.Algebra.Monoid
+import FLT.Mathlib.Topology.Constructions
+import FLT.Mathlib.Topology.Homeomorph
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.NumberField.IsTotallyReal
+import FLT.RestrictedProduct.Defs
 import FLT.TateCurve.TateCurve

FLT/HaarMeasure/DistribHaarChar.lean → FLT/HaarMeasure/DistribHaarChar/Basic.lean

@@ -66,16 +66,19 @@ lemma addHaarScalarFactor_smul_eq_distribHaarChar_inv (g : G) :
 lemma distribHaarChar_pos : 0 < distribHaarChar A g :=
   pos_iff_ne_zero.mpr ((Group.isUnit g).map (distribHaarChar A)).ne_zero
 
-variable [IsFiniteMeasureOnCompacts μ] [Regular μ] {s : Set A}
+variable [Regular μ] {s : Set A}
 
 variable (μ) in
-omit [IsFiniteMeasureOnCompacts μ] in
 lemma distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ (g • s) := by
   have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [dma_smul_apply]
   rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
     ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
 
-omit [IsFiniteMeasureOnCompacts μ] in
 lemma distribHaarChar_eq_div (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (g : G) :
     distribHaarChar A g = μ (g • s) / μ s := by
-  rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right hs₀ hs]
+  rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right] <;> simp [*]
+
+lemma distribHaarChar_eq_of_measure_smul_eq_mul (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) {r : ℝ≥0}
+    (hμgs : μ (g • s) = r * μ s) : distribHaarChar A g = r := by
+  refine ENNReal.coe_injective ?_
+  rw [distribHaarChar_eq_div hs₀ hs, hμgs, ENNReal.mul_div_cancel_right] <;> simp [*]

FLT/HaarMeasure/DistribHaarChar/Padic.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Javier López-Contreras. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Javier López-Contreras
+-/
+import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.HaarMeasure.DistribHaarChar.Basic
+import FLT.HaarMeasure.MeasurableSpacePadics
+
+/-!
+# The distributive Haar characters of the p-adics
+
+This file computes `distribHaarChar` in the case of the actions of `ℤ_[p]ˣ` on `ℤ_[p]` and of
+`ℚ_[p]ˣ` on `ℚ_[p]`.
+
+This lets us know what `volume (x • s)` is in terms of `‖x‖` and `volume s`, when `x` is a
+p-adic/p-adic integer and `s` is a set of p-adics/p-adic integers.
+
+## Main declarations
+
+* `distribHaarChar_padic`: `distribHaarChar ℚ_[p]` is the usual p-adic norm on `ℚ_[p]ˣ`.
+* `distribHaarChar_padicInt`: `distribHaarChar ℤ_[p]` is constantly `1` on `ℤ_[p]ˣ`.
+* `Padic.volume_padic_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℚ_[p]` and
+  `s : Set ℚ_[p]`.
+* `PadicInt.volume_padicInt_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℤ_[p]` and
+  `s : Set ℤ_[p]`.
+-/
+
+open Padic MeasureTheory Measure Metric Set
+open scoped Pointwise ENNReal NNReal nonZeroDivisors
+
+variable {p : ℕ} [Fact p.Prime]
+
+private lemma distribHaarChar_padic_padicInt (x : ℤ_[p]⁰) :
+    distribHaarChar ℚ_[p] (x : ℚ_[p]ˣ) = ‖(x : ℚ_[p])‖₊ := by
+  -- Let `K` be the copy of `ℤ_[p]` inside `ℚ_[p]` and `H` be `xK`.
+  let K : AddSubgroup ℚ_[p] := (1 : Submodule ℤ_[p] ℚ_[p]).toAddSubgroup
+  let H := (x : ℚ_[p]) • K
+  -- We compute that `volume H = ‖x‖₊ * volume K`.
+  refine distribHaarChar_eq_of_measure_smul_eq_mul (s := K) (μ := volume) (G := ℚ_[p]ˣ)
+    (by simp [K, Padic.submodule_one_eq_closedBall, closedBall, Padic.volume_closedBall_one])
+    (by simp [K, Padic.submodule_one_eq_closedBall, closedBall, Padic.volume_closedBall_one]) ?_
+  change volume (H : Set ℚ_[p]) = ‖(x : ℚ_[p])‖₊ * volume (K : Set ℚ_[p])
+  -- This is true because `H` is a `‖x‖₊⁻¹`-index subgroup of `K`.
+  have hHK : H ≤ K := by
+    simpa [H, K, -Submodule.smul_le_self_of_tower]
+      using (1 : Submodule ℤ_[p] ℚ_[p]).smul_le_self_of_tower (x : ℤ_[p])
+  have : H.FiniteRelIndex K :=
+    PadicInt.smul_submodule_finiteRelIndex (p := p) (mem_nonZeroDivisors_iff_ne_zero.1 x.2) 1
+  have H_relindex_Z : (H.relindex K : ℝ≥0∞) = ‖(x : ℚ_[p])‖₊⁻¹ :=
+    congr(ENNReal.ofNNReal $(PadicInt.smul_submodule_relindex (p := p) x 1))
+  rw [← index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup hHK, H_relindex_Z, ENNReal.coe_inv,
+    ENNReal.mul_inv_cancel_left]
+  · simp
+  · simp
+  · simp
+  · simpa [H, K, Padic.submodule_one_eq_closedBall]
+      using measurableSet_closedBall.const_smul (x : ℚ_[p]ˣ)
+  · simpa [K, Padic.submodule_one_eq_closedBall] using measurableSet_closedBall
+
+/-- The distributive Haar character of the action of `ℚ_[p]ˣ` on `ℚ_[p]` is the usual p-adic norm.
+
+This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℚ_[p]` and `s : Set ℚ_[p]`.
+See `Padic.volume_padic_smul` -/
+@[simp]
+lemma distribHaarChar_padic (x : ℚ_[p]ˣ) : distribHaarChar ℚ_[p] x = ‖(x : ℚ_[p])‖₊ := by
+  -- Write the RHS as the application of a monoid hom `g`.
+  let g : ℚ_[p]ˣ →* ℝ≥0 := {
+    toFun := fun x => ‖(x : ℚ_[p])‖₊
+    map_one' := by simp
+    map_mul' := by simp
+  }
+  revert x
+  suffices distribHaarChar ℚ_[p] = g by simp [this, g]
+  -- By density of `ℤ_[p]⁰` inside `ℚ_[p]ˣ`, it's enough to check that `distribHaarChar ℚ_[p]` and
+  -- `g` agree on `ℤ_[p]⁰`.
+  refine MonoidHom.eq_of_eqOn_dense (PadicInt.closure_nonZeroDivisors_padicInt (p := p)) ?_
+  -- But this is what we proved in `distribHaarChar_padic_padicInt`.
+  simp
+  ext x
+  simp [g]
+  rw [distribHaarChar_padic_padicInt]
+  rfl
+
+@[simp]
+lemma Padic.volume_padic_smul (x : ℚ_[p]) (s : Set ℚ_[p]) : volume (x • s) = ‖x‖₊ * volume s := by
+  obtain rfl | hx := eq_or_ne x 0
+  · simp [(finite_zero.subset s.zero_smul_set_subset).measure_zero]
+  · lift x to ℚ_[p]ˣ using hx.isUnit
+    rw [← distribHaarChar_padic, distribHaarChar_mul, Units.smul_def]
+
+@[simp] lemma Padic.volume_padicInt_smul (x : ℤ_[p]) (s : Set ℚ_[p]) :
+    volume (x • s) = ‖x‖₊ * volume s := by simpa [-volume_padic_smul] using volume_padic_smul x s
+
+@[simp] lemma PadicInt.volume_padicInt_smul (x : ℤ_[p]) (s : Set ℤ_[p]) :
+    volume (x • s) = ‖x‖₊ * volume s := by
+  simpa [-volume_padicInt_smul, ← image_coe_smul_set] using Padic.volume_padicInt_smul x ((↑) '' s)
+
+/-- The distributive Haar character of the action of `ℤ_[p]ˣ` on `ℤ_[p]` is the constant `1`.
+
+This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℤ_[p]` and `s : Set ℤ_[p]`.
+See `PadicInt.volume_padicInt_smul` -/
+@[simp]
+lemma distribHaarChar_padicInt (x : ℤ_[p]ˣ) : distribHaarChar ℤ_[p] x = 1 :=
+  -- We compute `distribHaarChar ℤ_[p]` by lifting everything to `ℚ_[p]`.
+  distribHaarChar_eq_of_measure_smul_eq_mul (s := univ) (μ := volume) (by simp) (measure_ne_top _ _)
+    (by simp [PadicInt.volume_padicInt_smul])

FLT/HaarMeasure/DistribHaarChar/RealComplex.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Javier López-Contreras. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Javier López-Contreras
+-/
+import Mathlib.Analysis.Complex.ReImTopology
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
+import Mathlib.RingTheory.Complex
+import FLT.HaarMeasure.DistribHaarChar.Basic
+import FLT.Mathlib.Analysis.Complex.Basic
+import FLT.Mathlib.Data.Complex.Basic
+import FLT.Mathlib.LinearAlgebra.Determinant
+import FLT.Mathlib.RingTheory.Norm.Defs
+
+/-!
+# The distributive Haar characters of `ℝ` and `ℂ`
+
+This file computes `distribHaarChar` in the case of the actions of `ℝˣ` on `ℝ` and of `ℂˣ` on `ℂ`.
+
+This lets us know what `volume (x • s)` is in terms of `‖x‖` and `volume s`, when `x` is a
+real/complex number and `s` is a set of reals/complex numbers.
+
+## Main declarations
+
+* `distribHaarChar_real`: `distribHaarChar ℝ` is the usual norm on `ℝ`.
+* `distribHaarChar_complex`: `distribHaarChar ℂ` is the usual norm on `ℂ` squared.
+* `Real.volume_real_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℝ` and `s : Set ℝ`.
+* `Complex.volume_complex_smul`: `volume (z • s) = ‖z‖₊ ^ 2 * volume s` for all `z : ℂ` and
+  `s : Set ℂ`.
+-/
+
+open Real Complex MeasureTheory Measure Set
+open scoped Pointwise
+
+lemma Real.volume_real_smul (x : ℝ) (s : Set ℝ) : volume (x • s) = ‖x‖₊ * volume s := by
+  simp [← ennnorm_eq_ofReal_abs]
+
+/-- The distributive Haar character of the action of `ℝˣ` on `ℝ` is the usual norm.
+
+This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℝ` and `s : Set ℝ`.
+See `Real.volume_real_smul`. -/
+lemma distribHaarChar_real (x : ℝˣ) : distribHaarChar ℝ x = ‖(x : ℝ)‖₊ :=
+  -- We compute that `volume (x • [0, 1]) = ‖x‖₊ * volume [0, 1]`.
+  distribHaarChar_eq_of_measure_smul_eq_mul (s := Icc 0 1) (μ := volume)
+    (measure_pos_of_nonempty_interior _ <| by simp).ne' isCompact_Icc.measure_ne_top
+      (Real.volume_real_smul ..)
+
+/-- The distributive Haar character of the action of `ℂˣ` on `ℂ` is the usual norm squared.
+
+This means that `volume (z • s) = ‖z‖ ^ 2 * volume s` for all `z : ℂ` and `s : Set ℂ`.
+See `Complex.volume_complex_smul`. -/
+lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)‖₊ ^ 2 := by
+  -- We compute that `volume (x • ([0, 1] × [0, 1])) = ‖x‖₊ ^ 2 * volume ([0, 1] × [0, 1])`.
+  refine distribHaarChar_eq_of_measure_smul_eq_mul (s := Icc 0 1 ×ℂ Icc 0 1) (μ := volume)
+    (measure_pos_of_nonempty_interior _ <| by simp [interior_reProdIm]).ne'
+    (isCompact_Icc.reProdIm isCompact_Icc).measure_ne_top ?_
+  -- The determinant of left multiplication by `z⁻¹` as a `ℝ`-linear map is `‖z‖₊ ^ (-2)`.
+  have key : ((LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ).det = ‖z.val‖₊ ^ (-2 : ℤ) := by
+    refine Complex.ofReal_injective ?_
+    rw [LinearMap.det_restrictScalars]
+    simp [Algebra.norm_complex_apply, normSq_eq_norm_sq, zpow_ofNat]
+  -- Massaging, we find the result.
+  convert addHaar_preimage_linearMap (E := ℂ) volume
+    (f := (LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ) _ _ using 2
+  · simpa [LinearMap.mul, LinearMap.mk₂, LinearMap.mk₂', LinearMap.mk₂'ₛₗ, Units.smul_def, eq_comm]
+      using preimage_smul_inv z (Icc 0 1 ×ℂ Icc 0 1)
+  · simp [key, ofReal_norm_eq_coe_nnnorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat]
+  · simp [key, zpow_ofNat]
+
+lemma Complex.volume_complex_smul (z : ℂ) (s : Set ℂ) : volume (z • s) = ‖z‖₊ ^ 2 * volume s := by
+  obtain rfl | hz := eq_or_ne z 0
+  · simp [(finite_zero.subset s.zero_smul_set_subset).measure_zero]
+  · lift z to ℂˣ using hz.isUnit
+    rw [← ENNReal.coe_pow, ← distribHaarChar_complex, distribHaarChar_mul, Units.smul_def]

FLT/HaarMeasure/MeasurableSpacePadics.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Yaël Dillies, David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, David Loeffler
+-/
+import Mathlib.MeasureTheory.Measure.Haar.Basic
+import Mathlib.NumberTheory.Padics.ProperSpace
+import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+
+/-!
+# Measurability and measures on the p-adics
+
+This file endows `ℤ_[p]` and `ℚ_[p]` with their Borel sigma-algebra and their Haar measure that
+makes `ℤ_[p]` (or the copy of `ℤ_[p]` inside `ℚ_[p]`) have norm `1`.
+-/
+
+open MeasureTheory Measure TopologicalSpace Topology
+
+variable {p : ℕ} [Fact p.Prime]
+
+namespace Padic
+
+instance instMeasurableSpace : MeasurableSpace ℚ_[p] := borel _
+instance instBorelSpace : BorelSpace ℚ_[p] := ⟨rfl⟩
+
+-- Should we more generally make a map from `CompactOpens` to `PositiveCompacts`?
+private def unitBall_positiveCompact : PositiveCompacts ℚ_[p] where
+  carrier := {y | ‖y‖ ≤ 1}
+  isCompact' := by simpa only [Metric.closedBall, dist_zero_right] using
+    isCompact_closedBall (0 : ℚ_[p]) 1
+  interior_nonempty' := by
+    rw [IsOpen.interior_eq]
+    · exact ⟨0, by simp⟩
+    · simpa only [Metric.closedBall, dist_zero_right] using
+        IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero
+
+noncomputable instance instMeasureSpace : MeasureSpace ℚ_[p] :=
+  ⟨addHaarMeasure unitBall_positiveCompact⟩
+
+instance instIsAddHaarMeasure : IsAddHaarMeasure (volume : Measure ℚ_[p]) :=
+  isAddHaarMeasure_addHaarMeasure _
+
+lemma volume_closedBall_one : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self
+
+end Padic
+
+namespace PadicInt
+
+instance instMeasurableSpace : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace
+instance instBorelSpace : BorelSpace ℤ_[p] := Subtype.borelSpace _
+
+lemma isMeasurableEmbedding_coe : MeasurableEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
+  convert isOpenEmbedding_coe.measurableEmbedding
+  exact inferInstanceAs (BorelSpace ℤ_[p])
+
+noncomputable instance instMeasureSpace : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩
+
+instance instIsAddHaarMeasure : IsAddHaarMeasure (volume : Measure ℤ_[p]) :=
+  isAddHaarMeasure_addHaarMeasure _
+
+@[simp] lemma volume_univ : volume (Set.univ : Set ℤ_[p]) = 1 := addHaarMeasure_self
+
+instance instIsFiniteMeasure : IsFiniteMeasure (volume : Measure ℤ_[p]) where
+  measure_univ_lt_top := by simp
+
+-- https://github.com/ImperialCollegeLondon/FLT/issues/278
+@[simp] lemma volume_coe (s : Set ℤ_[p]) : volume ((↑) '' s : Set ℚ_[p]) = volume s := sorry
+
+end PadicInt

FLT/Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -0,0 +1,6 @@
+import Mathlib.Algebra.Group.Subgroup.Defs
+
+namespace Subgroup
+
+-- TODO: Rename in mathlib
+@[to_additive] alias coe_subtype := coeSubtype

FLT/Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -0,0 +1,12 @@
+import Mathlib.Algebra.Group.Subgroup.Pointwise
+import Mathlib.Algebra.Module.End
+
+open scoped Pointwise
+
+namespace AddSubgroup
+variable {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M]
+
+@[simp] protected lemma smul_zero (s : AddSubgroup M) : (0 : R) • s = ⊥ :=
+  show s.map (Module.toAddMonoidEnd _ _ 0) = ⊥ by simp
+
+end AddSubgroup

FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -0,0 +1,15 @@
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
+
+open scoped nonZeroDivisors
+
+variable {G₀ : Type*} [GroupWithZero G₀]
+
+attribute [simp] mem_nonZeroDivisors_iff_ne_zero
+
+@[simps]
+noncomputable def nonZeroDivisorsEquivUnits : G₀⁰ ≃* G₀ˣ where
+  toFun u := .mk0 _ <| mem_nonZeroDivisors_iff_ne_zero.1 u.2
+  invFun u := ⟨u, u.isUnit.mem_nonZeroDivisors⟩
+  left_inv u := rfl
+  right_inv u := by simp
+  map_mul' u v := by simp

FLT/Mathlib/Analysis/Complex/Basic.lean

@@ -0,0 +1,8 @@
+import Mathlib.Analysis.Complex.Basic
+
+open Complex
+
+variable {s t : Set ℝ}
+
+lemma IsCompact.reProdIm (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ℂ t) :=
+  equivRealProdCLM.toHomeomorph.isCompact_preimage.2 (hs.prod ht)

FLT/Mathlib/Data/Complex/Basic.lean

@@ -0,0 +1,19 @@
+import Mathlib.Data.Complex.Basic
+
+open Set
+
+namespace Complex
+variable {s t : Set ℝ}
+
+open Set
+
+lemma «forall» {p : ℂ → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ := by aesop
+lemma «exists» {p : ℂ → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ := by aesop
+
+@[simp] lemma reProdIm_nonempty : (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
+  simp [Set.Nonempty, reProdIm, Complex.exists]
+
+@[simp] lemma reProdIm_eq_empty : s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
+  simp [← not_nonempty_iff_eq_empty, reProdIm_nonempty, -not_and, not_and_or]
+
+end Complex