awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h_fin :
  LT.lt (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normLeOne K) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
refine lt_top_iff_ne_top.mp <| lt_of_le_of_lt (measure_mono interior_subset) ?_

Premises used: lt_of_le_of_lt, interior_subset, lt_top_iff_ne_top, MeasureTheory.measure_mono, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h_fin :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) < ∞
⊢ LT.lt (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normLeOne K) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [volume_normLeOne]

Premises used: NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) < ∞

Tactic:
Batteries.compareOfLessAndEq_eq_lt.mp rfl

Premises used: Batteries.compareOfLessAndEq_eq_lt, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) < ∞

Tactic:
exact Batteries.compareOfLessAndEq_eq_lt.mp rfl

Premises used: Batteries.compareOfLessAndEq_eq_lt, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ Eq (α := realMixedSpace K)
    ((mixedSpaceToRealMixedSpace K : (a : mixedSpace K) → realMixedSpace K) x : realMixedSpace K)
    ((x.1, fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (Complex.equivRealProd : (a : ℂ) → ℝ × ℝ) (x.2 w)) :
      ({ w : InfinitePlace K // w.IsReal } → ℝ) × ((w : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ))

Tactic:
rfl

Premises used: Prod.map, Pi.map, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurePreserving (α := realMixedSpace K) (β := mixedSpace K)
    (⇑(Homeomorph.symm (mixedSpaceToRealMixedSpace K)) : (a : realMixedSpace K) → mixedSpace K)
    (volume : Measure (realMixedSpace K)) (volume : Measure (mixedSpace K))

Tactic:
(MeasurePreserving.id _).prod <|
    volume_preserving_pi fun _ ↦ Complex.volume_preserving_equiv_real_prod.symm

Premises used: MeasureTheory.volume_preserving_pi, MeasureTheory.MeasurePreserving.prod, MeasureTheory.MeasurePreserving.symm, Complex.measurableEquivRealProd, Prod.map, Complex.volume_preserving_equiv_real_prod, MeasureTheory.MeasurePreserving.id
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsAddHaarMeasure.{u_1} (G := realMixedSpace K) volume

Tactic:
prod.instIsAddHaarMeasure _ _

Premises used: MeasureTheory.Measure.prod.instIsAddHaarMeasure
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable (α := realMixedSpace K)
    (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K)

Tactic:
measurable_fst.prodMk <| Measurable.comp ?_ measurable_snd

Premises used: Measurable.comp, Measurable.prodMk, OpenPartialHomeomorph.toFun', measurable_snd, measurable_fst
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  Measurable.{u_1, u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) (β :=
    { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
    (↑(PartialEquiv.symm
          (OpenPartialHomeomorph.toPartialEquiv
            (OpenPartialHomeomorph.pi (X := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (Y :=
              fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ)
              fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ polarCoord))) :
      ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) → { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
⊢ Measurable (α := realMixedSpace K)
    (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K)

Tactic:
refine measurable_fst.prodMk <| Measurable.comp ?_ measurable_snd

Premises used: Measurable.comp, Measurable.prodMk, measurable_snd, measurable_fst
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable.{u_1, u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) (β :=
    { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
    (↑(PartialEquiv.symm
          (OpenPartialHomeomorph.toPartialEquiv
            (OpenPartialHomeomorph.pi (X := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (Y :=
              fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ)
              fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ polarCoord))) :
      ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) → { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)

Tactic:
measurable_pi_lambda _
    fun _ ↦ continuous_polarCoord_symm.measurable.comp (measurable_pi_apply _)

Premises used: measurable_pi_lambda, Measurable.comp, continuous_polarCoord_symm, measurable_pi_apply, Continuous.measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable.{u_1, u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) (β :=
    { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
    (↑(PartialEquiv.symm
          (OpenPartialHomeomorph.toPartialEquiv
            (OpenPartialHomeomorph.pi (X := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (Y :=
              fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ)
              fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ polarCoord))) :
      ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) → { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)

Tactic:
exact measurable_pi_lambda _
    fun _ ↦ continuous_polarCoord_symm.measurable.comp (measurable_pi_apply _)

Premises used: measurable_pi_lambda, Measurable.comp, continuous_polarCoord_symm, Continuous.measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)) =
    SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
      Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ)) Set.univ
      (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
        fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ polarCoord.source)

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.pi, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
hx :
  Membership.mem (γ := Set (realMixedSpace K))
    (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x
w : { w : InfinitePlace K // w.IsComplex }
⊢ |(x.2 w).1| = (x.2 w).1

Tactic:
abs_of_pos (hx.2 w (Set.mem_univ _)).1

Premises used: And.right, And.left, Set.mem_univ, abs_of_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
⊢ HasFDerivAt (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K)
    (FDerivPolarCoordRealSymm K x) x

Tactic:
(hasFDerivAt_id x.1).prodMap x (hasFDerivAt_pi_polarCoord_symm x.2)

Premises used: ContinuousLinearMap.comp, LinearMap.fst, setOf, hasFDerivAt_id, ContinuousLinearMap.prodMap, OpenPartialHomeomorph.toFun', Prod.fst, NumberField.mixedEmbedding.FDerivPolarCoordRealSymm, hasFDerivAt_pi_polarCoord_symm, ContinuousLinearMap.fst, HasFDerivAt.prodMap, Prod.snd
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
⊢ HasFDerivAt (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K)
    (FDerivPolarCoordRealSymm K x) x

Tactic:
exact (hasFDerivAt_id x.1).prodMap x (hasFDerivAt_pi_polarCoord_symm x.2)

Premises used: hasFDerivAt_id, Prod.fst, hasFDerivAt_pi_polarCoord_symm, HasFDerivAt.prodMap, Prod.snd
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
⊢ HasFDerivAt (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K)
    (FDerivPolarCoordRealSymm K x) x

Tactic:
classical
  exact (hasFDerivAt_id x.1).prodMap x (hasFDerivAt_pi_polarCoord_symm x.2)
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
⊢ (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) =
    LinearMap.prodMap LinearMap.id
      (↑(fderivPiPolarCoordSymm x.2) :
        ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)

Tactic:
have : (FDerivPolarCoordRealSymm K x).toLinearMap =
      LinearMap.prodMap (LinearMap.id) (fderivPiPolarCoordSymm x.2).toLinearMap := rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
this :
  (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) =
    LinearMap.prodMap LinearMap.id
      (↑(fderivPiPolarCoordSymm x.2) :
        ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
rw :
  Eq (α := ℝ)
    ((LinearMap.det : (a : realMixedSpace K →ₗ[ℝ] realMixedSpace K) → ℝ)
        (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) :
      ℝ)
    (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((LinearMap.det : (a : realMixedSpace K →ₗ[ℝ] realMixedSpace K) → ℝ)
        (LinearMap.prodMap LinearMap.id
          (↑(fderivPiPolarCoordSymm x.2) :
            ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) :
      ℝ)
    (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
rw₂ :
  HMul.hMul (α := ℝ) (β := ℝ)
      ((LinearMap.det :
            (a : ({ w : InfinitePlace K // w.IsReal } → ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsReal } → ℝ) → ℝ)
          LinearMap.id :
        ℝ)
      ((LinearMap.det :
            (a :
                ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →
              ℝ)
          (↑(fderivPiPolarCoordSymm x.2) :
            ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) :
        ℝ) =
    ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
rw₃ :
  HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ)
      ((LinearMap.det :
            (a :
                ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →
              ℝ)
          (↑(fderivPiPolarCoordSymm x.2) :
            ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) :
        ℝ) =
    ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
rw₄ :
  Eq (α := ℝ)
    ((LinearMap.det :
          (a : ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →
            ℝ)
        (↑(fderivPiPolarCoordSymm x.2) :
          ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) :
      ℝ)
    (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
rw₅ : (fderivPiPolarCoordSymm x.2).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
rw₆ rw₇ :
  Eq (α := ℝ) (∏ i : { w : InfinitePlace K // w.IsComplex }, (x.2 i).1)
    (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1

Tactic:
rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul,
    ← ContinuousLinearMap.det, det_fderivPiPolarCoordSymm]

Premises used: LinearMap.det_prodMap, ContinuousLinearMap.det, LinearMap.det_id, det_fderivPiPolarCoordSymm, one_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
      Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ)) Set.univ
      (Set.image (α := (i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ)
        (Pi.map (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (β :=
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
        (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          polarCoord.target)) =ᶠ[ae (F := Measure (realMixedSpace K)) (Measure.prod volume volume)]
    SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
      Set ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) Set.univ Set.univ
⊢ (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) ''
      PartialEquiv.target
        (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)) =ᶠ[ae (F := Measure (realMixedSpace K)) volume]
    Set.univ

Tactic:
rw [← Set.univ_prod_univ, volume_eq_prod, (polarCoordReal K).symm_image_target_eq_source,
    polarCoordReal_source, ← polarCoord.symm_image_target_eq_source, ← Set.piMap_image_univ_pi]

Premises used: OpenPartialHomeomorph.symm_image_target_eq_source, NumberField.mixedEmbedding.polarCoordReal, NumberField.mixedEmbedding.polarCoordReal_source, Set.piMap_image_univ_pi, Set.univ_prod_univ, MeasureTheory.Measure.volume_eq_prod, polarCoord
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
      Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ)) Set.univ
      (Set.image (α := (i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ)
        (Pi.map (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (β :=
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
        (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          polarCoord.target)) =ᶠ[ae (F := Measure (realMixedSpace K)) (Measure.prod volume volume)]
    SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
      Set ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) Set.univ Set.univ

Tactic:
set_prod_ae_eq .rfl pi_polarCoord_symm_target_ae_eq_univ

Premises used: MeasureTheory.Measure.set_prod_ae_eq, pi_polarCoord_symm_target_ae_eq_univ, Filter.EventuallyEq.rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
      Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ)) Set.univ
      (Set.image (α := (i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ)
        (Pi.map (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (β :=
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
        (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          polarCoord.target)) =ᶠ[ae (F := Measure (realMixedSpace K)) (Measure.prod volume volume)]
    SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
      Set ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) Set.univ Set.univ

Tactic:
exact set_prod_ae_eq .rfl pi_polarCoord_symm_target_ae_eq_univ

Premises used: MeasureTheory.Measure.set_prod_ae_eq, pi_polarCoord_symm_target_ae_eq_univ, Filter.EventuallyEq.rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : realMixedSpace K → E
rw :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
      fun (x : realMixedSpace K) ↦
      HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
        (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
      fun (x : realMixedSpace K) ↦
      |(FDerivPolarCoordRealSymm K x).det| •
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
      fun (x : realMixedSpace K) ↦
      HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
        (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : realMixedSpace K) ↦ f x)

Tactic:
rw [← setIntegral_univ (f := f),
    ← setIntegral_congr_set (polarCoordReal_symm_target_ae_eq_univ K),
    integral_image_eq_integral_abs_det_fderiv_smul volume
      (polarCoordReal K).open_target.measurableSet
      (fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt)
      (polarCoordReal K).symm.injOn f]

Premises used: MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, NumberField.mixedEmbedding.polarCoordReal, HasFDerivAt.hasFDerivWithinAt, IsOpen.measurableSet, MeasureTheory.MeasureSpace.volume, OpenPartialHomeomorph.injOn, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, MeasureTheory.setIntegral_congr_set, OpenPartialHomeomorph.open_target, MeasureTheory.setIntegral_univ, OpenPartialHomeomorph.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : realMixedSpace K → E
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
      fun (x : realMixedSpace K) ↦
      HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
        (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
      fun (x : realMixedSpace K) ↦
      |(FDerivPolarCoordRealSymm K x).det| •
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))

Tactic:
setIntegral_congr_fun (polarCoordReal K).open_target.measurableSet fun x hx ↦ ?_

Premises used: NumberField.mixedEmbedding.polarCoordReal, IsOpen.measurableSet, MeasureTheory.setIntegral_congr_fun, OpenPartialHomeomorph.open_target
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : realMixedSpace K → E
refine :
  ∀ (x : realMixedSpace K)
    (hx :
      Membership.mem (γ := Set (realMixedSpace K))
        (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x),
    HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
        (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)) =
      |(FDerivPolarCoordRealSymm K x).det| •
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
      fun (x : realMixedSpace K) ↦
      HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
        (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
      fun (x : realMixedSpace K) ↦
      |(FDerivPolarCoordRealSymm K x).det| •
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))

Tactic:
refine setIntegral_congr_fun (polarCoordReal K).open_target.measurableSet fun x hx ↦ ?_

Premises used: NumberField.mixedEmbedding.polarCoordReal, IsOpen.measurableSet, MeasureTheory.setIntegral_congr_fun, OpenPartialHomeomorph.open_target
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : realMixedSpace K → E
x : realMixedSpace K
hx :
  Membership.mem (γ := Set (realMixedSpace K))
    (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x
simp_rw :
  HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
      (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)) =
    HSMul.hSMul (α := ℝ) |∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1|
      (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))
simp_rw₁ :
  HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
      (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)) =
    HSMul.hSMul (α := ℝ) (∏ x_1 : { w : InfinitePlace K // w.IsComplex }, |(x.2 x_1).1|)
      (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))
⊢ HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
      (f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)) =
    |(FDerivPolarCoordRealSymm K x).det| •
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)

Tactic:
simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod, abs_of_mem_polarCoordReal_target K hx]

Premises used: _private.0.NumberField.mixedEmbedding.abs_of_mem_polarCoordReal_target, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, Finset.abs_prod