awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π
have h : ∀ (a : ℂ) (him : 0 ≤ a.im) (hre : a.re < 0), a.arg = Real.arcsin ((-a).im / ‖a‖) + π
Tactic: filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | 0 ≤ z.im }),
      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
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a : ℂ
him : 0 ≤ a.im
hre : a.re < 0
⊢ a.arg = Real.arcsin ((-a).im / ‖a‖) + π
have 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‖) + π
Tactic: rw [arg, if_neg hre.not_ge, if_pos him]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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‖) + π
⊢ a.arg = Real.arcsin ((-a).im / ‖a‖) + π
have h₁ : (if 0 ≤ a.im then Real.arcsin ((-a).im / ‖a‖) + π else Real.arcsin ((-a).im / ‖a‖) - π) =
  Real.arcsin ((-a).im / ‖a‖) + π
Tactic: rw [arg, if_neg hre.not_ge, if_pos him]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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‖) + π
⊢ a.arg = Real.arcsin ((-a).im / ‖a‖) + π
have h₂ : Real.arcsin ((-a).im / ‖a‖) + π = Real.arcsin ((-a).im / ‖a‖) + π
Tactic: rw [arg, if_neg hre.not_ge, if_pos him]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt arg {z : ℂ | 0 ≤ z.im} z
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
have refine_1 : ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z : ℂ | 0 ≤ z.im} z
Tactic: refine ContinuousWithinAt.congr_of_eventuallyEq ?_ this ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ ContinuousWithinAt arg {z : ℂ | 0 ≤ z.im} z
have refine_2 : z.arg = Real.arcsin ((-z).im / ‖z‖) + π
Tactic: refine ContinuousWithinAt.congr_of_eventuallyEq ?_ this ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
have refine_1 : ‖z‖ ≠ 0
Tactic: refine
      (Real.continuousAt_arcsin.comp_continuousWithinAt
            ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
              continuous_norm.continuousWithinAt ?_)).add
        tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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‖ ≠ 0
have refine_1 : ∀ (z : ℝ) (hre : (↑z : ℂ).re < 0)
  (this : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] (↑z : ℂ)] fun (x : ℂ) ↦ Real.arcsin ((-x).im / ‖x‖) + π), ‖(↑z : ℂ)‖ ≠ 0
Tactic: lift z to ℝ using him
Cleared hypotheses: z, hre, him, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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.arg = Real.arcsin ((-z).im / ‖z‖) + π
have 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‖) + π
Tactic: rw [arg, if_neg hre.not_ge, if_pos him.ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π
have refine_2₁ : (if 0 ≤ z.im then Real.arcsin ((-z).im / ‖z‖) + π else Real.arcsin ((-z).im / ‖z‖) - π) =
  Real.arcsin ((-z).im / ‖z‖) + π
Tactic: rw [arg, if_neg hre.not_ge, if_pos him.ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π
have refine_2₂ : Real.arcsin ((-z).im / ‖z‖) + π = Real.arcsin ((-z).im / ‖z‖) + π
Tactic: rw [arg, if_neg hre.not_ge, if_pos him.ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : x ≠ 0
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x
have pos : ∀ (hs : x ∈ slitPlane), ContinuousAt (Real.Angle.coe ∘ arg) x
Tactic: by_cases hs : x ∈ slitPlane
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : x ≠ 0
pos : ∀ (hs : x ∈ slitPlane), ContinuousAt (Real.Angle.coe ∘ arg) x
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x
have neg : ∀ (hs : x ∉ slitPlane), ContinuousAt (Real.Angle.coe ∘ arg) x
Tactic: by_cases hs : x ∈ slitPlane
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x
have neg : ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x
Tactic: rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg),
      (funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ←
      Function.comp_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x
have neg : ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)
Tactic: refine ContinuousAt.comp ?_ continuous_neg.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)
have rwa : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)
have neg : ContinuousAt (Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle))
  (-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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
have 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)
Tactic: rw [Function.update_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle))
    (-x)
have ha : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ ContinuousAt (Function.update (β := fun (a : ℂ) ↦ Real.Angle) ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 (↑π : Real.Angle))
    (-x)
have neg : ContinuousAt (Y := Real.Angle) (fun (z : ℂ) ↦ (↑z.arg : Real.Angle) + (↑π : Real.Angle)) (-x)
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
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)
⊢ ContinuousAt (Y := Real.Angle) (fun (z : ℂ) ↦ (↑z.arg : Real.Angle) + (↑π : Real.Angle)) (-x)
have hs₁ : ¬(0 < x.re ∨ x.im ≠ 0)
Tactic: replace hs := mem_slitPlane_iff.mpr.mt hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
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)
⊢ ContinuousAt (Y := Real.Angle) (fun (z : ℂ) ↦ (↑z.arg : Real.Angle) + (↑π : Real.Angle)) (-x)
have hs₁ : x.re ≤ 0 ∧ x.im = 0
Tactic: push Not at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
have neg : 0 < (-x).re
Tactic: refine
      (Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl ?_))).add
        continuousAt_const
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ 0 < (-x).re
have neg : x.re < 0
Tactic: rw [neg_re, neg_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
⊢ arg (↑((exp : (a : ℝ) → Circle) x) : ℂ) = x
have rw : (cexp ((↑x : ℂ) * I)).arg = x
Tactic: rw [coe_exp, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
rw : (cexp ((↑x : ℂ) * I)).arg = x
⊢ arg (↑((exp : (a : ℝ) → Circle) x) : ℂ) = x
have rw₁ : (Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg = x
Tactic: rw [coe_exp, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
rw : (cexp ((↑x : ℂ) * I)).arg = x
rw₁ : (Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg = x
⊢ arg (↑((exp : (a : ℝ) → Circle) x) : ℂ) = x
have rw₂ : x = x
Tactic: rw [coe_exp, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : ℝ
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) ((exp : (a : ℝ) → Circle) y : Circle) ↔
    ∃ (m : ℤ), x = y + (↑m : ℝ) * (2 * π)
have rw : (∃ (n : ℤ), (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (m : ℤ), x = y + (↑m : ℝ) * (2 * π)
Tactic: rw [Subtype.ext_iff, coe_exp, coe_exp, exp_eq_exp_iff_exists_int]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : ℝ
⊢ (∃ (n : ℤ), (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (m : ℤ), x = y + (↑m : ℝ) * (2 * π)
have refine : ∀ (n : ℤ), (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I) ↔ x = y + (↑n : ℝ) * (2 * π)
Tactic: refine exists_congr fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : ℝ
n : ℤ
⊢ (↑x : ℂ) * I = (↑y : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I) ↔ x = y + (↑n : ℝ) * (2 * π)
have rw : (↑x : ℂ) = (↑y : ℂ) + (↑n : ℂ) * (2 * (↑π : ℂ)) ↔ x = y + (↑n : ℝ) * (2 * π)
Tactic: rw [← mul_assoc, ← add_mul, mul_left_inj' I_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : ℝ
n : ℤ
⊢ (↑x : ℂ) = (↑y : ℂ) + (↑n : ℂ) * (2 * (↑π : ℂ)) ↔ x = y + (↑n : ℝ) * (2 * π)
have norm_cast : x = y + (↑n : ℝ) * (2 * π) ↔ x = y + (↑n : ℝ) * (2 * π)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
z : ℝ
⊢ z + 2 * π = z + (↑1 : ℝ) * (2 * π)
have rw : z + 2 * π = z + 1 * (2 * π)
Tactic: rw [Int.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
z : ℝ
rw : z + 2 * π = z + 1 * (2 * π)
⊢ z + 2 * π = z + (↑1 : ℝ) * (2 * π)
have rw₁ : z + 2 * π = z + 2 * π
Tactic: rw [Int.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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)
⊢ t₁ = t₂
have h1 : -2 * π < t₁ - t₂
Tactic: obtain ⟨h1, h2⟩ := hs t₁ ht₁ t₂ ht₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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₂
have h2 : t₁ - t₂ < 2 * π
Tactic: obtain ⟨h1, h2⟩ := hs t₁ ht₁ t₂ ht₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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 * π
⊢ t₁ = t₂
have h1₁ : -(2 * π) < t₁ - t₂
Tactic: rw [neg_mul] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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 * π
⊢ t₁ = t₂
have rw : (cexp ((↑(t₁ - t₂) : ℂ) * I)).re = 1
Tactic: rw [← sub_eq_zero, ← cos_eq_one_iff_of_lt_of_lt h1 h2, ← exp_ofReal_mul_I_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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₁ - t₂) : ℂ) * I)).re = 1
have heq₁ : cexp ((↑t₁ : ℂ) * I) = cexp ((↑t₂ : ℂ) * I)
Tactic: replace heq : cexp _ = cexp _ := congrArg Subtype.val heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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 = 1
have heq₁ : (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
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a < 2 * π
x : ℝ
h_1 : x ∈ Icc a b
y : ℝ
h_2 : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ x - y ∈ Ioo (-2 * π) (2 * π)
have left : -2 * π < x - y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a < 2 * π
x : ℝ
h_1 : x ∈ Icc a b
y : ℝ
h_2 : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
left : -2 * π < x - y
⊢ x - y ∈ Ioo (-2 * π) (2 * π)
have right : x - y < 2 * π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a < 2 * π
x : ℝ
h_1 : x ∈ Icc a b
y : ℝ
h_2 : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ -2 * π < x - y
have linarith : x - y ≤ -2 * π → b - a - 2 * π + (a - x) + (y - b) + (x - y - -2 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a < 2 * π
x : ℝ
h_1 : x ∈ Icc a b
y : ℝ
h_2 : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ x - y < 2 * π
have linarith : 2 * π ≤ x - y → b - a - 2 * π + (x - b) + (a - y) + (2 * π - (x - y)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ico a b
y : ℝ
h_2 : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ x - y ∈ Ioo (-2 * π) (2 * π)
have left : -2 * π < x - y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ico a b
y : ℝ
h_2 : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
left : -2 * π < x - y
⊢ x - y ∈ Ioo (-2 * π) (2 * π)
have right : x - y < 2 * π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ico a b
y : ℝ
h_2 : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ -2 * π < x - y
have linarith : x - y ≤ -2 * π → b - a - 2 * π + (a - x) + (y - b) + (x - y - -2 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ico a b
y : ℝ
h_2 : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ x - y < 2 * π
have linarith : 2 * π ≤ x - y → b - a - 2 * π + (x - b) + (a - y) + (2 * π - (x - y)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ioc a b
y : ℝ
h_2 : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ x - y ∈ Ioo (-2 * π) (2 * π)
have left : -2 * π < x - y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ioc a b
y : ℝ
h_2 : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
left : -2 * π < x - y
⊢ x - y ∈ Ioo (-2 * π) (2 * π)
have right : x - y < 2 * π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ioc a b
y : ℝ
h_2 : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ -2 * π < x - y
have linarith : x - y ≤ -2 * π → b - a - 2 * π + (a - x) + (y - b) + (x - y - -2 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ioc a b
y : ℝ
h_2 : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ x - y < 2 * π
have linarith : 2 * π ≤ x - y → b - a - 2 * π + (x - b) + (a - y) + (2 * π - (x - y)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
⊢ HMul.hMul (α := Circle) ((exp : (a : ℝ) → Circle) (x.angleDiff y) : Circle) x = y
have rw : (exp : (a : ℝ) → Circle)
    ((if arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg then
        (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)
      else 2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)) +
      (↑x : ℂ).arg) =
  y
Tactic: rw [← exp_arg x, ← exp_add, angleDiff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
⊢ (exp : (a : ℝ) → Circle)
      ((if arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg then
          (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)
        else 2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)) +
        (↑x : ℂ).arg) =
    y
have pos : ∀ (hxy : arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg),
  (exp : (a : ℝ) → Circle) ((↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) + (↑x : ℂ).arg) = y
Tactic: split_ifs with hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
pos :
  ∀ (hxy : arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg),
    (exp : (a : ℝ) → Circle) ((↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) + (↑x : ℂ).arg) = y
⊢ (exp : (a : ℝ) → Circle)
      ((if arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg then
          (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)
        else 2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)) +
        (↑x : ℂ).arg) =
    y
have neg : ∀ (hxy : ¬arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg),
  (exp : (a : ℝ) → Circle) (2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) + (↑x : ℂ).arg) =
    y
Tactic: split_ifs with hxy