awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
neg : (if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) = θ
neg₁ : ¬0 ≤ Real.cos θ
neg₂ : Real.arcsin (-Real.sin θ) + π = θ
neg₃ : 0 ≤ Real.sin θ
neg₄ : ¬0 ≤ Real.cos θ
neg₅ : Real.arcsin (Real.sin (θ - π)) + π = θ
neg₆ : 0 ≤ Real.sin θ
neg₇ : ¬0 ≤ Real.cos θ
neg₈ : θ - π + π = θ
neg₉ : -(π / 2) ≤ θ - π
neg₁₀ : θ - π ≤ π / 2
neg₁₁ : 0 ≤ Real.sin θ
neg₁₂ : ¬0 ≤ Real.cos θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁₃ : θ = θ
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = θ
have rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
hθ : θ ∈ Ioc (-π) π
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = θ
have rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
hθ : θ ∈ Ioc (-π) π
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = θ
have rw₂ : θ = θ
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ (cexp z).arg = toIocMod Real.two_pi_pos (-π) z.im
have h : (cexp z).arg =
  ((↑(rexp z.re) : ℂ) *
      (cos (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) + sin (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) * I)).arg
Tactic: convert!
    arg_mul_cos_add_sin_mul_I (Real.exp_pos z.re) (θ := toIocMod Real.two_pi_pos (-π) z.im) _
    using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h :
  (cexp z).arg =
    ((↑(rexp z.re) : ℂ) *
        (cos (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) + sin (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) * I)).arg
⊢ (cexp z).arg = toIocMod Real.two_pi_pos (-π) z.im
have arg_mul_cos_add_sin_mul_I : toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π
Tactic: convert!
    arg_mul_cos_add_sin_mul_I (Real.exp_pos z.re) (θ := toIocMod Real.two_pi_pos (-π) z.im) _
    using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ (cexp z).arg =
    ((↑(rexp z.re) : ℂ) *
        (cos (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) + sin (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) * I)).arg
have h : (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) : ℂ) * I)).arg
Tactic: rw [← exp_mul_I, ofReal_exp, toIocMod]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) : ℂ) * I)).arg
have h : (cexp z).arg = (cexp (↑z.re : ℂ) * cexp (((↑z.im : ℂ) - toIocDiv Real.two_pi_pos (-π) z.im • (2 * (↑π : ℂ))) * I)).arg
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ (cexp z).arg = (cexp (↑z.re : ℂ) * cexp (((↑z.im : ℂ) - toIocDiv Real.two_pi_pos (-π) z.im • (2 * (↑π : ℂ))) * I)).arg
have h : (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑z.im : ℂ) * I)).arg
Tactic: rw [exp_mul_I_periodic.sub_zsmul_eq, ← exp_add, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h : (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑z.im : ℂ) * I)).arg
⊢ (cexp z).arg = (cexp (↑z.re : ℂ) * cexp (((↑z.im : ℂ) - toIocDiv Real.two_pi_pos (-π) z.im • (2 * (↑π : ℂ))) * I)).arg
have h₁ : (cexp z).arg = (cexp ((↑z.re : ℂ) + (↑z.im : ℂ) * I)).arg
Tactic: rw [exp_mul_I_periodic.sub_zsmul_eq, ← exp_add, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h : (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑z.im : ℂ) * I)).arg
h₁ : (cexp z).arg = (cexp ((↑z.re : ℂ) + (↑z.im : ℂ) * I)).arg
⊢ (cexp z).arg = (cexp (↑z.re : ℂ) * cexp (((↑z.im : ℂ) - toIocDiv Real.two_pi_pos (-π) z.im • (2 * (↑π : ℂ))) * I)).arg
have h₂ : (cexp z).arg = (cexp z).arg
Tactic: rw [exp_mul_I_periodic.sub_zsmul_eq, ← exp_add, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π
have h : π = -π + 2 * π
Tactic: convert! toIocMod_mem_Ioc ..
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
⊢ x = y
have rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = y
Tactic: rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = y
⊢ x = y
have rw₁ : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
Tactic: rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = y
rw₁ : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
⊢ x = y
have rw₂ : (↑‖y‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
Tactic: rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = y
rw₁ : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
rw₂ : (↑‖y‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
⊢ x = y
have rw₃ : (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
Tactic: rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π
have hπ : 0 < π
Tactic: have hπ : 0 < π := Real.pi_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hπ : 0 < π
⊢ z.arg ∈ Ioc (-π) π
have inl : arg 0 ∈ Ioc (-π) π
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hπ : 0 < π
inl : arg 0 ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π
have inr : ∀ (hz : z ≠ 0), z.arg ∈ Ioc (-π) π
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ z.arg ∈ Ioc (-π) π
have inr : ∀ (N : ℤ) (hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)), z.arg ∈ Ioc (-π) π
Tactic: rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ z.arg ∈ Ioc (-π) π
have hN₁ : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
Tactic: rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π
have inr : ((↑‖z‖ : ℂ) *
      (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg ∈
  Ioc (-π) π
Tactic: rw [← norm_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
⊢ ((↑‖z‖ : ℂ) *
        (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg ∈
    Ioc (-π) π
have this : ((↑‖z‖ : ℂ) * (cos (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) + sin (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) * I)).arg =
  z.arg + (↑N : ℝ) * (2 * π)
Tactic: have := arg_mul_cos_add_sin_mul_I (norm_pos_iff.mpr hz) hN
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
this :
  ((↑‖z‖ : ℂ) * (cos (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) + sin (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) * I)).arg =
    z.arg + (↑N : ℝ) * (2 * π)
⊢ ((↑‖z‖ : ℂ) *
        (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg ∈
    Ioc (-π) π
have this₁ : ((↑‖z‖ : ℂ) *
      (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg =
  z.arg + (↑N : ℝ) * (2 * π)
Tactic: push_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im
have inl : 0 ≤ arg 0 ↔ 0 ≤ im 0
Tactic: rcases eq_or_ne z 0 with (rfl | h₀)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
inl : 0 ≤ arg 0 ↔ 0 ≤ im 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im
have inr : ∀ (h₀ : z ≠ 0), 0 ≤ z.arg ↔ 0 ≤ z.im
Tactic: rcases eq_or_ne z 0 with (rfl | h₀)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg → 0 ≤ z.arg
have contrapose! : z.arg < 0 → Real.sin z.arg < 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im
have rw : 0 ≤ z.im / ‖z‖ ↔ 0 ≤ z.im
Tactic: rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : z ≠ 0
rw : 0 ≤ z.im / ‖z‖ ↔ 0 ≤ z.im
⊢ 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im
have rw₁ : 0 * ‖z‖ ≤ z.im ↔ 0 ≤ z.im
Tactic: rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : z ≠ 0
rw : 0 ≤ z.im / ‖z‖ ↔ 0 ≤ z.im
rw₁ : 0 * ‖z‖ ≤ z.im ↔ 0 ≤ z.im
⊢ 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im
have rw₂ : 0 ≤ z.im ↔ 0 ≤ z.im
Tactic: rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im
have arg : 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im
Tactic: calc
    0 ≤ arg z ↔ 0 ≤ Real.sin (arg z) :=
      ⟨fun h => Real.sin_nonneg_of_mem_Icc ⟨h, arg_le_pi z⟩, by
        contrapose!
        intro h
        exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)⟩
    _ ↔ _ := by rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
r : ℝ
hr : 0 < r
⊢ ((↑r : ℂ) * x).arg = x.arg
have inl : ((↑r : ℂ) * 0).arg = arg 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
r : ℝ
hr : 0 < r
inl : ((↑r : ℂ) * 0).arg = arg 0
⊢ ((↑r : ℂ) * x).arg = x.arg
have inr : ∀ (hx : x ≠ 0), ((↑r : ℂ) * x).arg = x.arg
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
⊢ ((↑r : ℂ) * 0).arg = arg 0
have inl : arg 0 = arg 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| ((↑r : ℂ) * x).arg
have rw : x.arg
Tactic: rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
      arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ ((↑r : ℂ) * x).arg = x.arg
have conv_lhs : ((↑r : ℂ) * x).arg = x.arg
Tactic: conv_lhs =>
    rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
      arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
conv_lhs : ((↑r : ℂ) * x).arg = x.arg
⊢ ((↑r : ℂ) * x).arg = x.arg
have inr : x.arg = x.arg
Tactic: conv_lhs =>
    rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
      arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ (↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x = y
have simp : x.arg = y.arg ↔ ((↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x).arg = y.arg
Tactic: simp only [ext_norm_arg_iff, norm_mul, norm_div, norm_real, norm_norm,
    div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hx), true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ ((↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x).arg = y.arg
have hr : 0 < ‖y‖ / ‖x‖
Tactic: rw [← ofReal_div, arg_real_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (x / x).arg = 0
have inl : (0 / 0).arg = 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
inl : (0 / 0).arg = 0
⊢ (x / x).arg = 0
have inr : ∀ (hx : x ≠ 0), (x / x).arg = 0
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ Real.tan x.arg = x.im / x.re
have pos : ∀ (h : x = 0), Real.tan x.arg = x.im / x.re
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
pos : ∀ (h : x = 0), Real.tan x.arg = x.im / x.re
⊢ Real.tan x.arg = x.im / x.re
have neg : ∀ (h : ¬x = 0), Real.tan x.arg = x.im / x.re
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : ¬x = 0
⊢ Real.tan x.arg = x.im / x.re
have neg : Real.sin x.arg / Real.cos x.arg = x.im / x.re
Tactic: rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
    div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : ¬x = 0
neg : Real.sin x.arg / Real.cos x.arg = x.im / x.re
⊢ Real.tan x.arg = x.im / x.re
have neg₁ : x.im / ‖x‖ / Real.cos x.arg = x.im / x.re
Tactic: rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
    div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : ¬x = 0
neg : Real.sin x.arg / Real.cos x.arg = x.im / x.re
neg₁ : x.im / ‖x‖ / Real.cos x.arg = x.im / x.re
⊢ Real.tan x.arg = x.im / x.re
have neg₂ : x.im / ‖x‖ / (x.re / ‖x‖) = x.im / x.re
Tactic: rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
    div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : ¬x = 0
neg : Real.sin x.arg / Real.cos x.arg = x.im / x.re
neg₁ : x.im / ‖x‖ / Real.cos x.arg = x.im / x.re
neg₂ : x.im / ‖x‖ / (x.re / ‖x‖) = x.im / x.re
⊢ Real.tan x.arg = x.im / x.re
have neg₃ : x.im / x.re = x.im / x.re
Tactic: rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
    div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0
have refine_1 : ∀ (h : z.arg = 0), 0 ≤ z.re ∧ z.im = 0
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
refine_1 : ∀ (h : z.arg = 0), 0 ≤ z.re ∧ z.im = 0
⊢ z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0
have refine_2 : 0 ≤ z.re ∧ z.im = 0 → z.arg = 0
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h : z.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0
have refine_1 : 0 ≤ ((↑‖z‖ : ℂ) * (cos (↑0 : ℂ) + sin (↑0 : ℂ) * I)).re ∧ ((↑‖z‖ : ℂ) * (cos (↑0 : ℂ) + sin (↑0 : ℂ) * I)).im = 0
Tactic: rw [← norm_mul_cos_add_sin_mul_I z, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0
have refine_2 : ∀ (x y : ℝ), 0 ≤ { re := x, im := y : ℂ }.re ∧ { re := x, im := y : ℂ }.im = 0 → { re := x, im := y : ℂ }.arg = 0
Tactic: obtain ⟨x, y⟩ := z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z
have rw : 0 ≤ z.re ∧ z.im = 0 ↔ 0 ≤ z
Tactic: rw [arg_eq_zero_iff, eq_comm, nonneg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : 0 ≤ z.re ∧ z.im = 0 ↔ 0 ≤ z
⊢ z.arg = 0 ↔ 0 ≤ z
have rw₁ : 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z
Tactic: rw [arg_eq_zero_iff, eq_comm, nonneg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : 0 ≤ z.re ∧ z.im = 0 ↔ 0 ≤ z
rw₁ : 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z
⊢ z.arg = 0 ↔ 0 ≤ z
have rw₂ : 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z.re ∧ 0 = z.im
Tactic: rw [arg_eq_zero_iff, eq_comm, nonneg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
have pos : ∀ (h₀ : z = 0), z.arg = π ↔ z.re < 0 ∧ z.im = 0
Tactic: by_cases h₀ : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
pos : ∀ (h₀ : z = 0), z.arg = π ↔ z.re < 0 ∧ z.im = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
have neg : ∀ (h₀ : ¬z = 0), z.arg = π ↔ z.re < 0 ∧ z.im = 0
Tactic: by_cases h₀ : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
have neg : z.arg = π → z.re < 0 ∧ z.im = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
neg : z.arg = π → z.re < 0 ∧ z.im = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
have neg₁ : z.re < 0 ∧ z.im = 0 → z.arg = π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ z.re < 0 ∧ z.im = 0
have neg : ((↑‖z‖ : ℂ) * (cos (↑π : ℂ) + sin (↑π : ℂ) * I)).re < 0 ∧ ((↑‖z‖ : ℂ) * (cos (↑π : ℂ) + sin (↑π : ℂ) * I)).im = 0
Tactic: rw [← norm_mul_cos_add_sin_mul_I z, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π
have neg : ∀ (x y : ℝ) (h₀ : ¬{ re := x, im := y : ℂ } = 0),
  { re := x, im := y : ℂ }.re < 0 ∧ { re := x, im := y : ℂ }.im = 0 → { re := x, im := y : ℂ }.arg = π
Tactic: obtain ⟨x, y⟩ := z
Cleared hypotheses: z, h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 : ℂ } = 0
⊢ { re := x, im := 0 : ℂ }.arg = π
have neg : { re := x, im := 0 : ℂ }.arg = ((↑(-x) : ℂ) * -1).arg
Tactic: rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
have rw : z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
Tactic: rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
have rw₁ : ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π
Tactic: rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
rw₁ : ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
have rw₂ : ¬0 ≤ z.re ∧ ¬z.im ≠ 0 ↔ z.arg = π
Tactic: rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
rw₁ : ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π
rw₂ : ¬0 ≤ z.re ∧ ¬z.im ≠ 0 ↔ z.arg = π
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
have rw₃ : z.re < 0 ∧ ¬z.im ≠ 0 ↔ z.arg = π
Tactic: rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
rw₁ : ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π
rw₂ : ¬0 ≤ z.re ∧ ¬z.im ≠ 0 ↔ z.arg = π
rw₃ : z.re < 0 ∧ ¬z.im ≠ 0 ↔ z.arg = π
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
have rw₄ : z.re < 0 ∧ z.im = 0 ↔ z.arg = π
Tactic: rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
rw₁ : ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π
rw₂ : ¬0 ≤ z.re ∧ ¬z.im ≠ 0 ↔ z.arg = π
rw₃ : z.re < 0 ∧ ¬z.im ≠ 0 ↔ z.arg = π
rw₄ : z.re < 0 ∧ z.im = 0 ↔ z.arg = π
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
have rw₅ : z.re < 0 ∧ z.im = 0 ↔ z.re < 0 ∧ z.im = 0
Tactic: rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
have pos : ∀ (h₀ : z = 0), z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
Tactic: by_cases h₀ : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
pos : ∀ (h₀ : z = 0), z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
have neg : ∀ (h₀ : ¬z = 0), z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
Tactic: by_cases h₀ : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
have neg : z.arg = π / 2 → z.re = 0 ∧ 0 < z.im
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
neg : z.arg = π / 2 → z.re = 0 ∧ 0 < z.im
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
have neg₁ : z.re = 0 ∧ 0 < z.im → z.arg = π / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ z.re = 0 ∧ 0 < z.im
have neg : ((↑‖z‖ : ℂ) * (cos (↑(π / 2) : ℂ) + sin (↑(π / 2) : ℂ) * I)).re = 0 ∧
  0 < ((↑‖z‖ : ℂ) * (cos (↑(π / 2) : ℂ) + sin (↑(π / 2) : ℂ) * I)).im
Tactic: rw [← norm_mul_cos_add_sin_mul_I z, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2
have neg : ∀ (x y : ℝ) (h₀ : ¬{ re := x, im := y : ℂ } = 0),
  { re := x, im := y : ℂ }.re = 0 ∧ 0 < { re := x, im := y : ℂ }.im → { re := x, im := y : ℂ }.arg = π / 2
Tactic: obtain ⟨x, y⟩ := z
Cleared hypotheses: z, h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : 0 < y
⊢ { re := 0, im := y : ℂ }.arg = π / 2
have neg : { re := 0, im := y : ℂ }.arg = I.arg
Tactic: rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : 0 < y
neg : { re := 0, im := y : ℂ }.arg = I.arg
⊢ { re := 0, im := y : ℂ }.arg = π / 2
have neg₁ : { re := 0, im := y : ℂ }.arg = ((↑y : ℂ) * I).arg
Tactic: rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]