awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h₂ : (↑(Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
h₂ : (↑(Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h₃ : (↑((↑(Real.cos x) : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
h₂ : (↑(Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₃ : (↑((↑(Real.cos x) : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h₄ : (↑((↑(Real.cos x) : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
h₂ : (↑(Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₃ : (↑((↑(Real.cos x) : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₄ : (↑((↑(Real.cos x) : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h₅ : (↑((↑(↑x : Angle).cos : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
h₂ : (↑(Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₃ : (↑((↑(Real.cos x) : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₄ : (↑((↑(Real.cos x) : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
h₅ : (↑((↑(↑x : Angle).cos : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h₆ : (↑((↑(↑x : Angle).cos : ℂ) + (↑(↑x : Angle).sin : ℂ) * I).arg : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
h₂ : (↑(Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₃ : (↑((↑(Real.cos x) : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₄ : (↑((↑(Real.cos x) : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
h₅ : (↑((↑(↑x : Angle).cos : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
h₆ : (↑((↑(↑x : Angle).cos : ℂ) + (↑(↑x : Angle).sin : ℂ) * I).arg : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h₇ : (↑x : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
⊢ Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)) T
have inl : Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / 0 * x)) 0
Tactic: rcases eq_or_ne T 0 with (rfl | hT)
Cleared hypotheses: T
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
inl : Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / 0 * x)) 0
⊢ Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)) T
have inr : ∀ (hT : T ≠ 0), Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)) T
Tactic: rcases eq_or_ne T 0 with (rfl | hT)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Eq (α := Circle) ((fun (x : ℝ) ↦ ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)) (x + T))
    ((fun (x : ℝ) ↦ ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)) x)
have inr : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π / T * T) : Circle)
  ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
Tactic: simp_rw [mul_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π / T * T) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
have inr : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π) : Circle)
  ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
Tactic: rw [div_mul_cancel₀ _ hT, Circle.periodic_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
x : ℝ
inr :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
⊢ Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π / T * T) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
have inr₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
  ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
Tactic: rw [div_mul_cancel₀ _ hT, Circle.periodic_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x y : AddCircle T
⊢ (x + y).toCircle = x.toCircle * y.toCircle
have H : ∀ (z : ℝ),
  ((↑z : ℝ ⧸ AddSubgroup.zmultiples T) + y).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * y.toCircle
Tactic: induction x using QuotientAddGroup.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
y : AddCircle T
z : ℝ
⊢ ((↑z : ℝ ⧸ AddSubgroup.zmultiples T) + y).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * y.toCircle
have H : ∀ (z_1 : ℝ),
  (HAdd.hAdd (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
Tactic: induction y using QuotientAddGroup.induction_on
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T z z_1 : ℝ
⊢ (HAdd.hAdd (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
have H : toCircle (T := T) (↑(z + z_1) : ℝ ⧸ AddSubgroup.zmultiples T) =
  toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
Tactic: simp_rw [← coe_add, toCircle_apply_mk, mul_add, Circle.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T z z_1 : ℝ
H :
  toCircle (T := T) (↑(z + z_1) : ℝ ⧸ AddSubgroup.zmultiples T) =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ (HAdd.hAdd (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
have H₁ : (Circle.exp : (a : ℝ) → Circle) (2 * π / T * (z + z_1)) =
  HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
Tactic: simp_rw [← coe_add, toCircle_apply_mk, mul_add, Circle.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T z z_1 : ℝ
H :
  toCircle (T := T) (↑(z + z_1) : ℝ ⧸ AddSubgroup.zmultiples T) =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
H₁ :
  (Circle.exp : (a : ℝ) → Circle) (2 * π / T * (z + z_1)) =
    HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
      ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
⊢ (HAdd.hAdd (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
have H₂ : (Circle.exp : (a : ℝ) → Circle) (2 * π / T * z + 2 * π / T * z_1) =
  HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
Tactic: simp_rw [← coe_add, toCircle_apply_mk, mul_add, Circle.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
⊢ toCircle (T := T) 0 = 1
have rw : toCircle (T := T) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) = 1
Tactic: rw [← QuotientAddGroup.mk_zero, toCircle_apply_mk, mul_zero, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
rw : toCircle (T := T) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) = 1
⊢ toCircle (T := T) 0 = 1
have rw₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * 0) : Circle) (1 : Circle)
Tactic: rw [← QuotientAddGroup.mk_zero, toCircle_apply_mk, mul_zero, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
rw : toCircle (T := T) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) = 1
rw₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * 0) : Circle) (1 : Circle)
⊢ toCircle (T := T) 0 = 1
have rw₂ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
Tactic: rw [← QuotientAddGroup.mk_zero, toCircle_apply_mk, mul_zero, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
rw : toCircle (T := T) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) = 1
rw₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * 0) : Circle) (1 : Circle)
rw₂ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
⊢ toCircle (T := T) 0 = 1
have rw₃ : Eq (α := Circle) 1 1
Tactic: rw [← QuotientAddGroup.mk_zero, toCircle_apply_mk, mul_zero, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
⊢ ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)
have succ : (n • x + x).toCircle = x.toCircle ^ (n + 1)
Tactic: rw [succ_nsmul, toCircle_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
succ : (n • x + x).toCircle = x.toCircle ^ (n + 1)
⊢ ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)
have succ₁ : (n • x).toCircle * x.toCircle = x.toCircle ^ (n + 1)
Tactic: rw [succ_nsmul, toCircle_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
succ : (n • x + x).toCircle = x.toCircle ^ (n + 1)
succ₁ : (n • x).toCircle * x.toCircle = x.toCircle ^ (n + 1)
⊢ ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)
have succ₂ : x.toCircle ^ n * x.toCircle = x.toCircle ^ (n + 1)
Tactic: rw [succ_nsmul, toCircle_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
succ : (n • x + x).toCircle = x.toCircle ^ (n + 1)
succ₁ : (n • x).toCircle * x.toCircle = x.toCircle ^ (n + 1)
succ₂ : x.toCircle ^ n * x.toCircle = x.toCircle ^ (n + 1)
⊢ ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)
have succ₃ : x.toCircle ^ n * x.toCircle = x.toCircle ^ n * x.toCircle
Tactic: rw [succ_nsmul, toCircle_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℕ
⊢ (n • x).toCircle = x.toCircle ^ n
have zero : (HSMul.hSMul (α := ℕ) 0 x).toCircle = HPow.hPow (β := ℕ) x.toCircle 0
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [succ_nsmul, toCircle_add, ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℕ
zero : (HSMul.hSMul (α := ℕ) 0 x).toCircle = HPow.hPow (β := ℕ) x.toCircle 0
⊢ (n • x).toCircle = x.toCircle ^ n
have succ : ∀ (n : ℕ) (ih : (n • x).toCircle = x.toCircle ^ n), ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [succ_nsmul, toCircle_add, ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℤ
⊢ (n • x).toCircle = x.toCircle ^ n
have ofNat : ∀ (a : ℕ), (Int.ofNat a • x).toCircle = x.toCircle ^ Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
x : AddCircle T
n : ℤ
ofNat : ∀ (a : ℕ), (Int.ofNat a • x).toCircle = x.toCircle ^ Int.ofNat a
⊢ (n • x).toCircle = x.toCircle ^ n
have negSucc : ∀ (a : ℕ), (Int.negSucc a • x).toCircle = x.toCircle ^ Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
a b : AddCircle T
h : a.toCircle = b.toCircle
⊢ a = b
have H : ∀ (z : ℝ) (h : toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b.toCircle),
  (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b
Tactic: induction a using QuotientAddGroup.induction_on
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
b : AddCircle T
z : ℝ
h : toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b.toCircle
⊢ (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b
have H : ∀ (z_1 : ℝ)
  (h : toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)),
  Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
Tactic: induction b using QuotientAddGroup.induction_on
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
⊢ Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
have H : ∀ (m : ℤ) (hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)),
  Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
Tactic: obtain ⟨m, hm⟩ := Circle.exp_eq_exp.mp h.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
⊢ Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
have H : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples T) (-z + z_1)
Tactic: rw [QuotientAddGroup.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
⊢ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples T) (-z + z_1)
have H : ∃ (k : ℤ), (↑k : ℝ) * T = -z + z_1
Tactic: simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
⊢ ∃ (k : ℤ), (↑k : ℝ) * T = -z + z_1
have h₁ : (↑m : ℝ) * T = -z + z_1
Tactic: use m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
⊢ (↑m : ℝ) * T = -z + z_1
have hm₁ : z_1 = z + T * (↑m : ℝ)
Tactic: field_simp at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : z_1 = z + T * (↑m : ℝ)
⊢ (↑m : ℝ) * T = -z + z_1
have linarith : (↑m : ℝ) * T < -z + z_1 → z_1 - (z + T * (↑m : ℝ)) + ((↑m : ℝ) * T - (-z + z_1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : z_1 = z + T * (↑m : ℝ)
linarith : (↑m : ℝ) * T < -z + z_1 → z_1 - (z + T * (↑m : ℝ)) + ((↑m : ℝ) * T - (-z + z_1)) = 0
⊢ (↑m : ℝ) * T = -z + z_1
have linarith₁ : -z + z_1 < (↑m : ℝ) * T → -(z_1 - (z + T * (↑m : ℝ))) + (-z + z_1 - (↑m : ℝ) * T) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
⊢ Continuous (Y := AddCircle (2 * π)) fun (x : Circle) ↦ (↑(↑x : ℂ).arg : ℝ ⧸ AddSubgroup.zmultiples (2 * π))
have rw : ∀ (x : Circle),
  ContinuousAt (Y := AddCircle (2 * π)) (fun (x : Circle) ↦ (↑(↑x : ℂ).arg : ℝ ⧸ AddSubgroup.zmultiples (2 * π))) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
T : ℝ
hT : T ≠ 0
x : AddCircle T
⊢ (homeomorphCircle hT : (a : AddCircle T) → Circle) x = x.toCircle
have H : ∀ (z : ℝ),
  (homeomorphCircle hT : (a : AddCircle T) → Circle) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T)
Tactic: cases x using QuotientAddGroup.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
⊢ IsAddQuotientCoveringMap (E := ℝ) (X := Circle) (⇑exp : (a : ℝ) → Circle) ↥(AddSubgroup.zmultiples (2 * π))
have h : Eq (α := ℝ → Circle) (⇑exp : (a : ℝ) → Circle)
  (comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
    (⇑(homeomorphCircle sorry) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk)
Tactic: convert! (isAddQuotientCoveringMap_coe _).homeomorph_comp (homeomorphCircle _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
h :
  Eq (α := ℝ → Circle) (⇑exp : (a : ℝ) → Circle)
    (comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
      (⇑(homeomorphCircle ⋯) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk)
⊢ IsAddQuotientCoveringMap (E := ℝ) (X := Circle) (⇑exp : (a : ℝ) → Circle) ↥(AddSubgroup.zmultiples (2 * π))
have convert_2 : 2 * π ≠ 0
Tactic: convert! (isAddQuotientCoveringMap_coe _).homeomorph_comp (homeomorphCircle _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
⊢ Eq (α := ℝ → Circle) (⇑exp : (a : ℝ) → Circle)
    (comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
      (⇑(homeomorphCircle ⋯) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk)
have h : ∀ (x : ℝ),
  Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) x) : ℂ)
    (↑(comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
          (⇑(homeomorphCircle sorry) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk x) :
      ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
Goal:
n : ℤ
inst : NeZero n
⊢ IsQuotientCoveringMap (X := Circle) (fun (x : Circle) ↦ x ^ n) ↥(MonoidHom.ker (zpowGroupHom n))
have hn : IsUnit (M := ℝ) (↑n : ℝ)
Tactic: have hn : IsUnit (n : ℝ) := by simpa using NeZero.ne n
-- 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 ⋯
⊢ IsQuotientCoveringMap (X := Circle) (fun (x : Circle) ↦ x ^ n) ↥(MonoidHom.ker (zpowGroupHom n))
have refine_1 : Topology.IsQuotientMap (X := Circle) (Y := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle)
Tactic: refine Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom
    (f := zpowGroupHom (α := Circle) n) ?_ (Set.Finite.isDiscrete <| .of_preimage ?_ e.surjective)
-- 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 ⋯
refine_1 : Topology.IsQuotientMap (X := Circle) (Y := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle)
⊢ IsQuotientCoveringMap (X := Circle) (fun (x : Circle) ↦ x ^ n) ↥(MonoidHom.ker (zpowGroupHom n))
have refine_2 : Set.Finite (α := AddCircle (𝕜 := ℝ) 1)
  ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))
Tactic: refine Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom
    (f := zpowGroupHom (α := Circle) n) ?_ (Set.Finite.isDiscrete <| .of_preimage ?_ e.surjective)
-- 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 := Circle) (Y := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle)
have refine_1 : Topology.IsQuotientMap (X := AddCircle (𝕜 := ℝ) 1) (Y := Circle)
  (comp (β := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle) (⇑e : (a : AddCircle 1) → Circle))
Tactic: refine .of_comp e.continuous (continuous_zpow n) ?_