awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(x * y).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)
have h : x * y =
  (↑(‖x‖ * ‖y‖) : ℂ) *
    ((↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).cos : ℂ) +
      (↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).sin : ℂ) * I)
Tactic: convert!
    arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy))
      (arg x + arg y : Real.Angle) using 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y =
    (↑(‖x‖ * ‖y‖) : ℂ) *
      ((↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).cos : ℂ) +
        (↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).sin : ℂ) * I)
have h : x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
Tactic: simp_rw [← Real.Angle.coe_add, Real.Angle.sin_coe, Real.Angle.cos_coe, ofReal_cos, ofReal_sin,
    cos_add_sin_I, ofReal_add, add_mul, exp_add, ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
have h : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I)))
Tactic: rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
h : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I)))
⊢ x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
have h₁ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I)))
Tactic: rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
h : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I)))
h₁ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I)))
⊢ x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
have h₂ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I))
Tactic: rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
h : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I)))
h₁ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I)))
h₂ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I))
⊢ x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
have h₃ : x * y = (↑‖x‖ : ℂ) * (y * cexp ((↑x.arg : ℂ) * I))
Tactic: rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
h : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I)))
h₁ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I)))
h₂ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I))
h₃ : x * y = (↑‖x‖ : ℂ) * (y * cexp ((↑x.arg : ℂ) * I))
⊢ x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
have h₄ : x * y = (↑‖x‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * y)
Tactic: rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
h : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I)))
h₁ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I)))
h₂ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I))
h₃ : x * y = (↑‖x‖ : ℂ) * (y * cexp ((↑x.arg : ℂ) * I))
h₄ : x * y = (↑‖x‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * y)
⊢ x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
have h₅ : x * y = (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) * y
Tactic: rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
h : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I)))
h₁ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * (cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I)))
h₂ : x * y = (↑‖x‖ : ℂ) * ((↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I) * cexp ((↑x.arg : ℂ) * I))
h₃ : x * y = (↑‖x‖ : ℂ) * (y * cexp ((↑x.arg : ℂ) * I))
h₄ : x * y = (↑‖x‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * y)
h₅ : x * y = (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) * y
⊢ x * y = (↑‖x‖ : ℂ) * (↑‖y‖ : ℂ) * (cexp ((↑x.arg : ℂ) * I) * cexp ((↑y.arg : ℂ) * I))
have h₆ : x * y = x * y
Tactic: rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(x / y).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
have rw : (↑(x * y⁻¹).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
Tactic: rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
rw : (↑(x * y⁻¹).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
⊢ (↑(x / y).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
have rw₁ : (↑x.arg : Real.Angle) + (↑y⁻¹.arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
Tactic: rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
rw : (↑(x * y⁻¹).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
rw₁ : (↑x.arg : Real.Angle) + (↑y⁻¹.arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
⊢ (↑(x / y).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
have rw₂ : (↑x.arg : Real.Angle) + -(↑y.arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
Tactic: rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
rw : (↑(x * y⁻¹).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
rw₁ : (↑x.arg : Real.Angle) + (↑y⁻¹.arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
rw₂ : (↑x.arg : Real.Angle) + -(↑y.arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
⊢ (↑(x / y).arg : Real.Angle) = (↑x.arg : Real.Angle) - (↑y.arg : Real.Angle)
have rw₃ : (↑x.arg : Real.Angle) + -(↑y.arg : Real.Angle) = (↑x.arg : Real.Angle) + -(↑y.arg : Real.Angle)
Tactic: rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
n : ℕ
⊢ (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
have inl : (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
Tactic: obtain rfl | x0 := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
n : ℕ
inl : (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
⊢ (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
have inr : ∀ (x0 : x ≠ 0), (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
Tactic: obtain rfl | x0 := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
n : ℕ
⊢ (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
have pos : ∀ (n0 : n = 0), (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
Tactic: by_cases n0 : n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
n : ℕ
pos : ∀ (n0 : n = 0), (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
⊢ (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
have neg : ∀ (n0 : ¬n = 0), (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
Tactic: by_cases n0 : n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
⊢ (↑(x ^ (n + 1)).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
have inr : (↑(x ^ n * x).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
Tactic: rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
inr : (↑(x ^ n * x).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
⊢ (↑(x ^ (n + 1)).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
have inr₁ : (↑(x ^ n).arg : Real.Angle) + (↑x.arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
Tactic: rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
inr : (↑(x ^ n * x).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
inr₁ : (↑(x ^ n).arg : Real.Angle) + (↑x.arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
⊢ (↑(x ^ (n + 1)).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
have inr₂ : n • (↑x.arg : Real.Angle) + (↑x.arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
Tactic: rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
inr : (↑(x ^ n * x).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
inr₁ : (↑(x ^ n).arg : Real.Angle) + (↑x.arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
inr₂ : n • (↑x.arg : Real.Angle) + (↑x.arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
⊢ (↑(x ^ (n + 1)).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
have inr₃ : n • (↑x.arg : Real.Angle) + (↑x.arg : Real.Angle) = n • (↑x.arg : Real.Angle) + (↑x.arg : Real.Angle)
Tactic: rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
n : ℕ
x0 : x ≠ 0
⊢ (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
have inr : (↑(HPow.hPow (β := ℕ) x 0).arg : Real.Angle) = HSMul.hSMul (α := ℕ) 0 (↑x.arg : Real.Angle)
Tactic: induction n with
    | zero => simp
    | succ n ih => rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
n : ℕ
x0 : x ≠ 0
inr : (↑(HPow.hPow (β := ℕ) x 0).arg : Real.Angle) = HSMul.hSMul (α := ℕ) 0 (↑x.arg : Real.Angle)
⊢ (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
have inr₁ : ∀ (n : ℕ) (ih : (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)),
  (↑(x ^ (n + 1)).arg : Real.Angle) = (n + 1) • (↑x.arg : Real.Angle)
Tactic: induction n with
    | zero => simp
    | succ n ih => rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ (↑z.arg : Real.Angle).toReal = z.arg
have rw : z.arg ∈ Ioc (-π) π
Tactic: rw [Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
θ : Real.Angle
⊢ (↑z.arg : Real.Angle) = θ ↔ z.arg = θ.toReal
have rw : (↑z.arg : Real.Angle).toReal = θ.toReal ↔ z.arg = θ.toReal
Tactic: rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
θ : Real.Angle
rw : (↑z.arg : Real.Angle).toReal = θ.toReal ↔ z.arg = θ.toReal
⊢ (↑z.arg : Real.Angle) = θ ↔ z.arg = θ.toReal
have rw₁ : z.arg = θ.toReal ↔ z.arg = θ.toReal
Tactic: rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
⊢ (↑x.arg : Real.Angle) = (↑y.arg : Real.Angle) ↔ x.arg = y.arg
have simp_rw : (↑x.arg : Real.Angle).toReal = (↑y.arg : Real.Angle).toReal ↔ x.arg = y.arg
Tactic: simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
have rw : (↑(x * y).arg : Real.Angle).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
Tactic: rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
      Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
rw : (↑(x * y).arg : Real.Angle).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
⊢ (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
have rw₁ : ((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
Tactic: rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
      Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
rw : (↑(x * y).arg : Real.Angle).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
rw₁ : ((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
⊢ (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
have rw₂ : (↑(x.arg + y.arg) : Real.Angle).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
Tactic: rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
      Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
rw : (↑(x * y).arg : Real.Angle).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
rw₁ : ((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
rw₂ : (↑(x.arg + y.arg) : Real.Angle).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
⊢ (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
have rw₃ : x.arg + y.arg ∈ Ioc (-π) π ↔ x.arg + y.arg ∈ Ioc (-π) π
Tactic: rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
      Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ arg =ᶠ[𝓝 x] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
have suffices : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
Tactic: suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im from
    h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
have refine : IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ 0 < y.im
Tactic: refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ arg =ᶠ[𝓝 x] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π
have suffices : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
Tactic: suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ y.im < 0 from
    h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_neg hy.1 hy.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
have refine : IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ y.im < 0
Tactic: refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0
have rw : x ≠ 0
Tactic: rw [norm_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt arg x
have h₀ : ‖x‖ ≠ 0
Tactic: have h₀ : ‖x‖ ≠ 0 := by
    rw [norm_ne_zero_iff]
    exact slitPlane_ne_zero h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
x : ℂ
h : x ∈ slitPlane
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x
have h₁ : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
Tactic: rw [mem_slitPlane_iff, ← lt_or_lt_iff_ne] at h
Cleared hypotheses: h, h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x
have inl : ∀ (hx_re : 0 < x.re), ContinuousAt arg x
Tactic: rcases h with (hx_re | hx_im | hx_im)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
inl : ∀ (hx_re : 0 < x.re), ContinuousAt arg x
⊢ ContinuousAt arg x
have inr : ∀ (hx_im : x.im < 0), ContinuousAt arg x
Tactic: rcases h with (hx_re | hx_im | hx_im)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
inl : ∀ (hx_re : 0 < x.re), ContinuousAt arg x
inr : ∀ (hx_im : x.im < 0), ContinuousAt arg x
⊢ ContinuousAt arg x
have inr₁ : ∀ (hx_im : 0 < x.im), ContinuousAt arg x
Tactic: rcases h with (hx_re | hx_im | hx_im)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
⊢ Tendsto arg (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
have refine : (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z : ℂ | z.im < 0}] z] arg
Tactic: refine H.congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
⊢ (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z : ℂ | z.im < 0}] z] arg
have this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
Tactic: have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z : ℂ | z.im < 0}] z] arg
have h : ∀ (a : ℂ) (him : a.im < 0) (hre : a.re < 0), Real.arcsin ((-a).im / ‖a‖) - π = a.arg
Tactic: filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds this] with _ him hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre_1 : z.re < 0
him_1 : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a : ℂ
him : a.im < 0
hre : a.re < 0
⊢ Real.arcsin ((-a).im / ‖a‖) - π = a.arg
have h : Real.arcsin ((-a).im / ‖a‖) - π =
  if 0 ≤ a.re then Real.arcsin (a.im / ‖a‖)
  else if 0 ≤ a.im then Real.arcsin ((-a).im / ‖a‖) + π else Real.arcsin ((-a).im / ‖a‖) - π
Tactic: rw [arg, if_neg hre.not_ge, if_neg him.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre_1 : z.re < 0
him_1 : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a : ℂ
him : a.im < 0
hre : a.re < 0
h :
  Real.arcsin ((-a).im / ‖a‖) - π =
    if 0 ≤ a.re then Real.arcsin (a.im / ‖a‖)
    else if 0 ≤ a.im then Real.arcsin ((-a).im / ‖a‖) + π else Real.arcsin ((-a).im / ‖a‖) - π
⊢ Real.arcsin ((-a).im / ‖a‖) - π = a.arg
have h₁ : Real.arcsin ((-a).im / ‖a‖) - π = if 0 ≤ a.im then Real.arcsin ((-a).im / ‖a‖) + π else Real.arcsin ((-a).im / ‖a‖) - π
Tactic: rw [arg, if_neg hre.not_ge, if_neg him.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre_1 : z.re < 0
him_1 : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a : ℂ
him : a.im < 0
hre : a.re < 0
h :
  Real.arcsin ((-a).im / ‖a‖) - π =
    if 0 ≤ a.re then Real.arcsin (a.im / ‖a‖)
    else if 0 ≤ a.im then Real.arcsin ((-a).im / ‖a‖) + π else Real.arcsin ((-a).im / ‖a‖) - π
h₁ :
  Real.arcsin ((-a).im / ‖a‖) - π =
    if 0 ≤ a.im then Real.arcsin ((-a).im / ‖a‖) + π else Real.arcsin ((-a).im / ‖a‖) - π
⊢ Real.arcsin ((-a).im / ‖a‖) - π = a.arg
have h₂ : Real.arcsin ((-a).im / ‖a‖) - π = Real.arcsin ((-a).im / ‖a‖) - π
Tactic: rw [arg, if_neg hre.not_ge, if_neg him.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
have suffices : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
Tactic: suffices H : Tendsto (fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) - π)
      (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 (-π)) by
    refine H.congr' ?_
    have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
    filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds this] with _ him hre
    rw [arg, if_neg hre.not_ge, if_neg him.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
have h : 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun (a : ℂ) ↦ ‖a‖)) z - π)
Tactic: convert!
    (Real.continuousAt_arcsin.comp_continuousWithinAt
          ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
            continuous_norm.continuousWithinAt _)).sub_const
      π using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
h : 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun (a : ℂ) ↦ ‖a‖)) z - π)
⊢ Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
have convert_3 : ‖z‖ ≠ 0
Tactic: convert!
    (Real.continuousAt_arcsin.comp_continuousWithinAt
          ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
            continuous_norm.continuousWithinAt _)).sub_const
      π using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
have convert_3 : ∀ (z : ℝ) (hre : (↑z : ℂ).re < 0), ‖(↑z : ℂ)‖ ≠ 0
Tactic: lift z to ℝ using him
Cleared hypotheses: z, hre, him
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
have this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
Tactic: have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)