awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
h : ∀ (a : ℂ) (him : 0 ≤ a.im) (hre : a.re < 0), a.arg = Real.arcsin ((-a).im / ‖a‖) + π
⊢ arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | 0 ≤ z.im }),
      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
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a : ℂ
him : 0 ≤ a.im
hre : a.re < 0
h :
  (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‖) + π
h₁ :
  (if 0 ≤ a.im then Real.arcsin ((-a).im / ‖a‖) + π else Real.arcsin ((-a).im / ‖a‖) - π) =
    Real.arcsin ((-a).im / ‖a‖) + π
h₂ h₃ : Real.arcsin ((-a).im / ‖a‖) + π = Real.arcsin ((-a).im / ‖a‖) + π
⊢ a.arg = Real.arcsin ((-a).im / ‖a‖) + π

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

Premises used: Complex.arg, if_pos, LT.lt.not_ge, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
have : arg =ᶠ[𝓝[{ z : ℂ | 0 ≤ z.im }] z] fun x => Real.arcsin ((-x).im / ‖x‖) + π := by
    have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
    filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | 0 ≤ z.im }),
      mem_nhdsWithin_of_mem_nhds this] with _ him hre
    rw [arg, if_neg hre.not_ge, if_pos him]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ContinuousWithinAt arg {z : ℂ | 0 ≤ z.im} z

Tactic:
ContinuousWithinAt.congr_of_eventuallyEq ?_ this ?_

Premises used: ContinuousWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
refine_1 : ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z : ℂ | 0 ≤ z.im} z
refine_2 : z.arg = Real.arcsin ((-z).im / ‖z‖) + π
⊢ ContinuousWithinAt arg {z : ℂ | 0 ≤ z.im} z

Tactic:
refine ContinuousWithinAt.congr_of_eventuallyEq ?_ this ?_

Premises used: ContinuousWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z : ℂ | 0 ≤ z.im} z

Tactic:
(Real.continuousAt_arcsin.comp_continuousWithinAt
            ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
              continuous_norm.continuousWithinAt ?_)).add
        tendsto_const_nhds

Premises used: Real.arcsin, tendsto_const_nhds, continuousWithinAt_neg, Real.continuousAt_arcsin, Continuous.continuousAt, ContinuousWithinAt.add, 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
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
refine_1 : ‖z‖ ≠ 0
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z : ℂ | 0 ≤ z.im} z

Tactic:
refine
      (Real.continuousAt_arcsin.comp_continuousWithinAt
            ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
              continuous_norm.continuousWithinAt ?_)).add
        tendsto_const_nhds

Premises used: tendsto_const_nhds, continuousWithinAt_neg, Real.continuousAt_arcsin, Continuous.continuousAt, ContinuousWithinAt.add, 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
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.im = 0

Tactic:
him
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
refine_1 :
  ∀ (z : ℝ) (hre : (↑z : ℂ).re < 0)
    (this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] (↑z : ℂ)] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π), ‖(↑z : ℂ)‖ ≠ 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℝ
hre : (↑z : ℂ).re < 0
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] (↑z : ℂ)] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ‖(↑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
this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
refine_2 :
  (if 0 ≤ z.re then Real.arcsin (z.im / ‖z‖)
    else if 0 ≤ z.im then Real.arcsin ((-z).im / ‖z‖) + π else Real.arcsin ((-z).im / ‖z‖) - π) =
    Real.arcsin ((-z).im / ‖z‖) + π
refine_2₁ :
  (if 0 ≤ z.im then Real.arcsin ((-z).im / ‖z‖) + π else Real.arcsin ((-z).im / ‖z‖) - π) =
    Real.arcsin ((-z).im / ‖z‖) + π
refine_2₂ refine_2₃ : Real.arcsin ((-z).im / ‖z‖) + π = Real.arcsin ((-z).im / ‖z‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π

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

Premises used: Eq.ge, Complex.arg, if_pos, LT.lt.not_ge, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z : ℂ | 0 ≤ z.im}] z) (𝓝 π)

Tactic:
simpa only [arg_eq_pi_iff.2 ⟨hre, him⟩] using
    (continuousWithinAt_arg_of_re_neg_of_im_zero hre him).tendsto

Premises used: Iff.mpr, Complex.continuousWithinAt_arg_of_re_neg_of_im_zero, And.intro, ContinuousWithinAt.tendsto, Complex.arg_eq_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
pos : ∀ (hs : x ∈ slitPlane), ContinuousAt (Real.Angle.coe ∘ arg) x
neg : ∀ (hs : x ∉ slitPlane), ContinuousAt (Real.Angle.coe ∘ arg) x
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
by_cases hs : x ∈ slitPlane

Premises used: Complex.slitPlane
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)

Premises used: Complex.continuousAt_arg, Continuous.continuousAt, Real.Angle.continuous_coe, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)

Premises used: Complex.continuousAt_arg, Continuous.continuousAt, Real.Angle.continuous_coe, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
neg : ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg),
      (funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ←
      Function.comp_assoc]

Premises used: Iff.mpr, Function.comp_id, Real.Angle.coe, funext_iff, Function.comp, neg_neg, Complex.arg, id, Eq.symm, Function.comp_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x

Tactic:
ContinuousAt.comp ?_ continuous_neg.continuousAt

Premises used: ContinuousNeg.continuous_neg, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
neg : ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)
⊢ ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x

Tactic:
refine ContinuousAt.comp ?_ continuous_neg.continuousAt

Premises used: ContinuousNeg.continuous_neg, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
this :
  ContinuousAt (Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle))
    (-x)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)), ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)

Tactic:
rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this

Premises used: Iff.mpr, continuousAt_update_of_ne, neg_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
neg :
  ContinuousAt (Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle))
    (-x)
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)

Tactic:
suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by
      rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
rw :
  (↑π : Real.Angle) = (↑(arg 0) : Real.Angle) + (↑π : Real.Angle) ∧
    ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
⊢ Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
rw [Function.update_eq_iff]

Premises used: Function.update_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ (↑π : Real.Angle) = (↑(arg 0) : Real.Angle) + (↑π : Real.Angle)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ (↑π : Real.Angle) = (↑(arg 0) : Real.Angle) + (↑π : Real.Angle) ∧
    ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = (↑x.arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
have ha :
      Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π = fun z =>
        (arg z : Real.Angle) + π := by
      rw [Function.update_eq_iff]
      exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
neg : ContinuousAt (Y := Real.Angle) (fun (z : ℂ) ↦ (↑z.arg : Real.Angle) + (↑π : Real.Angle)) (-x)
⊢ ContinuousAt (Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle))
    (-x)

Tactic:
rw [ha]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
⊢ ¬(0 < x.re ∨ x.im ≠ 0)

Tactic:
replace hs := mem_slitPlane_iff.mpr.mt hs
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ x.re ≤ 0 ∧ x.im = 0

Tactic:
push Not at hs

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
hs : x.re ≤ 0 ∧ x.im = 0
⊢ ContinuousAt (Y := Real.Angle) (fun (z : ℂ) ↦ (↑z.arg : Real.Angle) + (↑π : Real.Angle)) (-x)

Tactic:
(Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl ?_))).add
        continuousAt_const

Premises used: Real.Angle.coe, ContinuousAt.add, Complex.continuousAt_arg, continuousAt_const, Continuous.continuousAt, Real.Angle.continuous_coe, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
hs : x.re ≤ 0 ∧ x.im = 0
neg : 0 < (-x).re
⊢ ContinuousAt (Y := Real.Angle) (fun (z : ℂ) ↦ (↑z.arg : Real.Angle) + (↑π : Real.Angle)) (-x)

Tactic:
refine
      (Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl ?_))).add
        continuousAt_const

Premises used: ContinuousAt.add, Complex.continuousAt_arg, continuousAt_const, Continuous.continuousAt, Real.Angle.continuous_coe, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
hs : x.re ≤ 0 ∧ x.im = 0
neg : x.re < 0
⊢ 0 < (-x).re

Tactic:
rw [neg_re, neg_pos]

Premises used: neg_pos, Complex.neg_re
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0

Tactic:
hs.1.lt_of_ne fun h0 => h (Complex.ext_iff.2 ⟨h0, hs.2⟩)

Premises used: Iff.mpr, Complex.ext_iff, LE.le.lt_of_ne, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x ≠ 0
ha :
  Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle) = fun (z : ℂ) ↦
    (↑z.arg : Real.Angle) + (↑π : Real.Angle)
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0

Tactic:
exact hs.1.lt_of_ne fun h0 => h (Complex.ext_iff.2 ⟨h0, hs.2⟩)

Premises used: Iff.mpr, Complex.ext_iff, LE.le.lt_of_ne, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ Injective (β := ℝ) fun (z : Circle) ↦ (↑z : ℂ).arg

Tactic:
fun z w h =>
  Subtype.ext <| ext_norm_arg (z.norm_coe.trans w.norm_coe.symm) h

Premises used: Circle.norm_coe, Complex.ext_norm_arg, Circle, Function.Injective, Eq.symm, Eq.trans, Subtype.ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
z w : Circle
⊢ (↑z : ℂ).arg = (↑w : ℂ).arg ↔ z = w

Tactic:
injective_arg.eq_iff

Premises used: Circle.injective_arg, Function.Injective.eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
rw : (cexp ((↑x : ℂ) * I)).arg = x
rw₁ : (Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg = x
rw₂ rw₃ : x = x
⊢ arg (↑((exp : (a : ℝ) → Circle) x) : ℂ) = x

Tactic:
rw [coe_exp, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]

Premises used: Complex.arg_cos_add_sin_mul_I, And.intro, Circle.coe_exp, Complex.exp_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
z : Circle
⊢ (exp : (a : ℝ) → Circle) (↑z : ℂ).arg = z

Tactic:
injective_arg <| arg_exp (neg_pi_lt_arg _) (arg_le_pi _)

Premises used: Circle.injective_arg, Complex.arg_le_pi, Complex.neg_pi_lt_arg, Circle.arg_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ LeftInverse (α := Circle) (⇑exp : (a : ℝ) → Circle)
    (arg ∘ Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x))

Tactic:
exp_arg

Premises used: Circle.exp_arg, Function.LeftInverse, Complex.arg, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ InvOn (β := Circle)
    (arg ∘ Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x))
    (⇑exp : (a : ℝ) → Circle) (Ioc (-π) π) univ

Tactic:
argPartialEquiv.symm.invOn

Premises used: Set.Ioc, Set.univ, setOf, PartialEquiv.symm, Complex.arg, Circle.argPartialEquiv, PartialEquiv.invOn, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ SurjOn (β := Circle) (⇑exp : (a : ℝ) → Circle) (Ioc (-π) π) univ

Tactic:
argPartialEquiv.symm.surjOn

Premises used: Set.Ioc, Set.univ, setOf, PartialEquiv.symm, Circle.argPartialEquiv, PartialEquiv.surjOn
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : ℝ
rw : (∃ (n : ℤ), (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (m : ℤ), x = y + (↑m : ℝ) * (2 * π)
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) ((exp : (a : ℝ) → Circle) y : Circle) ↔
    ∃ (m : ℤ), x = y + (↑m : ℝ) * (2 * π)

Tactic:
rw [Subtype.ext_iff, coe_exp, coe_exp, exp_eq_exp_iff_exists_int]

Premises used: Complex.exp_eq_exp_iff_exists_int, Subtype.ext_iff, Circle.coe_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : ℝ
⊢ (∃ (n : ℤ), (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (m : ℤ), x = y + (↑m : ℝ) * (2 * π)

Tactic:
exists_congr fun n => ?_

Premises used: exists_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : ℝ
refine : ∀ (n : ℤ), (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I) ↔ x = y + (↑n : ℝ) * (2 * π)
⊢ (∃ (n : ℤ), (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (m : ℤ), x = y + (↑m : ℝ) * (2 * π)

Tactic:
refine exists_congr fun n => ?_

Premises used: exists_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : ℝ
n : ℤ
rw : (↑x : ℂ) = (↑y : ℂ) + (↑n : ℂ) * (2 * (↑π : ℂ)) ↔ x = y + (↑n : ℝ) * (2 * π)
⊢ (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I) ↔ x = y + (↑n : ℝ) * (2 * π)

Tactic:
rw [← mul_assoc, ← add_mul, mul_left_inj' I_ne_zero]

Premises used: add_mul, mul_assoc, Complex.I_ne_zero, mul_left_inj'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : ℝ
n : ℤ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : x = y + (↑n : ℝ) * (2 * π) ↔ x = y + (↑n : ℝ) * (2 * π)
⊢ (↑x : ℂ) = (↑y : ℂ) + (↑n : ℂ) * (2 * (↑π : ℂ)) ↔ x = y + (↑n : ℝ) * (2 * π)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
z : ℝ
rw : z + 2 * π = z + 1 * (2 * π)
rw₁ rw₂ : z + 2 * π = z + 2 * π
⊢ z + 2 * π = z + (↑1 : ℝ) * (2 * π)

Tactic:
rw [Int.cast_one, one_mul]

Premises used: one_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) (2 * π) : Circle) (1 : Circle)

Tactic:
periodic_exp.eq.trans exp_zero

Premises used: Circle.periodic_exp, Circle.exp_zero, Function.Periodic.eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) ((↑n : ℝ) * (2 * π))) : ℂ) (↑1 : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) (2 * π * (↑n : ℝ)) : Circle) (1 : Circle)

Tactic:
simpa only [mul_comm] using exp_int_mul_two_pi n

Premises used: Circle.exp_int_mul_two_pi, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
r : ℝ
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) r : Circle) (1 : Circle) ↔ ∃ (n : ℤ), r = (↑n : ℝ) * (2 * π)

Tactic:
simp [Circle.ext_iff, Complex.exp_eq_one_iff, ← mul_assoc, Complex.I_ne_zero,
    ← Complex.ofReal_inj]

Premises used: mul_assoc, Circle.ext_iff, Complex.I_ne_zero, Complex.ofReal_inj, Complex.exp_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
r s : ℝ
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) r : Circle) ((exp : (a : ℝ) → Circle) s : Circle) ↔ r ≡ s [PMOD 2 * π]

Tactic:
simp [AddCommGroup.modEq_iff_zsmul', ← exp_eq_one, div_eq_one, eq_comm (a := exp r)]

Premises used: eq_comm, AddCommGroup.modEq_iff_zsmul', div_eq_one, Circle.exp_eq_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) (x - 2 * π) : Circle) ((exp : (a : ℝ) → Circle) x : Circle)

Tactic:
periodic_exp.sub_eq x

Premises used: Circle.periodic_exp, Function.Periodic.sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) (x + 2 * π) : Circle) ((exp : (a : ℝ) → Circle) x : Circle)

Tactic:
periodic_exp x

Premises used: Circle.periodic_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : Eq (α := Circle) ((exp : (a : ℝ) → Circle) t₁ : Circle) ((exp : (a : ℝ) → Circle) t₂ : Circle)
⊢ -2 * π < t₁ - t₂

Tactic:
obtain ⟨h1, h2⟩ := hs t₁ ht₁ t₂ ht₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : Eq (α := Circle) ((exp : (a : ℝ) → Circle) t₁ : Circle) ((exp : (a : ℝ) → Circle) t₂ : Circle)
h1 : -2 * π < t₁ - t₂
⊢ t₁ - t₂ < 2 * π

Tactic:
obtain ⟨h1, h2⟩ := hs t₁ ht₁ t₂ ht₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : Eq (α := Circle) ((exp : (a : ℝ) → Circle) t₁ : Circle) ((exp : (a : ℝ) → Circle) t₂ : Circle)
h1 : -2 * π < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ -(2 * π) < t₁ - t₂

Tactic:
rw [neg_mul] at h1

Premises used: neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : Eq (α := Circle) ((exp : (a : ℝ) → Circle) t₁ : Circle) ((exp : (a : ℝ) → Circle) t₂ : Circle)
h1 : -2 * π < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
h1₁ : -(2 * π) < t₁ - t₂
⊢ t₁ - t₂ < 2 * π

Tactic:
rw [neg_mul] at h1

Premises used: neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : Eq (α := Circle) ((exp : (a : ℝ) → Circle) t₁ : Circle) ((exp : (a : ℝ) → Circle) t₂ : Circle)
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
rw : (cexp ((↑(t₁ - t₂) : ℂ) * I)).re = 1
⊢ t₁ = t₂

Tactic:
rw [← sub_eq_zero, ← cos_eq_one_iff_of_lt_of_lt h1 h2, ← exp_ofReal_mul_I_re]

Premises used: sub_eq_zero, Complex.exp_ofReal_mul_I_re, Real.cos_eq_one_iff_of_lt_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : Eq (α := Circle) ((exp : (a : ℝ) → Circle) t₁ : Circle) ((exp : (a : ℝ) → Circle) t₂ : Circle)
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ cexp ((↑t₁ : ℂ) * I) = cexp ((↑t₂ : ℂ) * I)

Tactic:
replace heq : cexp _ = cexp _ := congrArg Subtype.val heq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : cexp ((↑t₁ : ℂ) * I) = cexp ((↑t₂ : ℂ) * I)
⊢ (cexp ((↑(t₁ - t₂) : ℂ) * I)).re = re 1 ∧ (cexp ((↑(t₁ - t₂) : ℂ) * I)).im = im 1

Tactic:
rw [exp_eq_exp_iff_exp_sub_eq_one, ← sub_mul, ← ofReal_sub, Complex.ext_iff] at heq

Premises used: Complex.exp_eq_exp_iff_exp_sub_eq_one, Complex.ext_iff, sub_mul, Complex.ofReal_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : (cexp ((↑(t₁ - t₂) : ℂ) * I)).re = re 1 ∧ (cexp ((↑(t₁ - t₂) : ℂ) * I)).im = im 1
⊢ (cexp ((↑(t₁ - t₂) : ℂ) * I)).re = 1

Tactic:
heq.1

Premises used: And.left