awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have 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
Tactic: rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul,
    ← ContinuousLinearMap.det, det_fderivPiPolarCoordSymm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have 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 : ℝ)
Tactic: rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul,
    ← ContinuousLinearMap.det, det_fderivPiPolarCoordSymm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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 : ℝ)
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have rw₅ : (fderivPiPolarCoordSymm x.2).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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have rw₆ : Eq (α := ℝ) (∏ i : { w : InfinitePlace K // w.IsComplex }, (x.2 i).1)
  (∏ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) ''
      PartialEquiv.target
        (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)) =ᶠ[ae (F := Measure (realMixedSpace K)) volume]
    Set.univ
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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 volume fun (x : realMixedSpace K) ↦ f x)
have 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))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
have 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)
Tactic: refine setIntegral_congr_fun (polarCoordReal K).open_target.measurableSet fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ 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)
have 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))
Tactic: simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod, abs_of_mem_polarCoordReal_target K hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
⊢ 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)
have 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))
Tactic: simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod, abs_of_mem_polarCoordReal_target K hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ∫⁻ (x : realMixedSpace K), f x
have rw : ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
    (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
  ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
    ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
Tactic: rw [← setLIntegral_univ f, ← setLIntegral_congr (polarCoordReal_symm_target_ae_eq_univ K),
    lintegral_image_eq_lintegral_abs_det_fderiv_mul volume
      (polarCoordReal K).open_target.measurableSet
      (fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt)
      (polarCoordReal K).symm.injOn f]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
have refine : ∀ (x : realMixedSpace K)
  (hx :
    Membership.mem (γ := Set (realMixedSpace K))
      (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x),
  (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
Tactic: refine setLIntegral_congr_fun (polarCoordReal K).open_target.measurableSet (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx :
  Membership.mem (γ := Set (realMixedSpace K))
    (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x
⊢ (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
have simp_rw : (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
    f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
  ENNReal.ofReal |∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1| *
    f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
Tactic: simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _), abs_of_mem_polarCoordReal_target K hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx :
  Membership.mem (γ := Set (realMixedSpace K))
    (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x
simp_rw :
  (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ENNReal.ofReal |∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1| *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
⊢ (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
have simp_rw₁ : (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
    f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
  ENNReal.ofReal (∏ x_1 : { w : InfinitePlace K // w.IsComplex }, |(x.2 x_1).1|) *
    f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
Tactic: simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _), abs_of_mem_polarCoordReal_target K hx]