awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have refine : ∀ (x : ℝ × ℝ) (hx : x ∈ polarCoord.target),
  ENNReal.ofReal |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
    ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
Tactic: refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ ENNReal.ofReal |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
    ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
have rw : ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
  ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
Tactic: rw [abs_of_pos hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ), f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have _ : ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
Tactic: calc
    _ = ∫⁻ p in polarCoord.symm '' polarCoord.target, f p := by
      rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (polarCoord.symm p) := by
      rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
      · simp_rw [det_fderivPolarCoordSymm]; rfl
      exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) := by
      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
      rw [abs_of_pos hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
_ : ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
⊢ ∫⁻ (p : ℝ × ℝ), f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have _₁ : ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p =
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
Tactic: calc
    _ = ∫⁻ p in polarCoord.symm '' polarCoord.target, f p := by
      rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (polarCoord.symm p) := by
      rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
      · simp_rw [det_fderivPolarCoordSymm]; rfl
      exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) := by
      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
      rw [abs_of_pos hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
_ : ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
_₁ :
  ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
⊢ ∫⁻ (p : ℝ × ℝ), f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have _₂ : ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p) =
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
Tactic: calc
    _ = ∫⁻ p in polarCoord.symm '' polarCoord.target, f p := by
      rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (polarCoord.symm p) := by
      rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
      · simp_rw [det_fderivPolarCoordSymm]; rfl
      exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) := by
      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
      rw [abs_of_pos hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
a : ℂ
⊢ (↑Complex.polarCoord : ℂ → ℝ × ℝ) a = (‖a‖, a.arg)
have simp_rw : (↑Complex.polarCoord : ℂ → ℝ × ℝ) a = (√(HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.im 2), a.arg)
Tactic: simp_rw [Complex.norm_def, Complex.normSq_apply, ← pow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ Eq.{u_1 + 1} (α := E)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p))
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.volume fun (p : ℂ) ↦
      f p)
have rw : Eq.{u_1 + 1} (α := E)
  (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
    (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p))
  (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
    (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    p.1 • f ((measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)))
Tactic: rw [← (Complex.volume_preserving_equiv_real_prod.symm).integral_comp
    measurableEquivRealProd.symm.measurableEmbedding, ← integral_comp_polarCoord_symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p) =
    ∫⁻ (p : ℂ), f p
have rw : ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p) =
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target,
    ENNReal.ofReal p.1 • f ((measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
Tactic: rw [← (volume_preserving_equiv_real_prod.symm).lintegral_comp_emb
    measurableEquivRealProd.symm.measurableEmbedding, ← lintegral_comp_polarCoord_symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Finite ι
p : ι → ℝ × ℝ
⊢ HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) (fderivPiPolarCoordSymm p) p
have have : ∀ (this : Fintype ι),
  HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) (fderivPiPolarCoordSymm p) p
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) (fderivPiPolarCoordSymm p) p
have rw : ∀ (i : ι),
  HasFDerivAt (fun (x : ι → ℝ × ℝ) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
    (fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj (φ := fun (a : ι) ↦ ℝ × ℝ) i) p
Tactic: rw [fderivPiPolarCoordSymm, hasFDerivAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ι → ℝ × ℝ
⊢ (fderivPiPolarCoordSymm p).det = ∏ i : ι, (p i).1
have simp_rw : Eq (α := ℝ)
  (ContinuousLinearMap.det.{0, u_1} (M := ι → ℝ × ℝ)
    (ContinuousLinearMap.pi (φ := fun (a : ι) ↦ ℝ × ℝ) fun (i : ι) ↦
      fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj (φ := fun (a : ι) ↦ ℝ × ℝ) i))
  (∏ i : ι, (p i).1)
Tactic: simp_rw [fderivPiPolarCoordSymm, ContinuousLinearMap.det_pi, det_fderivPolarCoordSymm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ι → ℝ × ℝ
simp_rw :
  Eq (α := ℝ)
    (ContinuousLinearMap.det.{0, u_1} (M := ι → ℝ × ℝ)
      (ContinuousLinearMap.pi (φ := fun (a : ι) ↦ ℝ × ℝ) fun (i : ι) ↦
        fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj (φ := fun (a : ι) ↦ ℝ × ℝ) i))
    (∏ i : ι, (p i).1)
⊢ (fderivPiPolarCoordSymm p).det = ∏ i : ι, (p i).1
have simp_rw₁ : Eq (α := ℝ) (∏ i : ι, (fderivPolarCoordSymm (p i)).det) (∏ i : ι, (p i).1)
Tactic: simp_rw [fderivPiPolarCoordSymm, ContinuousLinearMap.det_pi, det_fderivPolarCoordSymm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Set.image (α := (i : ι) → ℝ × ℝ)
      (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦
        polarCoord.target) =ᶠ[ae (F := Measure ((i : ι) → ℝ × ℝ)) volume]
    Set.univ
have rw : (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦
    polarCoord.source) =ᶠ[ae (F := Measure ((i : ι) → ℝ × ℝ))
    (Measure.pi (α := fun (i : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ volume)]
  Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦ Set.univ
Tactic: rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
rw :
  (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦
      polarCoord.source) =ᶠ[ae (F := Measure ((i : ι) → ℝ × ℝ))
      (Measure.pi (α := fun (i : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ volume)]
    Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦ Set.univ
⊢ Set.image (α := (i : ι) → ℝ × ℝ)
      (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦
        polarCoord.target) =ᶠ[ae (F := Measure ((i : ι) → ℝ × ℝ)) volume]
    Set.univ
have rw₁ : Set ι
Tactic: rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ι → ℝ × ℝ) ↦ f p)
have rw : Eq.{u_2 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
    fun (p : (i : ι) → ℝ × ℝ) ↦
    HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume
      (Set.image (α := (i : ι) → ℝ × ℝ)
        (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
        (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target)))
    fun (x : (i : ι) → ℝ × ℝ) ↦ f x)
Tactic: rw [← setIntegral_univ (f := f), ← setIntegral_congr_set pi_polarCoord_symm_target_ae_eq_univ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume
        (Set.image (α := (i : ι) → ℝ × ℝ)
          (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦
            (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
          (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target)))
      fun (x : (i : ι) → ℝ × ℝ) ↦ f x)
have h : Eq.{u_2 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
    fun (p : (i : ι) → ℝ × ℝ) ↦
    HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target)) fun (x : ι → ℝ × ℝ) ↦
    |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
Tactic: convert!
    (integral_image_eq_integral_abs_det_fderiv_smul volume measurableSet_pi_polarCoord_target
        (fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt) injOn_pi_polarCoord_symm
        f).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (x : ι → ℝ × ℝ) ↦ |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
have h : ∀ (x : (i : ι) → ℝ × ℝ)
  (hx :
    Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
      (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x),
  HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
Tactic: refine setIntegral_congr_fun measurableSet_pi_polarCoord_target fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : (i : ι) → ℝ × ℝ
hx :
  Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x
⊢ HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
have h : HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
  HSMul.hSMul (α := ℝ) |∏ i : ι, (x i).1| (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
Tactic: simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, abs_fst_of_mem_pi_polarCoord_target hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : (i : ι) → ℝ × ℝ
hx :
  Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x
h :
  HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    HSMul.hSMul (α := ℝ) |∏ i : ι, (x i).1| (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
⊢ HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
have h₁ : HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
  HSMul.hSMul (α := ℝ) (∏ x_1 : ι, |(x x_1).1|) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
Tactic: simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, abs_fst_of_mem_pi_polarCoord_target hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℂ) → E
e : ((a : ι) → ℝ × ℝ) ≃ᵐ ((a : ι) → ℂ) :=
  MeasurableEquiv.piCongrRight (π := fun (x : ι) ↦ ℝ × ℝ) (π' := fun (x : ι) ↦ ℂ) fun (x : ι) ↦
    measurableEquivRealProd.symm
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ι → ℂ) ↦ f p)
have this : MeasurePreserving (β := (i : ι) → ℂ)
  (fun (a : (i : ι) → ℝ × ℝ) (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i))
  (volume : Measure ((i : ι) → ℝ × ℝ)) (volume : Measure ((i : ι) → ℂ))
Tactic: have := volume_preserving_pi (fun _ : ι ↦ Complex.volume_preserving_equiv_real_prod.symm)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℂ) → E
e : ((a : ι) → ℝ × ℝ) ≃ᵐ ((a : ι) → ℂ) :=
  MeasurableEquiv.piCongrRight (π := fun (x : ι) ↦ ℝ × ℝ) (π' := fun (x : ι) ↦ ℂ) fun (x : ι) ↦
    measurableEquivRealProd.symm
this :
  MeasurePreserving (β := (i : ι) → ℂ)
    (fun (a : (i : ι) → ℝ × ℝ) (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i))
    (volume : Measure ((i : ι) → ℝ × ℝ)) (volume : Measure ((i : ι) → ℂ))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ι → ℂ) ↦ f p)
have rw : Eq.{u_2 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target))
    fun (p : (i : ι) → ℝ × ℝ) ↦
    HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)))
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ι) ↦ ℝ × ℝ)) (volume : Measure ((i : ι) → ℝ × ℝ))
    fun (x : (i : ι) → ℝ × ℝ) ↦ f fun (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x i))
Tactic: rw [← MeasurePreserving.integral_comp this e.measurableEmbedding f]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)) =
    ∫⁻ (p : ι → ℝ × ℝ), f p
have rw : (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
    (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)) =
  ∫⁻ (x : (i : ι) → ℝ × ℝ) in
    Set.image (α := (i : ι) → ℝ × ℝ)
      (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target),
    f x
Tactic: rw [← setLIntegral_univ f, ← setLIntegral_congr pi_polarCoord_symm_target_ae_eq_univ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)) =
    ∫⁻ (x : (i : ι) → ℝ × ℝ) in
      Set.image (α := (i : ι) → ℝ × ℝ)
        (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
        (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target),
      f x
have h : (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
    (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)) =
  ∫⁻ (x : ι → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
Tactic: convert!
    (lintegral_image_eq_lintegral_abs_det_fderiv_mul volume measurableSet_pi_polarCoord_target
        (fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt) injOn_pi_polarCoord_symm
        f).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)) =
    ∫⁻ (x : ι → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
      ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
have h : ∀ (x : (i : ι) → ℝ × ℝ)
  (hx :
    Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
      (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x),
  ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
Tactic: refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : (i : ι) → ℝ × ℝ
hx :
  Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x
⊢ ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
have h : ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
  ENNReal.ofReal |∏ i : ι, (x i).1| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
Tactic: simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
    abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]