awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A :
  MapsTo (α := ℝ × ℝ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    Complex.slitPlane
⊢ ContinuousOn (X := ℝ × ℝ) (Y := ℂ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ)
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})

Tactic:
Complex.equivRealProdCLM.symm.continuous.continuousOn

Premises used: ContinuousLinearEquiv.symm, Continuous.continuousOn, Complex.equivRealProdCLM, ContinuousLinearEquiv.continuous
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A :
  MapsTo (α := ℝ × ℝ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    Complex.slitPlane
⊢ ContinuousOn (X := ℝ × ℝ) (Y := ℂ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ)
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})

Tactic:
exact Complex.equivRealProdCLM.symm.continuous.continuousOn

Premises used: ContinuousLinearEquiv.symm, Continuous.continuousOn, Complex.equivRealProdCLM, ContinuousLinearEquiv.continuous
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ ContinuousOn (Y := ℝ × ℝ) (fun (p : ℝ × ℝ) ↦ (p.1 * cos p.2, p.1 * sin p.2))
    (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ × ℝ) ↦ x.1 * cos x.2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ × ℝ) ↦ x.1 * sin x.2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
rw :
  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
⊢ HasFDerivAt (𝕜 := ℝ) (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ)
    (((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]))
    p

Tactic:
rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]

Premises used: Matrix.toLin_finTwoProd_toContinuousLinearMap
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
⊢ HasFDerivAt
    (fun (x : ℝ × ℝ) ↦
      (HMul.hMul (α := ℝ × ℝ → ℝ) (β := ℝ × ℝ → ℝ) Prod.fst (cos ∘ Prod.snd) x,
        HMul.hMul (α := ℝ × ℝ → ℝ) (β := ℝ × ℝ → ℝ) Prod.fst (sin ∘ Prod.snd) x))
    ((p.1 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
          HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((cos ∘ Prod.snd) p) (ContinuousLinearMap.fst ℝ ℝ ℝ)).prod
      (p.1 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
        HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((sin ∘ Prod.snd) p) (ContinuousLinearMap.fst ℝ ℝ ℝ)))
    p

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

Premises used: Real.hasDerivAt_sin, Real.hasDerivAt_cos, HasFDerivAt.mul, HasFDerivAt.prodMk, HasDerivAt.comp_hasFDerivAt, Prod.snd
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_4_1 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_5_1 : Eq (α := AddCommMonoid (ℝ × ℝ)) Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid
e_6_1 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_9 : Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid
e_10 : 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:
simp [smul_smul, add_comm, neg_mul, smul_neg, neg_smul _ (ContinuousLinearMap.snd ℝ ℝ ℝ)]

Premises used: neg_smul, Real, smul_smul, smul_neg, ContinuousLinearMap.snd, add_comm, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_4_1 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_5_1 : Eq (α := AddCommMonoid (ℝ × ℝ)) Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid
e_6_1 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_13 : Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid
e_14 : 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:
simp [smul_smul, add_comm, neg_mul, smul_neg, neg_smul _ (ContinuousLinearMap.snd ℝ ℝ ℝ)]

Premises used: neg_smul, Real, smul_smul, smul_neg, ContinuousLinearMap.snd, add_comm, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
rw : (HPow.hPow (β := ℕ) (cos p.2) 2 + HPow.hPow (β := ℕ) (sin p.2) 2) * p.1
| p.1

Tactic:
rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]

Premises used: Prod.fst, Real.cos_sq_add_sin_sq, Prod.snd, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
conv_rhs : (fderivPolarCoordSymm p).det = (HPow.hPow (β := ℕ) (cos p.2) 2 + HPow.hPow (β := ℕ) (sin p.2) 2) * p.1
⊢ (fderivPolarCoordSymm p).det = p.1

Tactic:
conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]

Premises used: Prod.fst, Real.cos_sq_add_sin_sq, Prod.snd, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
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
⊢ 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

Tactic:
simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin,
    Matrix.det_fin_two_of, sub_neg_eq_add]

Premises used: LinearMap.det_toContinuousLinearMap, Matrix.det_fin_two_of, neg_mul, LinearMap.det_toLin, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
⊢ 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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ Measure.IsAddHaarMeasure (G := ℝ × ℝ) volume

Tactic:
Measure.prod.instIsAddHaarMeasure _ _

Premises used: MeasureTheory.Measure.prod.instIsAddHaarMeasure
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ 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

Premises used: Set.compl_union, Classical.not_not, Set.mem_inter_iff, Set.mem_setOf_eq, not_lt, polarCoord_source, Set.mem_compl_iff
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x : ℝ × ℝ
hx : x.1 ≤ 0 ∧ x.2 = 0
⊢ x ∈ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))

Tactic:
hx.2

Premises used: Set.Mem, setOf, And.right, Set.preimage, Set.singleton
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x : ℝ × ℝ
hx : x.1 ≤ 0 ∧ x.2 = 0
⊢ x ∈ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
hs : Ne (α := Submodule ℝ (ℝ × ℝ)) (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) ⊤
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
apply Measure.addHaar_submodule

Premises used: MeasureTheory.Measure.addHaar_submodule
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
hs : ¬Eq (α := ℝ × ℝ →ₗ[ℝ] ℝ) (LinearMap.snd ℝ ℝ ℝ) 0
⊢ Ne (α := Submodule ℝ (ℝ × ℝ)) (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) ⊤

Tactic:
rw [Ne, LinearMap.ker_eq_top]

Premises used: LinearMap.ker_eq_top, Ne
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
h : Eq (α := ℝ × ℝ →ₗ[ℝ] ℝ) (LinearMap.snd ℝ ℝ ℝ) 0
rw rw₁ : Eq (α := ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ)
⊢ Eq (α := ℝ) ((LinearMap.snd ℝ ℝ ℝ : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
h : Eq (α := ℝ × ℝ →ₗ[ℝ] ℝ) (LinearMap.snd ℝ ℝ ℝ) 0
⊢ Eq (α := ℝ) ((LinearMap.snd ℝ ℝ ℝ : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ)

Tactic:
have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
h : Eq (α := ℝ × ℝ →ₗ[ℝ] ℝ) (LinearMap.snd ℝ ℝ ℝ) 0
this : Eq (α := ℝ) ((LinearMap.snd ℝ ℝ ℝ : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ) ((0 : (a : ℝ × ℝ) → ℝ) (0, 1) : ℝ)
⊢ False

Tactic:
simp at this
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
B :
  Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
simp : Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) polarCoord.sourceᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ polarCoord.source =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] univ

Tactic:
simp only [ae_eq_univ]

Premises used: MeasureTheory.ae_eq_univ
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
B :
  Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) polarCoord.sourceᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le

Premises used: le_antisymm, MeasureTheory.measure_mono, LE.le.trans, le_of_eq, bot_le
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A : polarCoord.sourceᶜ ⊆ (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ))
B :
  Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) (↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) : Set (ℝ × ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) polarCoord.sourceᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le

Premises used: le_antisymm, MeasureTheory.measure_mono, LE.le.trans, le_of_eq, bot_le
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
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))
⊢ 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)

Tactic:
symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
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)
⊢ 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:
rw [← setIntegral_univ]

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
hst : univ =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] polarCoord.source
⊢ 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:
apply setIntegral_congr_set

Premises used: MeasureTheory.setIntegral_congr_set
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ univ =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] polarCoord.source

Tactic:
polarCoord_source_ae_eq_univ.symm

Premises used: polarCoord_source_ae_eq_univ, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ univ =ᶠ[ae (F := Measure (ℝ × ℝ)) volume] polarCoord.source

Tactic:
exact polarCoord_source_ae_eq_univ.symm

Premises used: polarCoord_source_ae_eq_univ, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
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))
⊢ 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:
rw [← OpenPartialHomeomorph.symm_target,
      integral_target_eq_integral_abs_det_fderiv_smul volume
      (fun p _ ↦ hasFDerivAt_polarCoord_symm p), OpenPartialHomeomorph.symm_source]

Premises used: MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul, OpenPartialHomeomorph.symm_target, hasFDerivAt_polarCoord_symm, MeasureTheory.MeasureSpace.volume, OpenPartialHomeomorph.symm_source
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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 (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:
simp_rw [det_fderivPolarCoordSymm]

Premises used: det_fderivPolarCoordSymm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
apply :
  ∀ (x : ℝ × ℝ) (hx : x ∈ polarCoord.target),
    |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) = x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
⊢ 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:
apply setIntegral_congr_fun polarCoord.open_target.measurableSet fun x hx => ?_

Premises used: IsOpen.measurableSet, MeasureTheory.setIntegral_congr_fun, polarCoord, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ × ℝ → E
x : ℝ × ℝ
hx : x ∈ polarCoord.target
rw rw₁ : x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) = x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
⊢ |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) = x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)

Tactic:
rw [abs_of_pos hx.1]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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))
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))
⊢ 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:
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]

Premises used: PartialEquiv.target, polarCoord, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
symm :
  ∫⁻ (p : ℝ × ℝ), f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p) =
    ∫⁻ (p : ℝ × ℝ), f p

Tactic:
symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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
rw₂ rw₃ : ∫⁻ (x : ℝ × ℝ) in polarCoord.source, f x = ∫⁻ (p : ℝ × ℝ) in polarCoord.source, f p
⊢ ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (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]

Premises used: OpenPartialHomeomorph.symm_image_target_eq_source, polarCoord, polarCoord_source_ae_eq_univ, Filter.EventuallyEq.symm, MeasureTheory.setLIntegral_congr, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
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
rw₁ : MeasurableSet polarCoord.target
⊢ ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p =
    ∫⁻ (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)]

Premises used: HasFDerivAt.hasFDerivWithinAt, MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, hasFDerivAt_polarCoord_symm, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
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)
⊢ ∫⁻ (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:
simp_rw [det_fderivPolarCoordSymm]

Premises used: det_fderivPolarCoordSymm