[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
      (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈ Ioi 0 ×ˢ Ioo (-π) π
[PROOFSTEP]
rintro ⟨x, y⟩ hxy
[GOAL]
case mk
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y) ∈ Ioi 0 ×ˢ Ioo (-π) π
[PROOFSTEP]
simp only [prod_mk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg, true_and_iff,
  Complex.arg_lt_pi_iff]
[GOAL]
case mk
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2 ∧ (0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0)
[PROOFSTEP]
constructor
[GOAL]
case mk.left
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
cases' hxy with hxy hxy
[GOAL]
case mk.left.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst}
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
dsimp at hxy 
[GOAL]
case mk.left.inl
x y : ℝ
hxy : 0 < x
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
linarith [sq_pos_of_ne_zero _ hxy.ne', sq_nonneg y]
[GOAL]
case mk.left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.snd ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
linarith [sq_nonneg x, sq_pos_of_ne_zero _ hxy]
[GOAL]
case mk.right
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ 0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0
[PROOFSTEP]
cases' hxy with hxy hxy
[GOAL]
case mk.right.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst}
⊢ 0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0
[PROOFSTEP]
exact Or.inl (le_of_lt hxy)
[GOAL]
case mk.right.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.snd ≠ 0}
⊢ 0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0
[PROOFSTEP]
exact Or.inr hxy
[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ Ioi 0 ×ˢ Ioo (-π) π → (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
rintro ⟨r, θ⟩ ⟨hr, hθ⟩
[GOAL]
case mk.intro
r θ : ℝ
hr : (r, θ).fst ∈ Ioi 0
hθ : (r, θ).snd ∈ Ioo (-π) π
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
dsimp at hr hθ 
[GOAL]
case mk.intro
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
rcases eq_or_ne θ 0 with (rfl | h'θ)
[GOAL]
case mk.intro.inl
r : ℝ
hr : r ∈ Ioi 0
hθ : 0 ∈ Ioo (-π) π
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, 0) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
simpa using hr
[GOAL]
case mk.intro.inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
right
[GOAL]
case mk.intro.inr.h
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | q.snd ≠ 0}
[PROOFSTEP]
simp at hr 
[GOAL]
case mk.intro.inr.h
r θ : ℝ
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
hr : 0 < r
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | q.snd ≠ 0}
[PROOFSTEP]
simpa only [ne_of_gt hr, Ne.def, mem_setOf_eq, mul_eq_zero, false_or_iff, sin_eq_zero_iff_of_lt_of_lt hθ.1 hθ.2] using
  h'θ
[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
      (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
          ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
        x
[PROOFSTEP]
rintro ⟨x, y⟩ _
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
have A : sqrt (x ^ 2 + y ^ 2) = Complex.abs (x + y * Complex.I) := by
  simp [Complex.abs_def, Complex.normSq, pow_two, MonoidWithZeroHom.coe_mk, Complex.add_re, Complex.ofReal_re,
    Complex.mul_re, Complex.I_re, mul_zero, Complex.ofReal_im, Complex.I_im, sub_self, add_zero, Complex.add_im,
    Complex.mul_im, mul_one, zero_add]
[GOAL]
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
[PROOFSTEP]
simp [Complex.abs_def, Complex.normSq, pow_two, MonoidWithZeroHom.coe_mk, Complex.add_re, Complex.ofReal_re,
  Complex.mul_re, Complex.I_re, mul_zero, Complex.ofReal_im, Complex.I_im, sub_self, add_zero, Complex.add_im,
  Complex.mul_im, mul_one, zero_add]
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
A : sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
have Z := Complex.abs_mul_cos_add_sin_mul_I (x + y * Complex.I)
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
A : sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
Z :
  ↑(↑Complex.abs (↑x + ↑y * Complex.I)) *
      (Complex.cos ↑(Complex.arg (↑x + ↑y * Complex.I)) +
        Complex.sin ↑(Complex.arg (↑x + ↑y * Complex.I)) * Complex.I) =
    ↑x + ↑y * Complex.I
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
simp only [← Complex.ofReal_cos, ← Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc] at Z 
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
A : sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
Z :
  ↑(↑Complex.abs (↑x + ↑y * Complex.I) * cos (Complex.arg (↑x + ↑y * Complex.I))) +
      ↑(↑Complex.abs (↑x + ↑y * Complex.I) * sin (Complex.arg (↑x + ↑y * Complex.I))) * Complex.I =
    ↑x + ↑y * Complex.I
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
simpa [A, -Complex.ofReal_cos, -Complex.ofReal_sin] using Complex.ext_iff.1 Z
[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ Ioi 0 ×ˢ Ioo (-π) π →
      (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
          ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
        x
[PROOFSTEP]
rintro ⟨r, θ⟩ ⟨hr, hθ⟩
[GOAL]
case mk.intro
r θ : ℝ
hr : (r, θ).fst ∈ Ioi 0
hθ : (r, θ).snd ∈ Ioo (-π) π
⊢ (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
      ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ)) =
    (r, θ)
[PROOFSTEP]
dsimp at hr hθ 
[GOAL]
case mk.intro
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
      ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ)) =
    (r, θ)
[PROOFSTEP]
simp only [Prod.mk.inj_iff]
[GOAL]
case mk.intro
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ sqrt ((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r ∧ Complex.arg (↑Complex.equivRealProd.symm (r * cos θ, r * sin θ)) = θ
[PROOFSTEP]
constructor
[GOAL]
case mk.intro.left
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ sqrt ((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r
[PROOFSTEP]
conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| r
[PROOFSTEP]
rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| r
[PROOFSTEP]
rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| r
[PROOFSTEP]
rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
case mk.intro.left
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ sqrt ((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = sqrt ((sin θ ^ 2 + cos θ ^ 2) * r ^ 2)
[PROOFSTEP]
congr 1
[GOAL]
case mk.intro.left.e_x
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (r * cos θ) ^ 2 + (r * sin θ) ^ 2 = (sin θ ^ 2 + cos θ ^ 2) * r ^ 2
[PROOFSTEP]
ring
[GOAL]
case mk.intro.right
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ Complex.arg (↑Complex.equivRealProd.symm (r * cos θ, r * sin θ)) = θ
[PROOFSTEP]
convert Complex.arg_mul_cos_add_sin_mul_I hr ⟨hθ.1, hθ.2.le⟩
[GOAL]
case h.e'_2.h.e'_1
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ ↑Complex.equivRealProd.symm (r * cos θ, r * sin θ) = ↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)
[PROOFSTEP]
simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos, Complex.ofReal_sin]
[GOAL]
case h.e'_2.h.e'_1
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ ↑r * Complex.cos ↑θ + ↑r * Complex.sin ↑θ * Complex.I = ↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)
[PROOFSTEP]
ring
[GOAL]
⊢ ContinuousOn
    ↑{ toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
apply ((continuous_fst.pow 2).add (continuous_snd.pow 2)).sqrt.continuousOn.prod
[GOAL]
⊢ ContinuousOn (fun x => Complex.arg (↑Complex.equivRealProd.symm x))
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
have A : MapsTo Complex.equivRealProd.symm ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0} :=
  by rintro ⟨x, y⟩ hxy; simpa only using hxy
[GOAL]
⊢ MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
[PROOFSTEP]
rintro ⟨x, y⟩ hxy
[GOAL]
case mk
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ ↑Complex.equivRealProd.symm (x, y) ∈ {z | 0 < z.re ∨ z.im ≠ 0}
[PROOFSTEP]
simpa only using hxy
[GOAL]
A : MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
⊢ ContinuousOn (fun x => Complex.arg (↑Complex.equivRealProd.symm x))
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
refine' ContinuousOn.comp (f := Complex.equivRealProd.symm) (g := Complex.arg) (fun z hz => _) _ A
[GOAL]
case refine'_1
A : MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
z : ℂ
hz : z ∈ {z | 0 < z.re ∨ z.im ≠ 0}
⊢ ContinuousWithinAt Complex.arg {z | 0 < z.re ∨ z.im ≠ 0} z
[PROOFSTEP]
exact (Complex.continuousAt_arg hz).continuousWithinAt
[GOAL]
case refine'_2
A : MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
⊢ ContinuousOn ↑Complex.equivRealProd.symm
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
exact Complex.equivRealProdClm.symm.continuous.continuousOn
[GOAL]
p : ℝ × ℝ
⊢ HasFDerivAt (↑(LocalHomeomorph.symm polarCoord))
    (↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]])))
    p
[PROOFSTEP]
rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]
[GOAL]
p : ℝ × ℝ
⊢ HasFDerivAt (↑(LocalHomeomorph.symm polarCoord))
    (ContinuousLinearMap.prod
      (cos p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.fst * sin p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ)
      (sin p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.fst * cos p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
[PROOFSTEP]
convert
  HasFDerivAt.prod (𝕜 := ℝ) (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
[GOAL]
case h.e'_10.h.e'_15.h.h.h
p : ℝ × ℝ
e_4✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = AddCommGroup.toAddCommMonoid
e_8✝ : NonUnitalNonAssocSemiring.toAddCommMonoid = AddCommGroup.toAddCommMonoid
he✝¹ : Prod.instModule = NormedSpace.toModule
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ cos p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.fst * sin p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.fst • -sin p.snd • ContinuousLinearMap.snd ℝ ℝ ℝ + (cos ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
simp [smul_smul, add_comm, neg_mul, neg_smul, smul_neg]
[GOAL]
case h.e'_10.h.e'_16.h.h.h
p : ℝ × ℝ
e_4✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = AddCommGroup.toAddCommMonoid
e_11✝ : NonUnitalNonAssocSemiring.toAddCommMonoid = AddCommGroup.toAddCommMonoid
he✝¹ : Prod.instModule = NormedSpace.toModule
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ sin p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.fst * cos p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.fst • cos p.snd • ContinuousLinearMap.snd ℝ ℝ ℝ + (sin ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
simp [smul_smul, add_comm, neg_mul, neg_smul, smul_neg]
[GOAL]
⊢ polarCoord.source =ᵐ[volume] univ
[PROOFSTEP]
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
[GOAL]
⊢ polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
[PROOFSTEP]
intro x hx
[GOAL]
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
[PROOFSTEP]
simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt, Classical.not_not] at hx 
[GOAL]
x : ℝ × ℝ
hx : x.fst ≤ 0 ∧ x.snd = 0
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
[PROOFSTEP]
exact hx.2
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ polarCoord.source =ᵐ[volume] univ
[PROOFSTEP]
have B : volume (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) : Set (ℝ × ℝ)) = 0 :=
  by
  apply Measure.addHaar_submodule
  rw [Ne.def, LinearMap.ker_eq_top]
  intro h
  have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
  simp at this 
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
[PROOFSTEP]
apply Measure.addHaar_submodule
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) ≠ ⊤
[PROOFSTEP]
rw [Ne.def, LinearMap.ker_eq_top]
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ¬LinearMap.snd ℝ ℝ ℝ = 0
[PROOFSTEP]
intro h
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ False
[PROOFSTEP]
have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ ↑(LinearMap.snd ℝ ℝ ℝ) (0, 1) = ↑0 (0, 1)
[PROOFSTEP]
rw [h]
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
this : ↑(LinearMap.snd ℝ ℝ ℝ) (0, 1) = ↑0 (0, 1)
⊢ False
[PROOFSTEP]
simp at this 
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ polarCoord.source =ᵐ[volume] univ
[PROOFSTEP]
simp only [ae_eq_univ]
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ ↑↑volume polarCoord.sourceᶜ = 0
[PROOFSTEP]
exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
set B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ := fun p =>
  LinearMap.toContinuousLinearMap
    (Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
have A : ∀ p ∈ polarCoord.symm.source, HasFDerivAt polarCoord.symm (B p) p := fun p _ => hasFDerivAt_polarCoord_symm p
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
have B_det : ∀ p, (B p).det = p.1 := by
  intro p
  conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
  simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin, Matrix.det_fin_two_of, sub_neg_eq_add]
  ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
⊢ ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
[PROOFSTEP]
intro p
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
⊢ ContinuousLinearMap.det (B p) = p.fst
[PROOFSTEP]
conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
| p.fst
[PROOFSTEP]
rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
| p.fst
[PROOFSTEP]
rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
| p.fst
[PROOFSTEP]
rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
⊢ ContinuousLinearMap.det (B p) = (cos p.snd ^ 2 + sin p.snd ^ 2) * p.fst
[PROOFSTEP]
simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin, Matrix.det_fin_two_of, sub_neg_eq_add]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
⊢ cos p.snd * (p.fst * cos p.snd) + p.fst * sin p.snd * sin p.snd = (cos p.snd ^ 2 + sin p.snd ^ 2) * p.fst
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p)
[PROOFSTEP]
calc
  ∫ p, f p = ∫ p in polarCoord.source, f p := by
    rw [← integral_univ]
    apply set_integral_congr_set_ae
    exact polarCoord_source_ae_eq_univ.symm
  _ = ∫ p in polarCoord.target, abs (B p).det • f (polarCoord.symm p) := by
    apply integral_target_eq_integral_abs_det_fderiv_smul volume A
  _ = ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) :=
    by
    apply set_integral_congr polarCoord.open_target.measurableSet fun x hx => ?_
    rw [B_det, abs_of_pos]
    exact hx.1
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.source, f p
[PROOFSTEP]
rw [← integral_univ]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (x : ℝ × ℝ) in univ, f x = ∫ (p : ℝ × ℝ) in polarCoord.source, f p
[PROOFSTEP]
apply set_integral_congr_set_ae
[GOAL]
case hst
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ univ =ᵐ[volume] polarCoord.source
[PROOFSTEP]
exact polarCoord_source_ae_eq_univ.symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ) in polarCoord.source, f p =
    ∫ (p : ℝ × ℝ) in polarCoord.target, |ContinuousLinearMap.det (B p)| • f (↑(LocalHomeomorph.symm polarCoord) p)
[PROOFSTEP]
apply integral_target_eq_integral_abs_det_fderiv_smul volume A
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, |ContinuousLinearMap.det (B p)| • f (↑(LocalHomeomorph.symm polarCoord) p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p)
[PROOFSTEP]
apply set_integral_congr polarCoord.open_target.measurableSet fun x hx => ?_
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ |ContinuousLinearMap.det (B x)| • f (↑(LocalHomeomorph.symm polarCoord) x) =
    x.fst • f (↑(LocalHomeomorph.symm polarCoord) x)
[PROOFSTEP]
rw [B_det, abs_of_pos]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ 0 < x.fst
[PROOFSTEP]
exact hx.1
