awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
f : ℝ → ℝ :=
  (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (a : ℝ) ↦ ℝ)
    (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
h_jensen : f (∑ i ∈ t, HSMul.hSMul (β := ℝ) (w i) (↑(p i) : ℝ)) ≤ ∑ i ∈ t, w i • f (↑(p i) : ℝ)
⊢ Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * (↑((p i).descFactorial n) : ℝ)

Tactic:
simpa only [smul_eq_mul, f, Set.piecewise_eq_of_mem (Set.Ici (n - 1 : ℝ)) _ _ h_avg,
      piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial] using h_jensen

Premises used: Set.Ici, HSub.hSub, Set.piecewise_eq_of_mem, Nat.cast, smul_eq_mul, OfNat.ofNat, _private.0.piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
f : ℝ → ℝ :=
  (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (a : ℝ) ↦ ℝ)
    (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
suffices : f (∑ i ∈ t, HSMul.hSMul (β := ℝ) (w i) (↑(p i) : ℝ)) ≤ ∑ i ∈ t, w i • f (↑(p i) : ℝ)
⊢ Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * (↑((p i).descFactorial n) : ℝ)

Tactic:
suffices h_jensen : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i) by
    simpa only [smul_eq_mul, f, Set.piecewise_eq_of_mem (Set.Ici (n - 1 : ℝ)) _ _ h_avg,
      piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial] using h_jensen
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
f : ℝ → ℝ :=
  (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (a : ℝ) ↦ ℝ)
    (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
⊢ ∀ i ∈ t, Membership.mem (γ := Set ℝ) Set.univ (↑(p i) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
f : ℝ → ℝ :=
  (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (a : ℝ) ↦ ℝ)
    (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
⊢ f (∑ i ∈ t, HSMul.hSMul (β := ℝ) (w i) (↑(p i) : ℝ)) ≤ ∑ i ∈ t, w i • f (↑(p i) : ℝ)

Tactic:
exact ConvexOn.map_sum_le (convexOn_piecewise_Ici_descPochhammer_eval_zero hn) h₀ h₁ (by simp)

Premises used: ConvexOn.map_sum_le, _private.0.convexOn_piecewise_Ici_descPochhammer_eval_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
simp_rw :
  Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) / (↑n.factorial : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ x ∈ t, w x * (↑((p x).descFactorial n) : ℝ)) (↑n.factorial : ℝ)
⊢ Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) / (↑n.factorial : ℝ) ≤
    ∑ i ∈ t, w i * (↑((p i).choose n) : ℝ)

Tactic:
simp_rw [Nat.cast_choose_eq_descPochhammer_div,
    mul_div, ← Finset.sum_div, descPochhammer_eval_eq_descFactorial]

Premises used: mul_div, Nat.cast_choose_eq_descPochhammer_div, Finset.sum_div, descPochhammer_eval_eq_descFactorial
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
⊢ LE.le (α := ℝ) 0 (↑n.factorial : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
apply :
  Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) ≤ ∑ x ∈ t, w x * (↑((p x).descFactorial n) : ℝ)
⊢ Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) / (↑n.factorial : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ x ∈ t, w x * (↑((p x).descFactorial n) : ℝ)) (↑n.factorial : ℝ)

Tactic:
apply div_le_div_of_nonneg_right _ (by positivity)

Premises used: div_le_div_of_nonneg_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
⊢ Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) ≤ ∑ x ∈ t, w x * (↑((p x).descFactorial n) : ℝ)

Tactic:
descPochhammer_eval_le_sum_descFactorial hn p w h₀ h₁ h_avg

Premises used: descPochhammer_eval_le_sum_descFactorial
-- Module: Mathlib.Analysis.SpecialFunctions.Pochhammer
Goal:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq (α := ℝ) (∑ i ∈ t, w i) 1
h_avg : HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≤ ∑ i ∈ t, w i * (↑(p i) : ℝ)
⊢ Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) ≤ ∑ x ∈ t, w x * (↑((p x).descFactorial n) : ℝ)

Tactic:
exact descPochhammer_eval_le_sum_descFactorial hn p w h₀ h₁ h_avg

Premises used: descPochhammer_eval_le_sum_descFactorial
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
simp :
  0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 ∧
    (0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
      Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0)
⊢ (√(HPow.hPow (β := ℕ) (x, y).1 2 + HPow.hPow (β := ℕ) (x, y).2 2),
      Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y))) ∈
    SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π)

Tactic:
simp only [prodMk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg,
      true_and, Complex.arg_lt_pi_iff]

Premises used: Set.mem_Ioo, Set.mem_Ioi, Set.prodMk_mem_set_prod_eq, Complex.neg_pi_lt_arg, Complex.arg_lt_pi_iff, Real.sqrt_pos, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
left : 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
right :
  0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 ∧
    (0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
      Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
left :
  ∀ (hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | 0 < q.1} (x, y)),
    0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
left₁ :
  ∀ (hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} (x, y)),
    0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
rcases hxy with hxy | hxy
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : 0 < x
linarith :
  HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 ≤ 0 →
    HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 - 0 + (0 - HPow.hPow (β := ℕ) x 2) + (0 - HPow.hPow (β := ℕ) y 2) =
      0
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y]

Premises used: LT.lt.ne', sq_nonneg, sq_pos_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} (x, y)
linarith :
  HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 ≤ 0 →
    HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 - 0 + (0 - HPow.hPow (β := ℕ) x 2) +
        (0 - HPow.hPow (β := ℕ) (x, y).2 2) =
      0
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
linarith [sq_nonneg x, sq_pos_of_ne_zero hxy]

Premises used: sq_nonneg, sq_pos_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
right :
  ∀ (hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | 0 < q.1} (x, y)),
    0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
      Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0
right₁ :
  ∀ (hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} (x, y)),
    0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
      Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0
⊢ 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0

Tactic:
rcases hxy with hxy | hxy
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | 0 < q.1} (x, y)
⊢ 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0

Tactic:
Or.inl (le_of_lt hxy)

Premises used: le_of_lt, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | 0 < q.1} (x, y)
⊢ 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0

Tactic:
exact Or.inl (le_of_lt hxy)

Premises used: le_of_lt, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} (x, y)
⊢ 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0

Tactic:
Or.inr hxy

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} (x, y)
⊢ 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0

Tactic:
exact Or.inr hxy

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
inl :
  ∀ (hθ : 0 ∈ Ioo (-π) π),
    Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
      ((r, 0).1 * cos (r, 0).2, (r, 0).1 * sin (r, 0).2)
inr :
  ∀ (h'θ : θ ≠ 0),
    Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
      ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)
⊢ Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)

Tactic:
rcases eq_or_ne θ 0 with (rfl | h'θ)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : 0 ∈ Ioo (-π) π
⊢ Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    ((r, 0).1 * cos (r, 0).2, (r, 0).1 * sin (r, 0).2)

Tactic:
simpa using hr
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
inr : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)
⊢ Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ 0 < r

Tactic:
simp at hr
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
hr : 0 < r
⊢ Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)

Tactic:
simpa only [ne_of_gt hr, Ne, mem_setOf_eq, mul_eq_zero, false_or,
        sin_eq_zero_iff_of_lt_of_lt hθ.1 hθ.2] using h'θ

Premises used: ne_of_gt, Ne, Set.mem_setOf_eq, false_or, mul_eq_zero, And.right, And.left, Real.sin_eq_zero_iff_of_lt_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
h : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
rw :
  √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) =
    √((Complex.normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * Complex.I))
rw₁ rw₂ : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = ‖(↑x : ℂ) + (↑y : ℂ) * Complex.I‖

Tactic:
rw [Complex.norm_def, Complex.normSq_add_mul_I]

Premises used: Complex.norm_def, Complex.normSq_add_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
h : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = ‖(↑x : ℂ) + (↑y : ℂ) * Complex.I‖

Tactic:
have A : √(x ^ 2 + y ^ 2) = ‖x + y * Complex.I‖ := by
      rw [Complex.norm_def, Complex.normSq_add_mul_I]
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
h : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
A : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = ‖(↑x : ℂ) + (↑y : ℂ) * Complex.I‖
⊢ ((√(HPow.hPow (β := ℕ) (x, y).1 2 + HPow.hPow (β := ℕ) (x, y).2 2),
            Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y))).1 *
        cos
          (√(HPow.hPow (β := ℕ) (x, y).1 2 + HPow.hPow (β := ℕ) (x, y).2 2),
              Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y))).2,
      (√(HPow.hPow (β := ℕ) (x, y).1 2 + HPow.hPow (β := ℕ) (x, y).2 2),
            Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y))).1 *
        sin
          (√(HPow.hPow (β := ℕ) (x, y).1 2 + HPow.hPow (β := ℕ) (x, y).2 2),
              Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y))).2) =
    (x, y)

Tactic:
simp [A]
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) (r, θ).1
hθ : (r, θ).2 ∈ Ioo (-π) π
fst :
  (√(HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 2 +
            HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 2),
        Complex.arg
          ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2))).1 =
    (r, θ).1
snd :
  (√(HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 2 +
            HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 2),
        Complex.arg
          ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2))).2 =
    (r, θ).2
⊢ (√(HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 2 +
          HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 2),
      Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2))) =
    (r, θ)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) (r, θ).1
hθ : (r, θ).2 ∈ Ioo (-π) π
fst : √(HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2) = r
⊢ (√(HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 2 +
            HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 2),
        Complex.arg
          ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2))).1 =
    (r, θ).1

Tactic:
dsimp at hr hθ ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) (r, θ).1
hθ : (r, θ).2 ∈ Ioo (-π) π
snd : Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ)) = θ
⊢ (√(HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 2 +
            HPow.hPow (β := ℕ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 2),
        Complex.arg
          ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2))).2 =
    (r, θ).2

Tactic:
dsimp at hr hθ ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
rw : √((HPow.hPow (β := ℕ) (sin θ) 2 + HPow.hPow (β := ℕ) (cos θ) 2) * HPow.hPow (β := ℕ) r 2)
| r

Tactic:
rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]

Premises used: le_of_lt, HPow.hPow, Real.sin_sq_add_cos_sq, Real.sqrt_sq, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
fst :
  √(HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2) =
    √((HPow.hPow (β := ℕ) (sin θ) 2 + HPow.hPow (β := ℕ) (cos θ) 2) * HPow.hPow (β := ℕ) r 2)
⊢ √(HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2) = r

Tactic:
conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]

Premises used: le_of_lt, HPow.hPow, Real.sin_sq_add_cos_sq, Real.sqrt_sq, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
fst :
  HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2 =
    (HPow.hPow (β := ℕ) (sin θ) 2 + HPow.hPow (β := ℕ) (cos θ) 2) * HPow.hPow (β := ℕ) r 2
⊢ √(HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2) =
    √((HPow.hPow (β := ℕ) (sin θ) 2 + HPow.hPow (β := ℕ) (cos θ) 2) * HPow.hPow (β := ℕ) r 2)

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
⊢ HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2 =
    (HPow.hPow (β := ℕ) (sin θ) 2 + HPow.hPow (β := ℕ) (cos θ) 2) * HPow.hPow (β := ℕ) r 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
⊢ ((↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)).arg = θ

Tactic:
Complex.arg_mul_cos_add_sin_mul_I hr ⟨hθ.1, hθ.2.le⟩

Premises used: Complex.arg_mul_cos_add_sin_mul_I, LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
h :
  (Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ) =
    (↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)
⊢ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ)) = θ

Tactic:
convert! Complex.arg_mul_cos_add_sin_mul_I hr ⟨hθ.1, hθ.2.le⟩

Premises used: Complex.arg_mul_cos_add_sin_mul_I, LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
h :
  (↑r : ℂ) * Complex.cos (↑θ : ℂ) + (↑r : ℂ) * Complex.sin (↑θ : ℂ) * Complex.I =
    (↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)
⊢ (Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ) =
    (↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)

Tactic:
simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos,
        Complex.ofReal_sin]

Premises used: Complex.equivRealProd_symm_apply, Complex.ofReal_cos, Complex.ofReal_sin, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
⊢ (↑r : ℂ) * Complex.cos (↑θ : ℂ) + (↑r : ℂ) * Complex.sin (↑θ : ℂ) * Complex.I =
    (↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ √(HPow.hPow (β := ℕ) q.1 2 + HPow.hPow (β := ℕ) q.2 2))
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
refine :
  ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) q))
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
⊢ ContinuousOn (Y := ℝ × ℝ)
    (fun (q : ℝ × ℝ) ↦
      (√(HPow.hPow (β := ℕ) q.1 2 + HPow.hPow (β := ℕ) q.2 2),
        Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) q)))
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})

Tactic:
refine .prodMk (by fun_prop) ?_
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
⊢ Membership.mem (α := ℂ) Complex.slitPlane ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y) : ℂ)

Tactic:
simpa only using hxy
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ MapsTo (α := ℝ × ℝ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    Complex.slitPlane

Tactic:
have A : MapsTo Complex.equivRealProd.symm ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
        Complex.slitPlane := by
      rintro ⟨x, y⟩ hxy; simpa only using hxy
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A :
  MapsTo (α := ℝ × ℝ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    Complex.slitPlane
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) q))
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})

Tactic:
ContinuousOn.comp (f := Complex.equivRealProd.symm)
      (g := Complex.arg) (fun z hz => ?_) ?_ A

Premises used: Complex.arg, ContinuousOn.comp, ite
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A :
  MapsTo (α := ℝ × ℝ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    Complex.slitPlane
refine_1 : ∀ (z : ℂ) (hz : z ∈ Complex.slitPlane), ContinuousWithinAt Complex.arg Complex.slitPlane z
refine_2 :
  ContinuousOn (X := ℝ × ℝ) (Y := ℂ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ)
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) q))
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})

Tactic:
refine ContinuousOn.comp (f := Complex.equivRealProd.symm)
      (g := Complex.arg) (fun z hz => ?_) ?_ A

Premises used: ContinuousOn.comp
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A :
  MapsTo (α := ℝ × ℝ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    Complex.slitPlane
z : ℂ
hz : z ∈ Complex.slitPlane
⊢ ContinuousWithinAt Complex.arg Complex.slitPlane z

Tactic:
(Complex.continuousAt_arg hz).continuousWithinAt

Premises used: Complex.continuousAt_arg, ContinuousAt.continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
A :
  MapsTo (α := ℝ × ℝ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    Complex.slitPlane
z : ℂ
hz : z ∈ Complex.slitPlane
⊢ ContinuousWithinAt Complex.arg Complex.slitPlane z

Tactic:
exact (Complex.continuousAt_arg hz).continuousWithinAt

Premises used: Complex.continuousAt_arg, ContinuousAt.continuousWithinAt