awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ Topology.IsQuotientMap (X := AddCircle (𝕜 := ℝ) 1) (Y := Circle)
    (comp (β := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle) (⇑e : (a : AddCircle 1) → Circle))
have h : Eq (α := AddCircle (𝕜 := ℝ) 1 → Circle)
  (comp (β := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle) (⇑e : (a : AddCircle 1) → Circle))
  (comp (β := AddCircle (𝕜 := ℝ) 1) (⇑e : (a : AddCircle 1) → Circle)
    fun (x : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)) ↦ n • x)
Tactic: convert!
      e.isQuotientMap.comp <|
        IsUnit.isQuotientMap_zsmul (M := ℝ) (QuotientAddGroup.mk' (AddSubgroup.zmultiples (1 : ℝ)))
          isQuotientMap_quotient_mk' n hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ Eq (α := AddCircle (𝕜 := ℝ) 1 → Circle)
    (comp (β := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle) (⇑e : (a : AddCircle 1) → Circle))
    (comp (β := AddCircle (𝕜 := ℝ) 1) (⇑e : (a : AddCircle 1) → Circle)
      fun (x : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)) ↦ n • x)
have h : ∀ (x : AddCircle (𝕜 := ℝ) 1),
  Eq (α := ℂ)
    (↑(comp (β := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle) (⇑e : (a : AddCircle 1) → Circle) x) : ℂ)
    (↑(comp (β := AddCircle (𝕜 := ℝ) 1) (⇑e : (a : AddCircle 1) → Circle)
          (fun (x : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)) ↦ n • x) x) :
      ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ Set.Finite (α := AddCircle (𝕜 := ℝ) 1)
    ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))
have h : Eq (α := Set (AddCircle (𝕜 := ℝ) 1))
  ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))
  {x : AddCircle (𝕜 := ℝ) 1 | n • x = 0}
Tactic: convert! finite_torsion_of_isSMulRegular_int (1 : ℝ) n fun _ ↦ by simp [NeZero.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ Eq (α := Set (AddCircle (𝕜 := ℝ) 1))
    ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))
    {x : AddCircle (𝕜 := ℝ) 1 | n • x = 0}
have h : ∀ (x : AddCircle (𝕜 := ℝ) 1),
  Membership.mem (γ := Set (AddCircle (𝕜 := ℝ) 1))
      ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle)) x ↔
    Membership.mem (γ := Set (AddCircle (𝕜 := ℝ) 1)) {x : AddCircle (𝕜 := ℝ) 1 | n • x = 0} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ℤ
⊢ (↑((toCircle : (a : ZMod N) → Circle) (↑j : ZMod N)) : ℂ) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))
have rw : cexp ((↑(2 * π / 1 * HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))
Tactic: rw [toCircle, AddChar.compAddMonoidHom_apply, toCircle_addChar, AddChar.coe_mk,
    AddCircle.toCircle, toAddCircle_intCast, Function.Periodic.lift_coe, Circle.coe_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ℤ
⊢ cexp ((↑(2 * π / 1 * HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))
have push_cast : cexp (2 * (↑π : ℂ) / 1 * HDiv.hDiv (α := ℂ) (↑j : ℂ) (↑N : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ) = cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ))
have rw : Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ) (↑((toCircle : (a : ZMod N) → Circle) (↑j.val : ZMod N)) : ℂ)
Tactic: rw [← toCircle_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
rw :
  Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ)
    (↑((toCircle : (a : ZMod N) → Circle) (↑j.val : ZMod N)) : ℂ)
⊢ (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ) = cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ))
have rw₁ : Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ)
Tactic: rw [← toCircle_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ Eq (α := Circle) ((toCircle : (a : ZMod N) → Circle) j : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : Circle)
have a : Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ)
  (↑((Circle.exp : (a : ℝ) → Circle) (2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ))) : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ)
    (↑((Circle.exp : (a : ℝ) → Circle) (2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ))) : ℂ)
have a : cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) = cexp ((↑(2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * I)
Tactic: rw [toCircle_apply, Circle.coe_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) =
    cexp ((↑(2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * I)
have a : cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) = cexp (2 * (↑π : ℂ) * HDiv.hDiv (α := ℂ) (↑j.val : ℂ) (↑N : ℂ) * I)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) = cexp (2 * (↑π : ℂ) * HDiv.hDiv (α := ℂ) (↑j.val : ℂ) (↑N : ℂ) * I)
have a : 2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ) = 2 * (↑π : ℂ) * HDiv.hDiv (α := ℂ) (↑j.val : ℂ) (↑N : ℂ) * I
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
⊢ AddChar.IsPrimitive (R := ZMod N) stdAddChar
have refine : ∀ (t : ZMod N) (ht : Eq (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) t : ℂ) (1 : ℂ)), t = 0
Tactic: refine AddChar.zmod_char_primitive_of_eq_one_only_at_zero _ _ (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
t : ZMod N
ht : Eq (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) t : ℂ) (1 : ℂ)
⊢ t = 0
have rwa : ∀ (ht : Eq (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) t : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) 0 : ℂ)), t = 0
Tactic: rwa [← (stdAddChar (N := N)).map_zero_eq_one, injective_stdAddChar.eq_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
t : ZMod N
ht : Eq (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) t : ℂ) (1 : ℂ)
rwa : ∀ (ht : Eq (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) t : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) 0 : ℂ)), t = 0
⊢ t = 0
have rwa₁ : ∀ (ht : t = 0), t = 0
Tactic: rwa [← (stdAddChar (N := N)).map_zero_eq_one, injective_stdAddChar.eq_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
n : ℕ
inst_1 : NeZero n
x : ZMod n
⊢ Membership.mem (α := Circleˣ) (γ := Subgroup Circleˣ) (rootsOfUnity n Circle)
    ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x) : Circleˣ)
have huv : (↑(↑(HPow.hPow (α := Circleˣ) ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x) : Circleˣ) n) :
        Circle) :
    ℂ) =
  (↑(↑1 : Circle) : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
N : ℕ
inst : NeZero N
n : ℕ
inst_1 : NeZero n
x x_1 : ZMod n
⊢ Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
      ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) (x + x_1))) ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity n Circle)) (β := ↥(rootsOfUnity n Circle))
      (Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
          ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x)) ⋯ :
        ↥(rootsOfUnity n Circle))
      (Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
          ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x_1)) ⋯ :
        ↥(rootsOfUnity n Circle))
have a : (↑(↑(↑(Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
                ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) (x + x_1))) sorry) :
            Circleˣ) :
        Circle) :
    ℂ) =
  (↑(↑(↑(HMul.hMul (α := ↥(rootsOfUnity n Circle)) (β := ↥(rootsOfUnity n Circle))
                (Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
                    ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x)) sorry :
                  ↥(rootsOfUnity n Circle))
                (Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
                    ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x_1)) sorry :
                  ↥(rootsOfUnity n Circle))) :
            Circleˣ) :
        Circle) :
    ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
n : ℕ
inst : NeZero n
z : ↥(rootsOfUnity n ℂ)
⊢ Membership.mem (α := Circleˣ) (γ := Subgroup Circleˣ) (rootsOfUnity n Circle)
    (((rootsOfUnitytoCircle n).toHomUnits : (a : ↥(rootsOfUnity n ℂ)) → Circleˣ) z : Circleˣ)
have rw : Eq (α := Circle) ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) (z ^ n) : Circle)
  ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) 1 : Circle)
Tactic: rw [mem_rootsOfUnity', MonoidHom.coe_toHomUnits, ← map_pow, ← (rootsOfUnitytoCircle n).map_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
n : ℕ
inst : NeZero n
z : ↥(rootsOfUnity n ℂ)
⊢ Eq (α := Circle) ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) (z ^ n) : Circle)
    ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) 1 : Circle)
have h : z ^ n = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar (goal)
Goal:
n : ℕ
inst : NeZero n
x : ↥(rootsOfUnity n ℂ)
w : ℂˣ
hw : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity 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
have 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
Tactic: obtain ⟨j, hj1, hj2⟩ := (Complex.mem_rootsOfUnity n w).mp hw
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
Goal:
R₁ R₂ θ₁ θ₂ : ℝ
⊢ circleMap 0 R₁ θ₁ * circleMap 0 R₂ θ₂ = circleMap 0 (R₁ * R₂) (θ₁ + θ₂)
have simp : (↑R₁ : ℂ) * cexp ((↑θ₁ : ℂ) * I) * ((↑R₂ : ℂ) * cexp ((↑θ₂ : ℂ) * I)) =
  (↑R₁ : ℂ) * (↑R₂ : ℂ) * (cexp ((↑θ₁ : ℂ) * I) * cexp ((↑θ₂ : ℂ) * I))
Tactic: simp only [circleMap_zero, ofReal_mul, ofReal_add, add_mul, Complex.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
Goal:
R₁ R₂ θ₁ θ₂ : ℝ
⊢ circleMap 0 R₁ θ₁ / circleMap 0 R₂ θ₂ = circleMap 0 (R₁ / R₂) (θ₁ - θ₂)
have simp : (↑R₁ : ℂ) * cexp ((↑θ₁ : ℂ) * I) / ((↑R₂ : ℂ) * cexp ((↑θ₂ : ℂ) * I)) =
  (↑R₁ : ℂ) / (↑R₂ : ℂ) * (cexp ((↑θ₁ : ℂ) * I) / cexp ((↑θ₂ : ℂ) * I))
Tactic: simp only [circleMap_zero, ofReal_div, ofReal_sub, sub_mul, Complex.exp_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (hypothesis)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
⊢ circleMap c R a = circleMap c R b ↔ ∃ (n : ℤ), (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (hypothesis)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
h : circleMap c R a = circleMap c R b
⊢ a = b
have h₁ : ∃ (n : ℤ), (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: rw [circleMap_eq_circleMap_iff c h_R] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
h : ∃ (n : ℤ), (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ a = b
have obtain : ∀ (n : ℤ) (hn : (↑a : ℂ) * I = (↑b : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)), a = b
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (hypothesis)
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
have hn₁ : (↑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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (hypothesis)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
n : ℤ
hn : (↑a : ℂ) = (↑b : ℂ) + HMul.hMul (α := ℂ) (↑n : ℂ) 2 * (↑π : ℂ)
⊢ a = b
have hn₁ : a = b + (↑(n * 2) : ℝ) * π
Tactic: norm_cast at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (hypothesis)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
n : ℤ
hn : a = b + (↑(n * 2) : ℝ) * π
⊢ a = b
have h_dist₁ : |(↑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
Cleared hypotheses: h_dist
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (hypothesis)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
n : ℤ
hn : a = b + (↑(n * 2) : ℝ) * π
h_dist : |(↑n : ℝ)| * (2 * π) < 2 * π
⊢ a = b
have h_dist₁ : LT.lt (α := ℝ) |(↑n : ℝ)| 1
Tactic: simp (disch := positivity) at h_dist
Cleared hypotheses: h_dist
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (hypothesis)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
n : ℤ
hn : a = b + (↑(n * 2) : ℝ) * π
h_dist : LT.lt (α := ℝ) |(↑n : ℝ)| 1
⊢ a = b
have h_dist₁ : |n| < 1
Tactic: norm_cast at h_dist
Cleared hypotheses: h_dist
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ x₁ = x₂
have apply : |x₁ - x₂| < 2 * π
Tactic: apply eq_of_circleMap_eq h_R _ h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ |x₁ - x₂| < 2 * π
have rw : -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
Tactic: rw [abs_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
have left : -(2 * π) < x₁ - x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : |a - b| ≤ 2 * π
x₁ : ℝ
left_1 : min a b < x₁
right : x₁ ≤ max a b
x₂ : ℝ
left_2 : min a b < x₂
right_1 : x₂ ≤ max a b
h : circleMap c R x₁ = circleMap c R x₂
left : -(2 * π) < x₁ - x₂
⊢ -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
have right : x₁ - x₂ < 2 * π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ -(2 * π) < x₁ - x₂
have 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
Tactic: linarith [max_sub_min_eq_abs' a b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ x₁ - x₂ < 2 * π
have 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
Tactic: linarith [max_sub_min_eq_abs' a b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ x₁ = x₂
have apply : |x₁ - x₂| < 2 * π
Tactic: apply eq_of_circleMap_eq h_R _ h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ |x₁ - x₂| < 2 * π
have rw : -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
Tactic: rw [abs_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
have left : -(2 * π) < x₁ - x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
Goal:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_1 : b - a ≤ 2 * π
x₁ : ℝ
left_1 : a ≤ x₁
right : x₁ < b
x₂ : ℝ
left_2 : a ≤ x₂
right_1 : x₂ < b
h : circleMap c R x₁ = circleMap c R x₂
left : -(2 * π) < x₁ - x₂
⊢ -(2 * π) < x₁ - x₂ ∧ x₁ - x₂ < 2 * π
have right : x₁ - x₂ < 2 * π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ -(2 * π) < x₁ - x₂
have linarith : x₁ - x₂ ≤ -(2 * π) → b - a - 2 * π + (a - x₁) + (x₂ - b) + (x₁ - x₂ - -(2 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (goal)
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₂
⊢ x₁ - x₂ < 2 * π
have linarith : 2 * π ≤ x₁ - x₂ → b - a - 2 * π + (x₁ - b) + (a - x₂) + (2 * π - (x₁ - x₂)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
⊢ cexp (log x) = x
have rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
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
⊢ cexp (log x) = x
have rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
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
⊢ cexp (log x) = x
have rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
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
⊢ cexp (log x) = x
have rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = 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]