awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
inl :
  ∀ (h_eq : n = 0),
    ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
⊢ ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
have inr : n > 0 →
  ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
Tactic: rcases n.eq_zero_or_pos with h_eq | _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
h : n > 0
⊢ ConvexOn ℝ (β := ℝ) (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)
have inr : MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
  (interior (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)))
Tactic: apply MonotoneOn.convexOn_of_deriv (convex_Ici (n - 1 : ℝ))
      continuous_descPochhammer_eval.continuousOn
      differentiable_descPochhammer_eval.differentiableOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
h : n > 0
⊢ MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
    (interior (Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)))
have inr : MonotoneOn (β := ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n))
  (Set.Ioi (HSub.hSub (α := ℝ) (↑n : ℝ) 1))
Tactic: rw [interior_Ici]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
k n : ℕ
⊢ Eq (α := ℝ)
    ((Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (i : ℝ) ↦ ℝ)
        (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0 (↑k : ℝ) :
      ℝ)
    ((↑(k.descFactorial n) : ℝ) : ℝ)
have rw : (↑k : ℝ) < HSub.hSub (α := ℝ) (↑n : ℝ) 1 → LT.lt (α := ℝ) (↑k : ℝ) (↑n : ℝ)
Tactic: rw [Set.piecewise, descPochhammer_eval_eq_descFactorial, ite_eq_left_iff, Set.mem_Ici, not_le,
    eq_comm, Pi.zero_apply, Nat.cast_eq_zero, Nat.descFactorial_eq_zero_iff_lt, ← @Nat.cast_lt ℝ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
⊢ ConvexOn ℝ (β := ℝ) Set.univ
    ((Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (a : ℝ) ↦ ℝ)
      (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0)
have hn₁ : 0 < n
Tactic: rw [← Nat.pos_iff_ne_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ ConvexOn ℝ (β := ℝ) Set.univ
    ((Set.Ici (HSub.hSub (α := ℝ) (↑n : ℝ) 1)).piecewise (β := fun (a : ℝ) ↦ ℝ)
      (fun (x : ℝ) ↦ Polynomial.eval x (descPochhammer ℝ n)) 0)
have apply : Polynomial.eval (HSub.hSub (α := ℝ) (↑n : ℝ) 1) (descPochhammer ℝ n) = 0
Tactic: apply convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic
    (convexOn_descPochhammer_eval n) (convexOn_const 0 (convex_Iic (n - 1 : ℝ)))
    (monotoneOn_descPochhammer_eval n) antitoneOn_const
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
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
⊢ Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * (↑((p i).descFactorial n) : ℝ)
have suffices : f (∑ i ∈ t, HSMul.hSMul (β := ℝ) (w i) (↑(p i) : ℝ)) ≤ ∑ i ∈ t, w i • f (↑(p i) : ℝ)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
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) / (↑n.factorial : ℝ) ≤
    ∑ i ∈ t, w i * (↑((p i).choose n) : ℝ)
have 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 : ℝ)
Tactic: simp_rw [Nat.cast_choose_eq_descPochhammer_div,
    mul_div, ← Finset.sum_div, descPochhammer_eval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pochhammer (goal)
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) / (↑n.factorial : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ x ∈ t, w x * (↑((p x).descFactorial n) : ℝ)) (↑n.factorial : ℝ)
have apply : Polynomial.eval (∑ i ∈ t, w i * (↑(p i) : ℝ)) (descPochhammer ℝ n) ≤ ∑ x ∈ t, w x * (↑((p x).descFactorial n) : ℝ)
Tactic: apply div_le_div_of_nonneg_right _ (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
⊢ (√(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 (-π) π)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
⊢ 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)
have left : 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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
⊢ 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)
have right : 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
  Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have left : ∀ (hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | 0 < q.1} (x, y)),
  0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rcases hxy with hxy | hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have left₁ : ∀ (hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} (x, y)),
  0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rcases hxy with hxy | hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
x y : ℝ
hxy : 0 < x
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have 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
Tactic: linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} (x, y)
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have 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
Tactic: linarith [sq_nonneg x, sq_pos_of_ne_zero hxy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
x y : ℝ
hxy : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
⊢ 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0
have 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
Tactic: rcases hxy with hxy | hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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
⊢ 0 ≤ Complex.re ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ∨
    Complex.im ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (x, y)) ≠ 0
have 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
Tactic: rcases hxy with hxy | hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
⊢ Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)
have 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)
Tactic: rcases eq_or_ne θ 0 with (rfl | h'θ)
Cleared hypotheses: θ, hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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)
⊢ Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)
have inr : ∀ (h'θ : θ ≠ 0),
  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'θ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
    ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)
have inr : Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ Membership.mem (γ := Set (ℝ × ℝ)) {q : ℝ × ℝ | q.2 ≠ 0} ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)
have hr₁ : 0 < r
Tactic: simp at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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‖
have rw : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = √((Complex.normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + (↑y : ℂ) * Complex.I))
Tactic: rw [Complex.norm_def, Complex.normSq_add_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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))
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = ‖(↑x : ℂ) + (↑y : ℂ) * Complex.I‖
have rw₁ : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
Tactic: rw [Complex.norm_def, Complex.normSq_add_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
x y : ℝ
h : Membership.mem (γ := Set (ℝ × ℝ)) ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) (x, y)
⊢ ((√(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)
have A : √(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) (r, θ).1
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(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, θ)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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
⊢ (√(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, θ)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) (r, θ).1
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(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
have fst : √(HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2) = r
Tactic: dsimp at hr hθ ⊢
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) (r, θ).1
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(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
have snd : Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ)) = θ
Tactic: dsimp at hr hθ ⊢
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
| r
have rw : √((HPow.hPow (β := ℕ) (sin θ) 2 + HPow.hPow (β := ℕ) (cos θ) 2) * HPow.hPow (β := ℕ) r 2)
Tactic: rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
⊢ √(HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2) = r
have fst : √(HPow.hPow (β := ℕ) (r * cos θ) 2 + HPow.hPow (β := ℕ) (r * sin θ) 2) =
  √((HPow.hPow (β := ℕ) (sin θ) 2 + HPow.hPow (β := ℕ) (cos θ) 2) * HPow.hPow (β := ℕ) r 2)
Tactic: conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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)
have fst : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
⊢ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ)) = θ
have h : (Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ) =
  (↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)
Tactic: convert! Complex.arg_mul_cos_add_sin_mul_I hr ⟨hθ.1, hθ.2.le⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
r θ : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hθ : θ ∈ Ioo (-π) π
⊢ (Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (r * cos θ, r * sin θ) =
    (↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)
have h : (↑r : ℂ) * Complex.cos (↑θ : ℂ) + (↑r : ℂ) * Complex.sin (↑θ : ℂ) * Complex.I =
  (↑r : ℂ) * (Complex.cos (↑θ : ℂ) + Complex.sin (↑θ : ℂ) * Complex.I)
Tactic: simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos,
        Complex.ofReal_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
⊢ 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})
have refine : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) q))
  ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
Tactic: refine .prodMk (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (hypothesis)
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) q))
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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})
have refine_1 : ∀ (z : ℂ) (hz : z ∈ Complex.slitPlane), ContinuousWithinAt Complex.arg Complex.slitPlane z
Tactic: refine ContinuousOn.comp (f := Complex.equivRealProd.symm)
      (g := Complex.arg) (fun z hz => ?_) ?_ A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
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
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ Complex.arg ((Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ) q))
    ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
have refine_2 : ContinuousOn (X := ℝ × ℝ) (Y := ℂ) (⇑Complex.equivRealProd.symm : (a : ℝ × ℝ) → ℂ)
  ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
Tactic: refine ContinuousOn.comp (f := Complex.equivRealProd.symm)
      (g := Complex.arg) (fun z hz => ?_) ?_ A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.PolarCoord (goal)
Goal:
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
have 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
Tactic: rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]