awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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 : ι) → ℂ))
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))
⊢ 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)

Tactic:
rw [← MeasurePreserving.integral_comp this e.measurableEmbedding f]

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integral_comp
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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 _ _ _ _ (MeasurableSpace.pi (X := fun (i : ι) ↦ ℝ × ℝ)) (volume : Measure ((i : ι) → ℝ × ℝ))
      fun (x : (i : ι) → ℝ × ℝ) ↦ f fun (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x i))

Tactic:
integral_comp_pi_polarCoord_symm (f ∘ e)

Premises used: Function.comp, OpenPartialHomeomorph.toFun', Pi.map, DFunLike.coe, integral_comp_pi_polarCoord_symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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 _ _ _ _ (MeasurableSpace.pi (X := fun (i : ι) ↦ ℝ × ℝ)) (volume : Measure ((i : ι) → ℝ × ℝ))
      fun (x : (i : ι) → ℝ × ℝ) ↦ f fun (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x i))

Tactic:
exact integral_comp_pi_polarCoord_symm (f ∘ e)

Premises used: Function.comp, DFunLike.coe, integral_comp_pi_polarCoord_symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
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
⊢ (∫⁻ (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

Tactic:
rw [← setLIntegral_univ f, ← setLIntegral_congr pi_polarCoord_symm_target_ae_eq_univ]

Premises used: pi_polarCoord_symm_target_ae_eq_univ, MeasureTheory.setLIntegral_congr, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (x : ι → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
      ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ∫⁻ (x : ι → ℝ × ℝ) in
      (fun (p : (i : ι) → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)) ''
        Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target,
      f x

Tactic:
(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

Premises used: MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, MeasureTheory.MeasureSpace.volume, injOn_pi_polarCoord_symm, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
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)
⊢ (∫⁻ (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:
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

Premises used: MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, MeasureTheory.MeasureSpace.volume, injOn_pi_polarCoord_symm, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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)

Tactic:
setLIntegral_congr_fun measurableSet_pi_polarCoord_target (fun x hx ↦ ?_)

Premises used: measurableSet_pi_polarCoord_target, MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
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)
⊢ (∫⁻ (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:
refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target (fun x hx ↦ ?_)

Premises used: measurableSet_pi_polarCoord_target, MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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
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)
h₁ :
  ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    ENNReal.ofReal (∏ x_1 : ι, |(x x_1).1|) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
h₂ :
  ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    (∏ i : ι, ENNReal.ofReal |(x i).1|) * f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
⊢ ((∏ 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:
simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
    abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]

Premises used: abs_fst_of_mem_pi_polarCoord_target, ENNReal.ofReal_prod_of_nonneg, det_fderivPiPolarCoordSymm, abs_nonneg, Finset.abs_prod
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : ((a : ι) → ℝ × ℝ) ≃ᵐ ((a : ι) → ℂ) :=
  MeasurableEquiv.piCongrRight (π := fun (x : ι) ↦ ℝ × ℝ) (π' := fun (x : ι) ↦ ℂ) fun (x : ι) ↦
    measurableEquivRealProd.symm
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
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 : ι) → ℂ))
rw :
  (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)) =
    ∫⁻ (a : (i : ι) → ℝ × ℝ),
      f fun (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i) ∂(volume : Measure ((i : ι) → ℝ × ℝ))
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Tactic:
rw [← MeasurePreserving.lintegral_comp_emb this e.measurableEmbedding]

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.lintegral_comp_emb
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
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 : ι) → ℂ))
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)) =
    ∫⁻ (a : (i : ι) → ℝ × ℝ),
      f fun (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i) ∂(volume : Measure ((i : ι) → ℝ × ℝ))

Tactic:
lintegral_comp_pi_polarCoord_symm (f ∘ e)

Premises used: lintegral_comp_pi_polarCoord_symm, Function.comp, OpenPartialHomeomorph.toFun', Pi.map, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
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 : ι) → ℂ))
⊢ (∫⁻ (p : (i : ι) → ℝ × ℝ) in Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) (p i)) =
    ∫⁻ (a : (i : ι) → ℝ × ℝ),
      f fun (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i) ∂(volume : Measure ((i : ι) → ℝ × ℝ))

Tactic:
exact lintegral_comp_pi_polarCoord_symm (f ∘ e)

Premises used: lintegral_comp_pi_polarCoord_symm, Function.comp, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.PolynomialExp
Goal:
n : ℕ
c : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x ((monomial n : (a : ℝ) → ℝ[X]) c) / rexp x) atTop (𝓝 0)

Tactic:
simpa [exp_neg, div_eq_mul_inv, mul_assoc]
    using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_zero n)

Premises used: tendsto_const_nhds, mul_assoc, div_eq_mul_inv, Filter.Tendsto.mul, Real.exp_neg, Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.PolynomialExp
Goal:
p q : ℝ[X]
hp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x p / rexp x) atTop (𝓝 0)
hq : Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x q / rexp x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x (p + q) / rexp x) atTop (𝓝 0)

Tactic:
simpa [add_div] using hp.add hq

Premises used: Filter.Tendsto.add, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.PolynomialExp
Goal:
p : ℝ[X]
monomial :
  ∀ (n : ℕ) (c : ℝ),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x ((Polynomial.monomial n : (a : ℝ) → ℝ[X]) c) / rexp x) atTop (𝓝 0)
add :
  ∀ (p q : ℝ[X]) (hp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x p / rexp x) atTop (𝓝 0))
    (hq : Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x q / rexp x) atTop (𝓝 0)),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x (p + q) / rexp x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ eval x p / rexp x) atTop (𝓝 0)

Tactic:
induction p using Polynomial.induction_on' with
  | monomial n c => simpa [exp_neg, div_eq_mul_inv, mul_assoc]
    using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_zero n)
  | add p q hp hq => simpa [add_div] using hp.add hq

Premises used: mul_assoc, Polynomial.monomial, div_eq_mul_inv, Real.exp_neg, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
rw : ∀ (i : ℝ), 0 ≤ i → ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici i
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ y) atTop atTop

Tactic:
rw [(atTop_basis' 0).tendsto_right_iff]

Premises used: Filter.atTop_basis', Filter.HasBasis.tendsto_right_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
h : ∀ (x : ℝ) (hx₀ : 0 ≤ x) (hx : b ^ (1 / y) ≤ x), x ^ y ∈ Set.Ici b
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici b

Tactic:
filter_upwards [eventually_ge_atTop 0, eventually_ge_atTop (b ^ (1 / y))] with x hx₀ hx

Premises used: HDiv.hDiv, HPow.hPow, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
x : ℝ
hx₀ : 0 ≤ x
hx : b ^ (1 / y) ≤ x
⊢ x ^ y ∈ Set.Ici b

Tactic:
simpa (disch := positivity) [Real.rpow_inv_le_iff_of_pos] using hx

Premises used: Real.rpow_inv_le_iff_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hr : y < 0
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x⁻¹ ^ (-y)) (𝓝[>] 0) atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ y) (𝓝[>] 0) atTop

Tactic:
simp_rw +singlePass [← neg_neg y, Real.rpow_neg_eq_inv_rpow]

Premises used: neg_neg, Real.rpow_neg_eq_inv_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hr : y < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x⁻¹ ^ (-y)) (𝓝[>] 0) atTop

Tactic:
(tendsto_rpow_atTop <| neg_pos.mpr hr).comp tendsto_inv_nhdsGT_zero

Premises used: Iff.mpr, neg_pos, tendsto_rpow_atTop, tendsto_inv_nhdsGT_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hr : y < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x⁻¹ ^ (-y)) (𝓝[>] 0) atTop

Tactic:
exact (tendsto_rpow_atTop <| neg_pos.mpr hr).comp tendsto_inv_nhdsGT_zero

Premises used: Iff.mpr, neg_pos, tendsto_rpow_atTop, tendsto_inv_nhdsGT_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (-y)) atTop (𝓝 0)

Tactic:
Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop 0) fun _ hx => (rpow_neg (le_of_lt hx) y).symm)
    (tendsto_rpow_atTop hy).inv_tendsto_atTop

Premises used: Filter.eventuallyEq_of_mem, tendsto_rpow_atTop, le_of_lt, Filter.Ioi_mem_atTop, Filter.Tendsto.inv_tendsto_atTop, Filter.Tendsto.congr', OfNat.ofNat, Eq.symm, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
rcases : ∀ (hb : b < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
rcases₁ :
  ∀ (hb₀ : LT.lt (α := ℝ) (-1) 0) (hb₁ : LT.lt (α := ℝ) 0 1),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (𝓝 0)
rcases₂ : ∀ (hb : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)

Tactic:
rcases lt_trichotomy b 0 with hb | rfl | hb

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]

Premises used: ite_false, LT.lt.le, Real.rpow_def_of_nonpos, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
rw :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) fun (_x : ℝ) ↦ HMul.hMul (α := ℝ) 1 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) atTop (𝓝 0)

Tactic:
rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]

Premises used: Asymptotics.isLittleO_const_iff, one_ne_zero, OfNat.ofNat, Eq.symm, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) fun (_x : ℝ) ↦ HMul.hMul (α := ℝ) 1 1

Tactic:
IsLittleO.mul_isBigO ?exp ?cos

Premises used: Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x)) fun (_x : ℝ) ↦ 1
refine₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cos (x * π)) fun (_x : ℝ) ↦ 1
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x) * cos (x * π)) fun (_x : ℝ) ↦ HMul.hMul (α := ℝ) 1 1

Tactic:
refine IsLittleO.mul_isBigO ?exp ?cos

Premises used: Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x)) fun (_x : ℝ) ↦ 1

Tactic:
rw [isLittleO_const_iff one_ne_zero]

Premises used: Asymptotics.isLittleO_const_iff, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)

Tactic:
tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Real.exp, Real.tendsto_exp_atBot, Filter.tendsto_const_mul_atBot_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
refine : log b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Real.tendsto_exp_atBot, Filter.tendsto_const_mul_atBot_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
linarith : -b ≤ 0 → b - 0 + (-b - 0) = 0
⊢ 0 < -b

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
rw : -b < 1
⊢ log b < 0

Tactic:
rw [← log_neg_eq_log, log_neg_iff (by linarith)]

Premises used: Real.log_neg_eq_log, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
linarith : 1 ≤ -b → -1 - b + (1 - -b) = 0
⊢ -b < 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (log b * x)) fun (_x : ℝ) ↦ 1

Tactic:
case exp =>
      rw [isLittleO_const_iff one_ne_zero]
      refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
      rw [← log_neg_eq_log, log_neg_iff (by linarith)]
      linarith

Premises used: Iff.mpr, Asymptotics.isLittleO_const_iff, Real.log_neg_eq_log, Filter.tendsto_id, Real.exp, Real.tendsto_exp_atBot, Filter.tendsto_const_mul_atBot_of_neg, Filter.Tendsto.comp, one_ne_zero, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
rw : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * Norm.norm (E := ℝ) 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cos (x * π)) fun (_x : ℝ) ↦ 1

Tactic:
rw [isBigO_iff]

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
x : ℝ
⊢ ‖cos (x * π)‖ ≤ 1 * Norm.norm (E := ℝ) 1

Tactic:
simp [Real.abs_cos_le_one]

Premises used: Real.abs_cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * Norm.norm (E := ℝ) 1

Tactic:
exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩