[Merged by Bors] - feat: remove the diamond for Complex.measureSpace

Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean

@@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
-import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
-import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
 
 #align_import measure_theory.measure.lebesgue.complex from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
 
 /-!
 # Lebesgue measure on `ℂ`
 
-In this file we define Lebesgue measure on `ℂ`. Since `ℂ` is defined as a `structure` as the
-push-forward of the volume on `ℝ²` under the natural isomorphism. There are (at least) two
-frequently used ways to represent `ℝ²` in `mathlib`: `ℝ × ℝ` and `Fin 2 → ℝ`. We define measurable
-equivalences (`MeasurableEquiv`) to both types and prove that both of them are volume preserving
-(in the sense of `MeasureTheory.measurePreserving`).
+In this file, we consider the Lebesgue measure on `ℂ` defined as the push-forward of the volume
+on `ℝ²` under the natural isomorphism and prove that it is equal to the measure `volume` of `ℂ`
+coming from its `InnerProductSpace` structure over `ℝ`. For that, we consider the two frequently
+used ways to represent `ℝ²` in `mathlib`: `ℝ × ℝ` and `Fin 2 → ℝ`, define measurable equivalences
+(`MeasurableEquiv`) to both types and prove that both of them are volume preserving (in the sense
+of `MeasureTheory.measurePreserving`).
 -/
 
 
@@ -26,11 +26,6 @@ noncomputable section
 
 namespace Complex
 
-/-- Lebesgue measure on `ℂ`. -/
-instance measureSpace : MeasureSpace ℂ :=
-  ⟨Measure.map basisOneI.equivFun.symm volume⟩
-#align complex.measure_space Complex.measureSpace
-
 /-- Measurable equivalence between `ℂ` and `ℝ² = Fin 2 → ℝ`. -/
 def measurableEquivPi : ℂ ≃ᵐ (Fin 2 → ℝ) :=
   basisOneI.equivFun.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv
@@ -41,8 +36,13 @@ def measurableEquivRealProd : ℂ ≃ᵐ ℝ × ℝ :=
   equivRealProdClm.toHomeomorph.toMeasurableEquiv
 #align complex.measurable_equiv_real_prod Complex.measurableEquivRealProd
 
-theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi :=
-  (measurableEquivPi.symm.measurable.measurePreserving _).symm _
+theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi := by
+  convert (measurableEquivPi.symm.measurable.measurePreserving volume).symm
+  rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar,
+    measurableEquivPi, Homeomorph.toMeasurableEquiv_symm_coe,
+    ContinuousLinearEquiv.symm_toHomeomorph, ContinuousLinearEquiv.coe_toHomeomorph,
+    Basis.map_addHaar, eq_comm]
+  exact (Basis.addHaar_eq_iff _ _).mpr Complex.orthonormalBasisOneI.volume_parallelepiped
 #align complex.volume_preserving_equiv_pi Complex.volume_preserving_equiv_pi
 
 theorem volume_preserving_equiv_real_prod : MeasurePreserving measurableEquivRealProd :=