awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
          HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-p.1 * sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ)).prod
      (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (sin p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
        HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 * cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ)))
    p
have h : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
    Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
      Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        Eq (α := AddCommMonoid (ℝ × ℝ)) Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid →
          HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
            Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid →
              HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
                HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
                    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-p.1 * sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
                  p.1 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((cos ∘ Prod.snd) p) (ContinuousLinearMap.fst ℝ ℝ ℝ)
Tactic: convert!
    HasFDerivAt.prodMk (𝕜 := ℝ)
      (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
      (hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using
    2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
p : ℝ × ℝ
h :
  Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
      Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
          Eq (α := AddCommMonoid (ℝ × ℝ)) Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid →
            HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
              Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid →
                HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
                  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
                      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-p.1 * sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
                    p.1 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((cos ∘ Prod.snd) p) (ContinuousLinearMap.fst ℝ ℝ ℝ)
⊢ HasFDerivAt (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
          HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-p.1 * sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ)).prod
      (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (sin p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
        HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 * cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ)))
    p
have h₁ : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
    Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
      Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        Eq (α := AddCommMonoid (ℝ × ℝ)) Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid →
          HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
            Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid →
              HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
                HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (sin p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
                    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 * cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
                  p.1 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((sin ∘ Prod.snd) p) (ContinuousLinearMap.fst ℝ ℝ ℝ)
Tactic: convert!
    HasFDerivAt.prodMk (𝕜 := ℝ)
      (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
      (hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using
    2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
p : ℝ × ℝ
| p.1
have rw : (HPow.hPow (β := ℕ) (cos p.2) 2 + HPow.hPow (β := ℕ) (sin p.2) 2) * p.1
Tactic: rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
p : ℝ × ℝ
⊢ (fderivPolarCoordSymm p).det = p.1
have conv_rhs : (fderivPolarCoordSymm p).det = (HPow.hPow (β := ℕ) (cos p.2) 2 + HPow.hPow (β := ℕ) (sin p.2) 2) * p.1
Tactic: conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
p : ℝ × ℝ
⊢ ContinuousLinearMap.det (M := ℝ × ℝ)
      (((LinearMap.toContinuousLinearMap : (ℝ × ℝ →ₗ[ℝ] ℝ × ℝ) ≃ₗ[ℝ] ℝ × ℝ →L[ℝ] ℝ × ℝ) :
          (a : ℝ × ℝ →ₗ[ℝ] ℝ × ℝ) → ℝ × ℝ →L[ℝ] ℝ × ℝ)
        ((Matrix.toLin (Module.Basis.finTwoProd ℝ) (Module.Basis.finTwoProd ℝ) :
            (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ × ℝ →ₗ[ℝ] ℝ × ℝ)
          !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])) =
    (HPow.hPow (β := ℕ) (cos p.2) 2 + HPow.hPow (β := ℕ) (sin p.2) 2) * p.1
have simp : cos p.2 * (p.1 * cos p.2) + p.1 * sin p.2 * sin p.2 =
  (HPow.hPow (β := ℕ) (cos p.2) 2 + HPow.hPow (β := ℕ) (sin p.2) 2) * p.1
Tactic: simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin,
    Matrix.det_fin_two_of, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
have hx₁ : x.1 ≤ 0 ∧ x.2 = 0
Tactic: simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt,
      Classical.not_not] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
⊢ polarCoord.source =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] univ
have A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
Tactic: have A : polarCoord.sourceᶜ ⊆ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) := by
    intro x hx
    simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt,
      Classical.not_not] at hx
    exact hx.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have hs : Ne (α := Submodule ℝ (ℝ × ℝ)) (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) ⊤
Tactic: apply Measure.addHaar_submodule
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
⊢ Ne (α := Submodule ℝ (ℝ × ℝ)) (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) ⊤
have hs : ¬Eq (α := ℝ × ℝ →ₗ[ℝ] ℝ) (LinearMap.snd ℝ ℝ ℝ) 0
Tactic: rw [Ne, LinearMap.ker_eq_top]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
h : Eq (α := ℝ × ℝ →ₗ[ℝ] ℝ) (LinearMap.snd ℝ ℝ ℝ) 0
⊢ Eq (α := ℝ) ((LinearMap.snd ℝ ℝ ℝ : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ)
have rw : Eq (α := ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
h : Eq (α := ℝ × ℝ →ₗ[ℝ] ℝ) (LinearMap.snd ℝ ℝ ℝ) 0
⊢ False
have this : Eq (α := ℝ) ((LinearMap.snd ℝ ℝ ℝ : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ)
Tactic: have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
⊢ polarCoord.source =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] univ
have B : Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ)) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: have B : volume (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) : Set (ℝ × ℝ)) = 0 := by
    apply Measure.addHaar_submodule
    rw [Ne, LinearMap.ker_eq_top]
    intro h
    have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
    simp at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
B :
  Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ polarCoord.source =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] univ
have simp : Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) polarCoord.sourceᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_eq_univ]
-- 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)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
have symm : Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
Tactic: symm
-- 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) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
have rw : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume univ) fun (x : ℝ × ℝ) ↦ f x)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
Tactic: rw [← setIntegral_univ]
-- 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)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume univ) fun (x : ℝ × ℝ) ↦ f x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
have hst : univ =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] polarCoord.source
Tactic: apply setIntegral_congr_set
-- 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)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
have rw : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (x : ℝ × ℝ) ↦
    |(fderivPolarCoordSymm x).det| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
Tactic: rw [← OpenPartialHomeomorph.symm_target,
      integral_target_eq_integral_abs_det_fderiv_smul volume
      (fun p _ ↦ hasFDerivAt_polarCoord_symm p), OpenPartialHomeomorph.symm_source]
-- 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)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
have apply : ∀ (x : ℝ × ℝ) (hx : x ∈ polarCoord.target),
  |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) = x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
Tactic: apply setIntegral_congr_fun polarCoord.open_target.measurableSet fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) = x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
have rw : x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) = x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
Tactic: rw [abs_of_pos hx.1]
-- 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) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
have f₁ : Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
Tactic: calc
    ∫ p, f p = ∫ p in polarCoord.source, f p := by
      rw [← setIntegral_univ]
      apply setIntegral_congr_set
      exact polarCoord_source_ae_eq_univ.symm
    _ = ∫ p in polarCoord.target, |p.1| • f (polarCoord.symm p) := by
      rw [← OpenPartialHomeomorph.symm_target,
      integral_target_eq_integral_abs_det_fderiv_smul volume
      (fun p _ ↦ hasFDerivAt_polarCoord_symm p), OpenPartialHomeomorph.symm_source]
      simp_rw [det_fderivPolarCoordSymm]
    _ = ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) := by
      apply setIntegral_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:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
f₁ :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
have f₂ : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
Tactic: calc
    ∫ p, f p = ∫ p in polarCoord.source, f p := by
      rw [← setIntegral_univ]
      apply setIntegral_congr_set
      exact polarCoord_source_ae_eq_univ.symm
    _ = ∫ p in polarCoord.target, |p.1| • f (polarCoord.symm p) := by
      rw [← OpenPartialHomeomorph.symm_target,
      integral_target_eq_integral_abs_det_fderiv_smul volume
      (fun p _ ↦ hasFDerivAt_polarCoord_symm p), OpenPartialHomeomorph.symm_source]
      simp_rw [det_fderivPolarCoordSymm]
    _ = ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) := by
      apply setIntegral_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:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
f₁ :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
f₂ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.source) fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦ f p)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
have f₃ : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
Tactic: calc
    ∫ p, f p = ∫ p in polarCoord.source, f p := by
      rw [← setIntegral_univ]
      apply setIntegral_congr_set
      exact polarCoord_source_ae_eq_univ.symm
    _ = ∫ p in polarCoord.target, |p.1| • f (polarCoord.symm p) := by
      rw [← OpenPartialHomeomorph.symm_target,
      integral_target_eq_integral_abs_det_fderiv_smul volume
      (fun p _ ↦ hasFDerivAt_polarCoord_symm p), OpenPartialHomeomorph.symm_source]
      simp_rw [det_fderivPolarCoordSymm]
    _ = ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) := by
      apply setIntegral_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 : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p) =
    ∫⁻ (p : ℝ × ℝ), f p
have symm : ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
have rw : ∫⁻ (x : ℝ × ℝ) in univ, f x = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
Tactic: rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
rw : ∫⁻ (x : ℝ × ℝ) in univ, f x = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
⊢ ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
have rw₁ : ∫⁻ (x : ℝ × ℝ) in polarCoord.source, f x =
  ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
Tactic: rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
rw : ∫⁻ (x : ℝ × ℝ) in univ, f x = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
rw₁ :
  ∫⁻ (x : ℝ × ℝ) in polarCoord.source, f x =
    ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
⊢ ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
have rw₂ : ∫⁻ (x : ℝ × ℝ) in polarCoord.source, f x = ∫⁻ (p : ℝ × ℝ) in polarCoord.source, f p
Tactic: rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have rw : ∫⁻ (x : ℝ × ℝ) in polarCoord.target,
    ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
Tactic: rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
rw :
  ∫⁻ (x : ℝ × ℝ) in polarCoord.target,
      ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
⊢ ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have hf : InjOn (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) polarCoord.target
Tactic: rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
rw :
  ∫⁻ (x : ℝ × ℝ) in polarCoord.target,
      ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
hf : InjOn (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) polarCoord.target
⊢ ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have rw₁ : MeasurableSet polarCoord.target
Tactic: rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target,
      ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
have simp_rw : ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |x.1| * f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
Tactic: simp_rw [det_fderivPolarCoordSymm]