awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑((↑(‖x‖ * ‖y‖) : ℂ) *
            ((↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).cos : ℂ) +
              (↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).sin : ℂ) * I)).arg :
      Real.Angle) =
    (↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)

Tactic:
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)

Premises used: Iff.mpr, norm_pos_iff, Real.Angle.coe, Complex.arg, Complex.arg_mul_cos_add_sin_mul_I_coe_angle, mul_pos, HAdd.hAdd
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
h :
  x * y =
    (↑(‖x‖ * ‖y‖) : ℂ) *
      ((↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).cos : ℂ) +
        (↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).sin : ℂ) * I)
⊢ (↑(x * y).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)

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

Premises used: Iff.mpr, norm_pos_iff, Real.Angle.coe, Complex.arg, Complex.arg_mul_cos_add_sin_mul_I_coe_angle, mul_pos, HAdd.hAdd
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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‖) : ℂ) *
      ((↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).cos : ℂ) +
        (↑((↑x.arg : Real.Angle) + (↑y.arg : Real.Angle)).sin : ℂ) * 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]

Premises used: add_mul, Complex.exp_add, Real.Angle.coe_add, Complex.ofReal_add, Complex.cos_add_sin_I, Real.Angle.sin_coe, Real.Angle.cos_coe, Complex.ofReal_cos, Complex.ofReal_sin, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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
h₆ h₇ : x * y = x * y
⊢ 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]

Premises used: Norm.norm, mul_assoc, Complex.ofReal, Complex.norm_mul_exp_arg_mul_I, mul_comm, Complex.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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)
rw₃ 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)

Tactic:
rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]

Premises used: sub_eq_add_neg, div_eq_mul_inv, inv_ne_zero, Complex.arg_inv_coe_angle, Complex.arg_mul_coe_angle
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
n : ℕ
inl : (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
inr : ∀ (x0 : x ≠ 0), (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)
⊢ (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)

Tactic:
obtain rfl | x0 := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
n : ℕ
pos : ∀ (n0 : n = 0), (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)
neg : ∀ (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)

Tactic:
by_cases n0 : n = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
n : ℕ
n0 : n = 0
⊢ (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)

Tactic:
simp [n0]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
n : ℕ
n0 : ¬n = 0
⊢ (↑(HPow.hPow (α := ℂ) 0 n).arg : Real.Angle) = n • (↑(arg 0) : Real.Angle)

Tactic:
simp [n0]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
x0 : x ≠ 0
⊢ (↑(HPow.hPow (β := ℕ) x 0).arg : Real.Angle) = HSMul.hSMul (α := ℕ) 0 (↑x.arg : Real.Angle)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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)
inr₃ inr₄ : n • (↑x.arg : Real.Angle) + (↑x.arg : Real.Angle) = n • (↑x.arg : Real.Angle) + (↑x.arg : Real.Angle)
⊢ (↑(x ^ (n + 1)).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]

Premises used: pow_succ, pow_ne_zero, Complex.arg_mul_coe_angle, succ_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
n : ℕ
x0 : x ≠ 0
inr : (↑(HPow.hPow (β := ℕ) x 0).arg : Real.Angle) = HSMul.hSMul (α := ℕ) 0 (↑x.arg : Real.Angle)
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)
⊢ (↑(x ^ n).arg : Real.Angle) = n • (↑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]

Premises used: pow_succ, pow_ne_zero, Complex.arg_mul_coe_angle, succ_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
n : ℤ
m : ℕ
⊢ (↑(x ^ Int.ofNat m).arg : Real.Angle) = Int.ofNat m • (↑x.arg : Real.Angle)

Tactic:
simp [arg_pow_coe_angle]

Premises used: Complex.arg_pow_coe_angle
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
n : ℤ
m : ℕ
⊢ (↑(x ^ Int.negSucc m).arg : Real.Angle) = Int.negSucc m • (↑x.arg : Real.Angle)

Tactic:
simp [arg_pow_coe_angle]

Premises used: Complex.arg_pow_coe_angle
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
n : ℤ
⊢ (↑(x ^ n).arg : Real.Angle) = n • (↑x.arg : Real.Angle)

Tactic:
match n with
  | Int.ofNat m => simp [arg_pow_coe_angle]
  | Int.negSucc m => simp [arg_pow_coe_angle]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
rw : z.arg ∈ Ioc (-π) π
⊢ (↑z.arg : Real.Angle).toReal = z.arg

Tactic:
rw [Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]

Premises used: Real.Angle.toReal_coe_eq_self_iff_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
arg_mem_Ioc _

Premises used: Complex.arg_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
exact arg_mem_Ioc _

Premises used: Complex.arg_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
θ : Real.Angle
rw : (↑z.arg : Real.Angle).toReal = θ.toReal ↔ z.arg = θ.toReal
rw₁ rw₂ : z.arg = θ.toReal ↔ z.arg = θ.toReal
⊢ (↑z.arg : Real.Angle) = θ ↔ z.arg = θ.toReal

Tactic:
rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

Premises used: Real.Angle.toReal_inj, Complex.arg_coe_angle_toReal_eq_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
simp_rw : (↑x.arg : Real.Angle).toReal = (↑y.arg : Real.Angle).toReal ↔ x.arg = y.arg
⊢ (↑x.arg : Real.Angle) = (↑y.arg : Real.Angle) ↔ x.arg = y.arg

Tactic:
simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

Premises used: Real.Angle.toReal_inj, Complex.arg_coe_angle_toReal_eq_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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 (-π) π
rw₃ rw₄ : x.arg + y.arg ∈ Ioc (-π) π ↔ x.arg + y.arg ∈ Ioc (-π) π
⊢ (x * y).arg = 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]

Premises used: Real.Angle.toReal_coe_eq_self_iff_mem_Ioc, Real.Angle.coe_add, Complex.arg_coe_angle_toReal_eq_arg, Complex.arg_mul_coe_angle
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ z ∈ slitPlane ↔ z.arg ≠ π ∧ z ≠ 0

Tactic:
simp only [mem_slitPlane_iff_not_le_zero, le_iff_lt_or_eq, ne_eq, arg_eq_pi_iff_lt_zero, not_or]

Premises used: ne_eq, not_or, le_iff_lt_or_eq, Complex.mem_slitPlane_iff_not_le_zero, Complex.arg_eq_pi_iff_lt_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ z.arg ≠ π

Tactic:
(mem_slitPlane_iff_arg.mp hz).1

Premises used: Complex.mem_slitPlane_iff_arg, And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ cexp z ∈ slitPlane ↔ toIocMod Real.two_pi_pos (-π) z.im ≠ π

Tactic:
simp [mem_slitPlane_iff_arg, arg_exp]

Premises used: Complex.mem_slitPlane_iff_arg, Complex.arg_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : 0 < x.re
⊢ arg =ᶠ[𝓝 x] fun (x : ℂ) ↦ Real.arcsin (x.im / ‖x‖)

Tactic:
((continuous_re.tendsto _).eventually (lt_mem_nhds hx)).mono fun _ hy => arg_of_re_nonneg hy.le

Premises used: Complex.arg_of_re_nonneg, Complex.continuous_re, Filter.EventuallyEq, LT.lt.le, Filter.Eventually.mono, Continuous.tendsto, Filter.Tendsto.eventually, lt_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
suffices : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
⊢ arg =ᶠ[𝓝 x] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π

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
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im

Tactic:
IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)

Premises used: Set.Mem, IsOpen.eventually_mem, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
refine : IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ 0 < y.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im

Tactic:
refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)

Premises used: IsOpen.eventually_mem, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ 0 < y.im

Tactic:
IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)

Premises used: isOpen_lt, Complex.continuous_re, setOf, continuous_zero, IsOpen.and, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ 0 < y.im

Tactic:
exact
    IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)

Premises used: isOpen_lt, Complex.continuous_re, continuous_zero, IsOpen.and, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
suffices : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
⊢ arg =ᶠ[𝓝 x] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π

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
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0

Tactic:
IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)

Premises used: Set.Mem, IsOpen.eventually_mem, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
refine : IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ y.im < 0
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0

Tactic:
refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)

Premises used: IsOpen.eventually_mem, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ y.im < 0

Tactic:
IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)

Premises used: isOpen_lt, Complex.continuous_re, setOf, continuous_zero, IsOpen.and, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ IsOpen (X := ℂ) fun (y : ℂ) ↦ y.re < 0 ∧ y.im < 0

Tactic:
exact
    IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)

Premises used: isOpen_lt, Complex.continuous_re, continuous_zero, IsOpen.and, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : 0 < z.im
⊢ arg =ᶠ[𝓝 z] fun (x : ℂ) ↦ Real.arccos (x.re / ‖x‖)

Tactic:
((continuous_im.tendsto _).eventually (lt_mem_nhds hz)).mono fun _ => arg_of_im_pos

Premises used: Complex.arg_of_im_pos, Filter.EventuallyEq, Filter.Eventually.mono, Continuous.tendsto, Filter.Tendsto.eventually, lt_mem_nhds, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z.im < 0
⊢ arg =ᶠ[𝓝 z] fun (x : ℂ) ↦ -Real.arccos (x.re / ‖x‖)

Tactic:
((continuous_im.tendsto _).eventually (gt_mem_nhds hz)).mono fun _ => arg_of_im_neg

Premises used: gt_mem_nhds, Filter.EventuallyEq, Filter.Eventually.mono, Continuous.tendsto, Complex.arg_of_im_neg, Filter.Tendsto.eventually, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ∈ slitPlane
rw : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ x ≠ 0

Tactic:
slitPlane_ne_zero h

Premises used: Complex.slitPlane_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ x ≠ 0

Tactic:
exact slitPlane_ne_zero h

Premises used: Complex.slitPlane_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Tactic:
have h₀ : ‖x‖ ≠ 0 := by
    rw [norm_ne_zero_iff]
    exact slitPlane_ne_zero h
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ∈ slitPlane
h₀ : ‖x‖ ≠ 0
⊢ 0 < x.re ∨ x.im < 0 ∨ 0 < x.im

Tactic:
rw [mem_slitPlane_iff, ← lt_or_lt_iff_ne] at h

Premises used: Complex.mem_slitPlane_iff, lt_or_lt_iff_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ∈ slitPlane
h₀ : ‖x‖ ≠ 0
h₁ : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
⊢ ‖x‖ ≠ 0

Tactic:
rw [mem_slitPlane_iff, ← lt_or_lt_iff_ne] at h

Premises used: Complex.mem_slitPlane_iff, lt_or_lt_iff_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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
inr₁ : ∀ (hx_im : 0 < x.im), ContinuousAt arg x
⊢ ContinuousAt arg x

Tactic:
rcases h with (hx_re | hx_im | hx_im)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_re : 0 < x.re
⊢ ContinuousAt arg x

Tactic:
(Real.continuousAt_arcsin.comp
          (continuous_im.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_re_pos hx_re).symm

Premises used: ContinuousAt.congr, Real.continuousAt_arcsin, Continuous.continuousAt, ContinuousAt.comp, ContinuousAt.div, Complex.arg_eq_nhds_of_re_pos, continuous_norm, Filter.EventuallyEq.symm, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_im : x.im < 0
⊢ ContinuousAt arg x

Tactic:
(Real.continuous_arccos.continuousAt.comp
            (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).neg.congr
      (arg_eq_nhds_of_im_neg hx_im).symm

Premises used: Complex.continuous_re, ContinuousAt.congr, Complex.arg_eq_nhds_of_im_neg, ContinuousAt.neg, Continuous.continuousAt, ContinuousAt.comp, ContinuousAt.div, Real.continuous_arccos, continuous_norm, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_im : 0 < x.im
⊢ ContinuousAt arg x

Tactic:
(Real.continuous_arccos.continuousAt.comp
          (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_im_pos hx_im).symm

Premises used: Complex.continuous_re, ContinuousAt.congr, Continuous.continuousAt, ContinuousAt.comp, ContinuousAt.div, Complex.arg_eq_nhds_of_im_pos, Real.continuous_arccos, continuous_norm, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_re : 0 < x.re
⊢ ContinuousAt arg x

Tactic:
exacts [(Real.continuousAt_arcsin.comp
          (continuous_im.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_re_pos hx_re).symm,
    (Real.continuous_arccos.continuousAt.comp
            (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).neg.congr
      (arg_eq_nhds_of_im_neg hx_im).symm,
    (Real.continuous_arccos.continuousAt.comp
          (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_im_pos hx_im).symm]

Premises used: ContinuousAt.congr, Real.continuousAt_arcsin, Continuous.continuousAt, ContinuousAt.comp, ContinuousAt.div, Complex.arg_eq_nhds_of_re_pos, continuous_norm, Filter.EventuallyEq.symm, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ ContinuousOn arg slitPlane

Tactic:
fun _ h ↦ continuousAt_arg h |>.continuousWithinAt

Premises used: Complex.continuousAt_arg, ContinuousAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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) (𝓝 (-π))

Tactic:
H.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
refine : (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z : ℂ | z.im < 0}] z] arg
⊢ Tendsto arg (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))

Tactic:
refine H.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0

Tactic:
have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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
h : ∀ (a : ℂ) (him : a.im < 0) (hre : a.re < 0), Real.arcsin ((-a).im / ‖a‖) - π = a.arg
⊢ (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z : ℂ | z.im < 0}] z] arg

Tactic:
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds this] with _ him hre

Premises used: mem_nhdsWithin_of_mem_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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‖) - π
h₂ h₃ : Real.arcsin ((-a).im / ‖a‖) - π = Real.arcsin ((-a).im / ‖a‖) - π
⊢ Real.arcsin ((-a).im / ‖a‖) - π = a.arg

Tactic:
rw [arg, if_neg hre.not_ge, if_neg him.not_ge]

Premises used: Complex.arg, LT.lt.not_ge, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
suffices : Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
⊢ Tendsto arg (𝓝[{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]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun (x : ℂ) ↦ (Real.arcsin ∘ (im ∘ Neg.neg / fun (a : ℂ) ↦ ‖a‖)) x - π) (𝓝[{z : ℂ | z.im < 0}] z)
    (𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun (a : ℂ) ↦ ‖a‖)) z - π))

Tactic:
(Real.continuousAt_arcsin.comp_continuousWithinAt
          ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
            continuous_norm.continuousWithinAt _)).sub_const
      π

Premises used: Real.pi, Filter.Tendsto.sub_const, continuousWithinAt_neg, Real.continuousAt_arcsin, Continuous.continuousAt, ContinuousAt.comp_continuousWithinAt, ContinuousWithinAt.div, Continuous.continuousWithinAt, continuous_norm, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
h : 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun (a : ℂ) ↦ ‖a‖)) z - π)
convert_3 : ‖z‖ ≠ 0
⊢ Tendsto (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))

Tactic:
convert!
    (Real.continuousAt_arcsin.comp_continuousWithinAt
          ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
            continuous_norm.continuousWithinAt _)).sub_const
      π using 1

Premises used: Real.pi, Filter.Tendsto.sub_const, continuousWithinAt_neg, Real.continuousAt_arcsin, Continuous.continuousAt, ContinuousAt.comp_continuousWithinAt, ContinuousWithinAt.div, Continuous.continuousWithinAt, continuous_norm, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun (a : ℂ) ↦ ‖a‖)) z - π)

Tactic:
simp [him]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ z.im = 0

Tactic:
him
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
convert_3 : ∀ (z : ℝ) (hre : (↑z : ℂ).re < 0), ‖(↑z : ℂ)‖ ≠ 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℝ
hre : (↑z : ℂ).re < 0
⊢ ‖(↑z : ℂ)‖ ≠ 0

Tactic:
simpa using hre.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0

Tactic:
have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)