awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
⊢ HasEnoughRootsOfUnity Circle n

Tactic:
(rootsOfUnityCircleEquiv n).symm.hasEnoughRootsOfUnity

Premises used: MulEquiv.hasEnoughRootsOfUnity, rootsOfUnityCircleEquiv, MulEquiv.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
w : ↥(rootsOfUnity n Circle)
⊢ (↑(↑((rootsOfUnityCircleEquiv n : (a : ↥(rootsOfUnity n Circle)) → ↥(rootsOfUnity n ℂ)) w) : ℂˣ) : ℂ) =
    (↑(↑(↑w : Circleˣ) : Circle) : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
j : ZMod n
⊢ (↑(↑((rootsOfUnityCircleEquiv n : (a : ↥(rootsOfUnity n Circle)) → ↥(rootsOfUnity n ℂ))
              ((ZMod.rootsOfUnityAddChar n : (a : ZMod n) → ↥(rootsOfUnity n Circle)) j)) :
          ℂˣ) :
      ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑n : ℂ))

Tactic:
simp [← ZMod.toCircle_natCast, -ZMod.natCast_val, ZMod.natCast_zmod_val]

Premises used: ZMod.natCast_val, ZMod.natCast_zmod_val, ZMod.toCircle_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
x : ↥(rootsOfUnity n ℂ)
w : ℂˣ
hw : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) w
obtain :
  ∀ (j : ℕ) (hj1 : j < n) (hj2 : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑j : ℂ) (↑n : ℂ)) = (↑w : ℂ)),
    ∃ (a : ZMod n),
      comp (β := ↥(rootsOfUnity n Circle))
          (⇑(rootsOfUnityCircleEquiv n) : (a : ↥(rootsOfUnity n Circle)) → ↥(rootsOfUnity n ℂ))
          (⇑(ZMod.rootsOfUnityAddChar n) : (a : ZMod n) → ↥(rootsOfUnity n Circle)) a =
        Subtype.mk (p := fun (x : ℂˣ) ↦ Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) x) w hw
⊢ ∃ (a : ZMod n),
    comp (β := ↥(rootsOfUnity n Circle))
        (⇑(rootsOfUnityCircleEquiv n) : (a : ↥(rootsOfUnity n Circle)) → ↥(rootsOfUnity n ℂ))
        (⇑(ZMod.rootsOfUnityAddChar n) : (a : ZMod n) → ↥(rootsOfUnity n Circle)) a =
      Subtype.mk (p := fun (x : ℂˣ) ↦ Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) x) w hw

Tactic:
obtain ⟨j, hj1, hj2⟩ := (Complex.mem_rootsOfUnity n w).mp hw

Premises used: Complex.mem_rootsOfUnity, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
x : ↥(rootsOfUnity n ℂ)
w : ℂˣ
hw : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) w
j : ℕ
hj1 : j < n
hj2 : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑j : ℂ) (↑n : ℂ)) = (↑w : ℂ)
⊢ comp (α := ZMod n) (β := ↥(rootsOfUnity n Circle))
      (⇑(rootsOfUnityCircleEquiv n) : (a : ↥(rootsOfUnity n Circle)) → ↥(rootsOfUnity n ℂ))
      (⇑(ZMod.rootsOfUnityAddChar n) : (a : ZMod n) → ↥(rootsOfUnity n Circle)) (↑j : ZMod n) =
    Subtype.mk (p := fun (x : ℂˣ) ↦ Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) x) w hw

Tactic:
simp [Units.ext_iff, Subtype.ext_iff, ← hj2, ZMod.toCircle_natCast, mul_div_assoc]

Premises used: Units.ext_iff, mul_div_assoc, Subtype.ext_iff, ZMod.toCircle_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
x : ↥(rootsOfUnity n ℂ)
w : ℂˣ
hw : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) w
j : ℕ
hj1 : j < n
hj2 : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑j : ℂ) (↑n : ℂ)) = (↑w : ℂ)
⊢ ∃ (a : ZMod n),
    comp (β := ↥(rootsOfUnity n Circle))
        (⇑(rootsOfUnityCircleEquiv n) : (a : ↥(rootsOfUnity n Circle)) → ↥(rootsOfUnity n ℂ))
        (⇑(ZMod.rootsOfUnityAddChar n) : (a : ZMod n) → ↥(rootsOfUnity n Circle)) a =
      Subtype.mk (p := fun (x : ℂˣ) ↦ Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) x) w hw

Tactic:
exact ⟨j, by simp [Units.ext_iff, Subtype.ext_iff, ← hj2, ZMod.toCircle_natCast, mul_div_assoc]⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
x x_1 : ZMod n
⊢ Eq (α := ↥(rootsOfUnity n Circle))
      ((ZMod.rootsOfUnityAddChar n : (a : ZMod n) → ↥(rootsOfUnity n Circle)) x : ↥(rootsOfUnity n Circle))
      ((ZMod.rootsOfUnityAddChar n : (a : ZMod n) → ↥(rootsOfUnity n Circle)) x_1 : ↥(rootsOfUnity n Circle)) →
    x = x_1

Tactic:
simp [ZMod.rootsOfUnityAddChar, ZMod.injective_toCircle.eq_iff]

Premises used: ZMod.rootsOfUnityAddChar, Function.Injective.eq_iff, ZMod.injective_toCircle
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ - c = circleMap 0 R θ

Tactic:
simp [circleMap]

Premises used: circleMap
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
R θ : ℝ
⊢ circleMap 0 R θ = (↑R : ℂ) * cexp ((↑θ : ℂ) * I)

Tactic:
zero_add _

Premises used: circleMap, zero_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
R θ : ℝ
⊢ ‖circleMap 0 R θ‖ = |R|

Tactic:
simp [circleMap]

Premises used: circleMap
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ ∉ ball c R

Tactic:
simp [Complex.dist_eq, le_abs_self]

Premises used: le_abs_self, Complex.dist_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R : ℝ
w : ℂ
hw : w ∈ ball c R
θ : ℝ
⊢ circleMap c R θ ≠ w

Tactic:
(ne_of_mem_of_not_mem hw (circleMap_notMem_ball _ _ _)).symm

Premises used: circleMap_notMem_ball, Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ ∈ sphere c |R|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R : ℝ
hR : 0 ≤ R
θ : ℝ
⊢ circleMap c R θ ∈ sphere c R

Tactic:
simpa only [abs_of_nonneg hR] using circleMap_mem_sphere' c R θ

Premises used: abs_of_nonneg, circleMap_mem_sphere'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R : ℝ
hR : 0 ≤ R
θ : ℝ
⊢ circleMap c R θ ∈ closedBall c R

Tactic:
sphere_subset_closedBall (circleMap_mem_sphere c hR θ)

Premises used: circleMap_mem_sphere, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ = c ↔ R = 0

Tactic:
simp [circleMap, Complex.exp_ne_zero]

Premises used: Complex.exp_ne_zero, circleMap
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
⊢ circleMap c 0 = const ℝ c

Tactic:
funext fun _ => circleMap_eq_center_iff.2 rfl

Premises used: Iff.mpr, funext, circleMap_eq_center_iff, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
θ : ℝ
⊢ circleMap c R θ ≠ c

Tactic:
mt circleMap_eq_center_iff.1 hR

Premises used: mt, circleMap_eq_center_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
R₁ R₂ θ₁ θ₂ : ℝ
simp :
  (↑R₁ : ℂ) * cexp ((↑θ₁ : ℂ) * I) * ((↑R₂ : ℂ) * cexp ((↑θ₂ : ℂ) * I)) =
    (↑R₁ : ℂ) * (↑R₂ : ℂ) * (cexp ((↑θ₁ : ℂ) * I) * cexp ((↑θ₂ : ℂ) * I))
⊢ circleMap 0 R₁ θ₁ * circleMap 0 R₂ θ₂ = circleMap 0 (R₁ * R₂) (θ₁ + θ₂)

Tactic:
simp only [circleMap_zero, ofReal_mul, ofReal_add, add_mul, Complex.exp_add]

Premises used: add_mul, Complex.exp_add, Complex.ofReal_add, circleMap_zero, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
R₁ R₂ θ₁ θ₂ : ℝ
⊢ (↑R₁ : ℂ) * cexp ((↑θ₁ : ℂ) * I) * ((↑R₂ : ℂ) * cexp ((↑θ₂ : ℂ) * I)) =
    (↑R₁ : ℂ) * (↑R₂ : ℂ) * (cexp ((↑θ₁ : ℂ) * I) * cexp ((↑θ₂ : ℂ) * I))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
R₁ R₂ θ₁ θ₂ : ℝ
simp :
  (↑R₁ : ℂ) * cexp ((↑θ₁ : ℂ) * I) / ((↑R₂ : ℂ) * cexp ((↑θ₂ : ℂ) * I)) =
    (↑R₁ : ℂ) / (↑R₂ : ℂ) * (cexp ((↑θ₁ : ℂ) * I) / cexp ((↑θ₂ : ℂ) * I))
⊢ circleMap 0 R₁ θ₁ / circleMap 0 R₂ θ₂ = circleMap 0 (R₁ / R₂) (θ₁ - θ₂)

Tactic:
simp only [circleMap_zero, ofReal_div, ofReal_sub, sub_mul, Complex.exp_sub]

Premises used: circleMap_zero, sub_mul, Complex.ofReal_div, Complex.ofReal_sub, Complex.exp_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
R₁ R₂ θ₁ θ₂ : ℝ
⊢ (↑R₁ : ℂ) * cexp ((↑θ₁ : ℂ) * I) / ((↑R₂ : ℂ) * cexp ((↑θ₂ : ℂ) * I)) =
    (↑R₁ : ℂ) / (↑R₂ : ℂ) * (cexp ((↑θ₁ : ℂ) * I) / cexp ((↑θ₂ : ℂ) * I))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
R θ : ℝ
⊢ (circleMap 0 R θ)⁻¹ = circleMap 0 R⁻¹ (-θ)

Tactic:
simp [circleMap_zero, Complex.exp_neg, mul_comm]

Premises used: Complex.exp_neg, circleMap_zero, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
n : ℕ
R θ : ℝ
⊢ circleMap 0 R θ ^ n = circleMap 0 (R ^ n) ((↑n : ℝ) * θ)

Tactic:
simp [circleMap_zero, mul_pow, ← Complex.exp_nat_mul, ← mul_assoc]

Premises used: mul_assoc, circleMap_zero, Complex.exp_nat_mul, mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
n : ℤ
R θ : ℝ
⊢ circleMap 0 R θ ^ n = circleMap 0 (R ^ n) ((↑n : ℝ) * θ)

Tactic:
simp [circleMap_zero, mul_zpow, ← exp_int_mul, ← mul_assoc]

Premises used: mul_assoc, mul_zpow, circleMap_zero, Complex.exp_int_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
r θ : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (circleMap 0 r θ) = circleMap 0 r (-θ)

Tactic:
simp [circleMap_zero, ← exp_conj]

Premises used: circleMap_zero, Complex.exp_conj
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
r θ : ℝ
⊢ Eq (α := ℂ)
    ((fun (a : ℂ) ↦ HSub.hSub (β := ℂ) a ((starRingEnd ℂ : (a : ℂ) → ℂ) c : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (circleMap c r θ)))
    ((fun (a : ℂ) ↦ HSub.hSub (β := ℂ) a ((starRingEnd ℂ : (a : ℂ) → ℂ) c : ℂ))
      (circleMap ((starRingEnd ℂ : (a : ℂ) → ℂ) c) r (-θ)))

Tactic:
simp [← map_sub, conj_circleMap_zero]

Premises used: map_sub, conj_circleMap_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
r θ : ℝ
⊢ (circleMap 0 r θ).re = r * Real.cos θ

Tactic:
simp [circleMap_zero]

Premises used: circleMap_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
r θ : ℝ
⊢ (circleMap 0 r θ).im = r * Real.sin θ

Tactic:
simp [circleMap_zero]

Premises used: circleMap_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R : ℝ
⊢ circleMap c R (π / 2) = c + (↑R : ℂ) * I

Tactic:
simp only [circleMap, ofReal_div, ofReal_ofNat, exp_pi_div_two_mul_I]

Premises used: circleMap, Complex.exp_pi_div_two_mul_I, Complex.ofReal_div, Complex.ofReal_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R : ℝ
⊢ circleMap c R (-π / 2) = c - (↑R : ℂ) * I

Tactic:
simp only [circleMap, ofReal_div, ofReal_neg, ofReal_ofNat, exp_neg_pi_div_two_mul_I, mul_neg,
    sub_eq_add_neg]

Premises used: sub_eq_add_neg, Complex.ofReal_neg, Complex.exp_neg_pi_div_two_mul_I, circleMap, Complex.ofReal_div, Complex.ofReal_ofNat, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
c : ℂ
R θ : ℝ
⊢ circleMap c R (θ + 2 * π) = circleMap c R θ

Tactic:
simp [circleMap, add_mul, exp_periodic _]

Premises used: add_mul, Complex.exp_periodic, circleMap
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
s : Set ℂ
hs : s.Countable
c : ℂ
R : ℝ
hR : R ≠ 0
⊢ (circleMap c R ⁻¹' s).Countable

Tactic:
show (((↑) : ℝ → ℂ) ⁻¹' ((· * I) ⁻¹'
      (exp ⁻¹' ((R * ·) ⁻¹' ((c + ·) ⁻¹' s))))).Countable from
    (((hs.preimage (add_right_injective _)).preimage <|
      mul_right_injective₀ <| ofReal_ne_zero.2 hR).preimage_cexp.preimage <|
        mul_left_injective₀ I_ne_zero).preimage ofReal_injective

Premises used: Iff.mpr, Set.Mem, mul_left_injective₀, add_right_injective, setOf, mul_right_injective₀, Complex.ofReal_ne_zero, circleMap, Complex.I_ne_zero, Set.preimage, Complex.ofReal_injective, Set.Countable.preimage_cexp, Set.Countable.preimage
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
⊢ circleMap c R a = circleMap c R b ↔ (cexp ((↑a : ℂ) * I)).arg = (cexp ((↑b : ℂ) * I)).arg

Tactic:
simp [circleMap, ext_norm_arg_iff, h_R]

Premises used: circleMap, Complex.ext_norm_arg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
⊢ circleMap c R a = circleMap c R b ↔ (cexp ((↑a : ℂ) * I)).arg = (cexp ((↑b : ℂ) * I)).arg

Tactic:
have : circleMap c R a = circleMap c R b ↔ (exp (a * I)).arg = (exp (b * I)).arg := by
    simp [circleMap, ext_norm_arg_iff, h_R]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
this : circleMap c R a = circleMap c R b ↔ (cexp ((↑a : ℂ) * I)).arg = (cexp ((↑b : ℂ) * I)).arg
⊢ circleMap c R a = circleMap c R b ↔ ∃ (n : ℤ), (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
simp [this, arg_eq_arg_iff, exp_eq_exp_iff_exists_int]

Premises used: Complex.exp_eq_exp_iff_exists_int, Complex.arg_eq_arg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
h : circleMap c R a = circleMap c R b
⊢ ∃ (n : ℤ), (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rw [circleMap_eq_circleMap_iff c h_R] at h

Premises used: circleMap_eq_circleMap_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
h : ∃ (n : ℤ), (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
obtain : ∀ (n : ℤ) (hn : (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)), a = b
⊢ a = b

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
n : ℤ
hn : (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (↑n : ℂ) * (2 * (↑π : ℂ) * I) = HMul.hMul (α := ℂ) (↑n : ℂ) 2 * (↑π : ℂ) * I

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
n : ℤ
hn : (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (↑a : ℂ) = (↑b : ℂ) + HMul.hMul (α := ℂ) (↑n : ℂ) 2 * (↑π : ℂ)

Tactic:
simp only [show n * (2 * π * I) = (n * 2 * π) * I by ring, ← add_mul, mul_eq_mul_right_iff,
    I_ne_zero, or_false] at hn

Premises used: add_mul, Complex.I_ne_zero, mul_eq_mul_right_iff, or_false
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
n : ℤ
hn : (↑a : ℂ) = (↑b : ℂ) + HMul.hMul (α := ℂ) (↑n : ℂ) 2 * (↑π : ℂ)
⊢ a = b + (↑(n * 2) : ℝ) * π

Tactic:
norm_cast at hn
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
n : ℤ
hn : a = b + (↑(n * 2) : ℝ) * π
⊢ |(↑n : ℝ)| * (2 * π) < 2 * π

Tactic:
simp only [hn, Int.cast_mul, Int.cast_ofNat, mul_assoc, add_sub_cancel_left, abs_mul,
    Nat.abs_ofNat, abs_of_pos Real.pi_pos] at h_dist

Premises used: add_sub_cancel_left, mul_assoc, abs_mul, Real.pi_pos, Int.cast_ofNat, Int.cast_mul, Nat.abs_ofNat, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
n : ℤ
hn : a = b + (↑(n * 2) : ℝ) * π
h_dist : |(↑n : ℝ)| * (2 * π) < 2 * π
⊢ LT.lt (α := ℝ) |(↑n : ℝ)| 1

Tactic:
simp (disch := positivity) at h_dist
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
n : ℤ
hn : a = b + (↑(n * 2) : ℝ) * π
h_dist : LT.lt (α := ℝ) |(↑n : ℝ)| 1
⊢ |n| < 1

Tactic:
norm_cast at h_dist
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
n : ℤ
hn : a = b + (↑(n * 2) : ℝ) * π
h_dist : |n| < 1
⊢ a = b

Tactic:
simp [hn, Int.abs_lt_one_iff.mp h_dist]

Premises used: Iff.mp, Int.abs_lt_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : |a - b| ≤ 2 * π
x₁ : ℝ
left : min a b < x₁
right : x₁ ≤ max a b
x₂ : ℝ
left_1 : min a b < x₂
right_1 : x₂ ≤ max a b
h : circleMap c R x₁ = circleMap c R x₂
apply : |x₁ - x₂| < 2 * π
⊢ x₁ = x₂

Tactic:
apply eq_of_circleMap_eq h_R _ h

Premises used: eq_of_circleMap_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : |a - b| ≤ 2 * π
x₁ : ℝ
left : min a b < x₁
right : x₁ ≤ max a b
x₂ : ℝ
left_1 : min a b < x₂
right_1 : x₂ ≤ max a b
h : circleMap c R x₁ = circleMap c R x₂
rw : -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
⊢ |x₁ - x₂| < 2 * π

Tactic:
rw [abs_lt]

Premises used: abs_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : |a - b| ≤ 2 * π
x₁ : ℝ
left_1 : min a b < x₁
right_1 : x₁ ≤ max a b
x₂ : ℝ
left_2 : min a b < x₂
right_2 : x₂ ≤ max a b
h : circleMap c R x₁ = circleMap c R x₂
left : -(2 * π) < x₁ - x₂
right : x₁ - x₂ < 2 * π
⊢ -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : |a - b| ≤ 2 * π
x₁ : ℝ
left : min a b < x₁
right : x₁ ≤ max a b
x₂ : ℝ
left_1 : min a b < x₂
right_1 : x₂ ≤ max a b
h : circleMap c R x₁ = circleMap c R x₂
linarith :
  x₁ - x₂ ≤ -(2 * π) →
    |a - b| - 2 * π + (min a b - x₁) + (x₂ - max a b) + (x₁ - x₂ - -(2 * π)) + (max a b - min a b - |a - b|) = 0
⊢ -(2 * π) < x₁ - x₂

Tactic:
linarith [max_sub_min_eq_abs' a b]

Premises used: max_sub_min_eq_abs'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : |a - b| ≤ 2 * π
x₁ : ℝ
left : min a b < x₁
right : x₁ ≤ max a b
x₂ : ℝ
left_1 : min a b < x₂
right_1 : x₂ ≤ max a b
h : circleMap c R x₁ = circleMap c R x₂
linarith :
  2 * π ≤ x₁ - x₂ →
    |a - b| - 2 * π + (x₁ - max a b) + (min a b - x₂) + (2 * π - (x₁ - x₂)) + (max a b - min a b - |a - b|) = 0
⊢ x₁ - x₂ < 2 * π

Tactic:
linarith [max_sub_min_eq_abs' a b]

Premises used: max_sub_min_eq_abs'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : b - a ≤ 2 * π
x₁ : ℝ
left : a ≤ x₁
right : x₁ < b
x₂ : ℝ
left_1 : a ≤ x₂
right_1 : x₂ < b
h : circleMap c R x₁ = circleMap c R x₂
apply : |x₁ - x₂| < 2 * π
⊢ x₁ = x₂

Tactic:
apply eq_of_circleMap_eq h_R _ h

Premises used: eq_of_circleMap_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : b - a ≤ 2 * π
x₁ : ℝ
left : a ≤ x₁
right : x₁ < b
x₂ : ℝ
left_1 : a ≤ x₂
right_1 : x₂ < b
h : circleMap c R x₁ = circleMap c R x₂
rw : -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
⊢ |x₁ - x₂| < 2 * π

Tactic:
rw [abs_lt]

Premises used: abs_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : b - a ≤ 2 * π
x₁ : ℝ
left_1 : a ≤ x₁
right_1 : x₁ < b
x₂ : ℝ
left_2 : a ≤ x₂
right_2 : x₂ < b
h : circleMap c R x₁ = circleMap c R x₂
left : -(2 * π) < x₁ - x₂
right : x₁ - x₂ < 2 * π
⊢ -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : b - a ≤ 2 * π
x₁ : ℝ
left : a ≤ x₁
right : x₁ < b
x₂ : ℝ
left_1 : a ≤ x₂
right_1 : x₂ < b
h : circleMap c R x₁ = circleMap c R x₂
linarith : x₁ - x₂ ≤ -(2 * π) → b - a - 2 * π + (a - x₁) + (x₂ - b) + (x₁ - x₂ - -(2 * π)) = 0
⊢ -(2 * π) < x₁ - x₂

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : b - a ≤ 2 * π
x₁ : ℝ
left : a ≤ x₁
right : x₁ < b
x₂ : ℝ
left_1 : a ≤ x₂
right_1 : x₂ < b
h : circleMap c R x₁ = circleMap c R x₂
linarith : 2 * π ≤ x₁ - x₂ → b - a - 2 * π + (x₁ - b) + (a - x₂) + (2 * π - (x₁ - x₂)) = 0
⊢ x₁ - x₂ < 2 * π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ (log x).re = Real.log ‖x‖

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ (log x).im = x.arg

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ -π < (log x).im

Tactic:
simp only [log_im, neg_pi_lt_arg]

Premises used: Complex.neg_pi_lt_arg, Complex.log_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ (log x).im ≤ π

Tactic:
simp only [log_im, arg_le_pi]

Premises used: Complex.arg_le_pi, Complex.log_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₉ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₁₀ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
rw₁₁ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
rw₁₂ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ)) * I = x
rw₁₃ : (↑x.re : ℂ) + (↑x.im : ℂ) * I = x
rw₁₄ rw₁₅ : x = x
⊢ cexp (log x) = x

Tactic:
rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]

Premises used: Iff.mpr, Complex.log, norm_pos_iff, Complex.exp_add_mul_I, mul_assoc, Complex.ofReal_ne_zero, Complex.ofReal_exp, Real.exp_log, mul_div_cancel₀, norm_ne_zero_iff, Complex.ofReal_cos, Complex.ofReal_div, Complex.ofReal_sin, mul_add, Complex.re_add_im, Complex.sin_arg, Complex.cos_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ Membership.mem (γ := Set ℂ) {0}ᶜ (cexp x)

Tactic:
exp_ne_zero x

Premises used: Complex.exp_ne_zero, Set.Mem, setOf, Set.singleton, Not
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ Membership.mem (γ := Set ℂ) {0}ᶜ (cexp x)

Tactic:
exact exp_ne_zero x

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₃ : (↑x.re : ℂ) + (↑(cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
rw₄ : (↑x.re : ℂ) + (↑((↑(rexp x.re) : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
rw₅ : (↑x.re : ℂ) + (↑x.im : ℂ) * I = x
rw₆ rw₇ : x = x
⊢ log (cexp x) = x

Tactic:
rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]

Premises used: Complex.log, Real.log_exp, Complex.arg_mul_cos_add_sin_mul_I, Complex.ofReal_exp, And.intro, Complex.norm_exp, Complex.exp_eq_exp_re_mul_sin_add_cos, Complex.re_add_im, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
rw :
  (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
rw₁ :
  (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I =
    (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
rw₃ rw₄ :
  (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I =
    (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
⊢ log (cexp x) = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I

Tactic:
rw [log, norm_exp, Real.log_exp, arg_exp]

Premises used: Complex.log, Real.log_exp, Complex.norm_exp, Complex.arg_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
rw :
  (↑x.re : ℂ) + (↑x.im : ℂ) * I - (↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) : ℂ) * I =
    x - (↑(toIocDiv Real.two_pi_pos (-π) x.im) : ℂ) * (2 * (↑π : ℂ) * I)
⊢ log (cexp x) = x - (↑(toIocDiv Real.two_pi_pos (-π) x.im) : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rw [log_exp_eq_re_add_toIocMod, toIocMod, ofReal_sub, sub_mul, ← add_sub_assoc]

Premises used: add_sub_assoc, Complex.log_exp_eq_re_add_toIocMod, sub_mul, toIocMod, Complex.ofReal_sub