awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
h :
  ∀ (x : ℝ),
    Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) x) : ℂ)
      (↑(comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
            (⇑(homeomorphCircle ⋯) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk x) :
        ℂ)
⊢ Eq (α := ℝ → Circle) (⇑exp : (a : ℝ) → Circle)
    (comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
      (⇑(homeomorphCircle ⋯) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) x) : ℂ)
    (↑(comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
          (⇑(homeomorphCircle ⋯) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk x) :
      ℂ)

Tactic:
simp [homeomorphCircle_apply, toCircle]

Premises used: AddCircle.toCircle, AddCircle.homeomorphCircle_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ IsCoveringMap (E := ℝ) (X := Circle) (⇑exp : (a : ℝ) → Circle)

Tactic:
isAddQuotientCoveringMap_exp.isCoveringMap

Premises used: Circle.isAddQuotientCoveringMap_exp, IsAddQuotientCoveringMap.isCoveringMap
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ IsLocalHomeomorph (X := ℝ) (Y := Circle) (⇑Circle.exp : (a : ℝ) → Circle)

Tactic:
Circle.isCoveringMap_exp.isLocalHomeomorph

Premises used: IsCoveringMap.isLocalHomeomorph, Circle.isCoveringMap_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
⊢ IsUnit (M := ℝ) (↑n : ℝ)

Tactic:
simpa using NeZero.ne n

Premises used: NeZero.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
⊢ IsUnit (M := ℝ) (↑n : ℝ)

Tactic:
have hn : IsUnit (n : ℝ) := by simpa using NeZero.ne n
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))

Tactic:
Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom
    (f := zpowGroupHom (α := Circle) n) ?_ (Set.Finite.isDiscrete <| .of_preimage ?_ e.surjective)

Premises used: Set.Finite.isDiscrete, Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom, Set.Finite.of_preimage, Homeomorph.surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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)
refine_2 :
  Set.Finite (α := AddCircle (𝕜 := ℝ) 1)
    ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))
⊢ IsQuotientCoveringMap (X := Circle) (fun (x : Circle) ↦ x ^ n) ↥(MonoidHom.ker (zpowGroupHom n))

Tactic:
refine Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom
    (f := zpowGroupHom (α := Circle) n) ?_ (Set.Finite.isDiscrete <| .of_preimage ?_ e.surjective)

Premises used: Set.Finite.isDiscrete, Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom, Set.Finite.of_preimage, Homeomorph.surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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)

Tactic:
.of_comp e.continuous (continuous_zpow n) ?_

Premises used: continuous_zpow, Homeomorph.continuous, Topology.IsQuotientMap.of_comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
refine_1 :
  Topology.IsQuotientMap (X := AddCircle (𝕜 := ℝ) 1) (Y := Circle)
    (comp (β := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle) (⇑e : (a : AddCircle 1) → Circle))
⊢ Topology.IsQuotientMap (X := Circle) (Y := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle)

Tactic:
refine .of_comp e.continuous (continuous_zpow n) ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ Topology.IsQuotientMap (X := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)) (Y := Circle)
    (comp (β := AddCircle (𝕜 := ℝ) 1) (⇑e : (a : AddCircle 1) → Circle)
      fun (x : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)) ↦ n • x)

Tactic:
e.isQuotientMap.comp <|
        IsUnit.isQuotientMap_zsmul (M := ℝ) (QuotientAddGroup.mk' (AddSubgroup.zmultiples (1 : ℝ)))
          isQuotientMap_quotient_mk' n hn

Premises used: isQuotientMap_quotient_mk', Topology.IsQuotientMap.comp, IsUnit.isQuotientMap_zsmul, QuotientAddGroup.mk', AddSubgroup.zmultiples, OfNat.ofNat, Homeomorph.isQuotientMap
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
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)
⊢ Topology.IsQuotientMap (X := AddCircle (𝕜 := ℝ) 1) (Y := Circle)
    (comp (β := Circle) (⇑(zpowGroupHom n) : (a : Circle) → Circle) (⇑e : (a : AddCircle 1) → Circle))

Tactic:
convert!
      e.isQuotientMap.comp <|
        IsUnit.isQuotientMap_zsmul (M := ℝ) (QuotientAddGroup.mk' (AddSubgroup.zmultiples (1 : ℝ)))
          isQuotientMap_quotient_mk' n hn

Premises used: isQuotientMap_quotient_mk', Topology.IsQuotientMap.comp, IsUnit.isQuotientMap_zsmul, QuotientAddGroup.mk', AddSubgroup.zmultiples, OfNat.ofNat, Homeomorph.isQuotientMap
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
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) :
        ℂ)
⊢ 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:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
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:
simp [zpowGroupHom, e, homeomorphCircle_apply, toCircle_zsmul]

Premises used: AddCircle.toCircle_zsmul, zpowGroupHom, AddCircle.homeomorphCircle_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
x : ℝ
⊢ ∀ ⦃a₂ : ℝ⦄, Eq (α := ℝ) ((fun (x : ℝ) ↦ n • x) x) ((fun (x : ℝ) ↦ n • x) a₂) → x = a₂

Tactic:
simp [NeZero.ne]

Premises used: NeZero.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
h :
  Eq (α := Set (AddCircle (𝕜 := ℝ) 1))
    ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))
    {x : AddCircle (𝕜 := ℝ) 1 | n • x = 0}
⊢ Set.Finite (α := AddCircle (𝕜 := ℝ) 1)
    ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))

Tactic:
convert! finite_torsion_of_isSMulRegular_int (1 : ℝ) n fun _ ↦ by simp [NeZero.ne]

Premises used: AddCircle.finite_torsion_of_isSMulRegular_int, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
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
⊢ Eq (α := Set (AddCircle (𝕜 := ℝ) 1))
    ((⇑e : (a : AddCircle 1) → Circle) ⁻¹' (↑(MonoidHom.ker (zpowGroupHom n)) : Set Circle))
    {x : AddCircle (𝕜 := ℝ) 1 | n • x = 0}

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℤ
inst : NeZero n
hn : IsUnit (M := ℝ) (↑n : ℝ)
e : AddCircle (𝕜 := ℝ) 1 ≃ₜ Circle := homeomorphCircle ⋯
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:
simp [e, homeomorphCircle_apply, ← toCircle_zsmul, ← (injective_toCircle one_ne_zero).eq_iff]

Premises used: Function.Injective.eq_iff, AddCircle.injective_toCircle, AddCircle.toCircle_zsmul, one_ne_zero, AddCircle.homeomorphCircle_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
n : ℕ
inst : NeZero n
⊢ IsQuotientCoveringMap (X := Circle) (fun (x : Circle) ↦ x ^ n) ↥(MonoidHom.ker (powMonoidHom n))

Tactic:
isQuotientCoveringMap_zpow n

Premises used: Set.Mem, setOf, Circle.isQuotientCoveringMap_zpow, Nat.cast, zpowRec, powMonoidHom, Metric.sphere
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ℤ
rw :
  cexp ((↑(2 * π / 1 * HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))
⊢ (↑((toCircle : (a : ZMod N) → Circle) (↑j : ZMod N)) : ℂ) = 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]

Premises used: AddCircle.toCircle_addChar, ZMod.toCircle, ZMod.toAddCircle_intCast, AddChar.compAddMonoidHom_apply, Function.Periodic.lift_coe, AddCircle.toCircle, Circle.coe_exp, AddChar.coe_mk
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ℤ
push_cast :
  cexp (2 * (↑π : ℂ) / 1 * HDiv.hDiv (α := ℂ) (↑j : ℂ) (↑N : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))
⊢ cexp ((↑(2 * π / 1 * HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ℤ
⊢ cexp (2 * (↑π : ℂ) / 1 * HDiv.hDiv (α := ℂ) (↑j : ℂ) (↑N : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ℕ
⊢ (↑((toCircle : (a : ZMod N) → Circle) (↑j : ZMod N)) : ℂ) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))

Tactic:
simpa using toCircle_intCast (N := N) j

Premises used: Nat.cast, ZMod.toCircle_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
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)) : ℂ)
rw₁ rw₂ : Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ)
⊢ (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ) = cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ))

Tactic:
rw [← toCircle_natCast, natCast_zmod_val]

Premises used: ZMod.natCast_zmod_val, ZMod.toCircle_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
a :
  Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ)
    (↑((Circle.exp : (a : ℝ) → Circle) (2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ))) : ℂ)
⊢ Eq (α := Circle) ((toCircle : (a : ZMod N) → Circle) j : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : Circle)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
a :
  cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) =
    cexp ((↑(2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * I)
⊢ Eq (α := ℂ) (↑((toCircle : (a : ZMod N) → Circle) j) : ℂ)
    (↑((Circle.exp : (a : ℝ) → Circle) (2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ))) : ℂ)

Tactic:
rw [toCircle_apply, Circle.coe_exp]

Premises used: ZMod.toCircle_apply, Circle.coe_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
a :
  cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) = cexp (2 * (↑π : ℂ) * HDiv.hDiv (α := ℂ) (↑j.val : ℂ) (↑N : ℂ) * I)
⊢ cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) =
    cexp ((↑(2 * π * HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * I)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
a : 2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ) = 2 * (↑π : ℂ) * HDiv.hDiv (α := ℂ) (↑j.val : ℂ) (↑N : ℂ) * I
⊢ cexp (2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ)) = cexp (2 * (↑π : ℂ) * HDiv.hDiv (α := ℂ) (↑j.val : ℂ) (↑N : ℂ) * I)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ 2 * (↑π : ℂ) * I * (↑j.val : ℂ) / (↑N : ℂ) = 2 * (↑π : ℂ) * HDiv.hDiv (α := ℂ) (↑j.val : ℂ) (↑N : ℂ) * I

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
⊢ Injective (α := ZMod N) (β := Circle) (⇑toCircle : (a : ZMod N) → Circle)

Tactic:
(AddCircle.injective_toCircle one_ne_zero).comp (toAddCircle_injective N)

Premises used: Quotient.liftOn', Function.Periodic.lift, AddCircle.injective_toCircle, Function.Injective.comp, ZMod.toAddCircle_injective, AddCircle.toCircle, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ℤ
⊢ (stdAddChar : (a : ZMod N) → ℂ) (↑j : ZMod N) = cexp (2 * (↑π : ℂ) * I * (↑j : ℂ) / (↑N : ℂ))

Tactic:
simp [stdAddChar, toCircle_intCast]

Premises used: ZMod.stdAddChar, ZMod.toCircle_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ Eq (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) j : ℂ) ((↑((toCircle : (a : ZMod N) → Circle) j) : ℂ) : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
⊢ Injective (α := ZMod N) (β := ℂ) (⇑stdAddChar : (a : ZMod N) → ℂ)

Tactic:
Subtype.coe_injective.comp injective_toCircle

Premises used: Subtype.coe_injective, Function.Injective.comp, ZMod.injective_toCircle
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
⊢ AddChar.IsPrimitive (R := ZMod N) stdAddChar

Tactic:
AddChar.zmod_char_primitive_of_eq_one_only_at_zero _ _ (fun t ht ↦ ?_)

Premises used: AddChar.zmod_char_primitive_of_eq_one_only_at_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
refine : ∀ (t : ZMod N) (ht : Eq (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) t : ℂ) (1 : ℂ)), t = 0
⊢ AddChar.IsPrimitive (R := ZMod N) stdAddChar

Tactic:
refine AddChar.zmod_char_primitive_of_eq_one_only_at_zero _ _ (fun t ht ↦ ?_)

Premises used: AddChar.zmod_char_primitive_of_eq_one_only_at_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (ht : t = 0), t = 0
⊢ t = 0

Tactic:
rwa [← (stdAddChar (N := N)).map_zero_eq_one, injective_stdAddChar.eq_iff] at ht

Premises used: ZMod.stdAddChar, Function.Injective.eq_iff, AddChar.map_zero_eq_one, ZMod.injective_stdAddChar
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
n : ℕ
inst_1 : NeZero n
x : ZMod n
huv :
  (↑(↑(HPow.hPow (α := Circleˣ) ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x) : Circleˣ)
              n) :
          Circle) :
      ℂ) =
    (↑(↑1 : Circle) : ℂ)
⊢ Membership.mem (α := Circleˣ) (γ := Subgroup Circleˣ) (rootsOfUnity n Circle)
    ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x) : Circleˣ)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
n : ℕ
inst_1 : NeZero n
x : ZMod n
⊢ (↑(↑(HPow.hPow (α := Circleˣ) ((toUnits : (a : Circle) → Circleˣ) ((toCircle : (a : ZMod n) → Circle) x) : Circleˣ)
              n) :
          Circle) :
      ℂ) =
    (↑(↑1 : Circle) : ℂ)

Tactic:
simp [← AddChar.map_nsmul_eq_pow]

Premises used: AddChar.map_nsmul_eq_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
n : ℕ
inst_1 : NeZero n
⊢ Eq (α := ↥(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) 0)) ⋯ :
      ↥(rootsOfUnity n Circle))
    (1 : ↥(rootsOfUnity n Circle))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
N : ℕ
inst : NeZero N
n : ℕ
inst_1 : NeZero n
x x_1 : ZMod n
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))) ⋯) :
              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)) ⋯ :
                    ↥(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))) :
              Circleˣ) :
          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 + 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))

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
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))) ⋯) :
              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)) ⋯ :
                    ↥(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))) :
              Circleˣ) :
          Circle) :
      ℂ)

Tactic:
simp [AddChar.map_add_eq_mul]

Premises used: AddChar.map_add_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ Eq (α := Circle)
    ((↑(↑((rootsOfUnityAddChar n : (a : ZMod n) → ↥(rootsOfUnity n Circle)) x) : Circleˣ) : Circle) : Circle)
    ((toCircle : (a : ZMod n) → Circle) x : Circle)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
z : ↥(rootsOfUnity n ℂ)
rw :
  Eq (α := Circle) ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) (z ^ n) : Circle)
    ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) 1 : Circle)
⊢ Membership.mem (α := Circleˣ) (γ := Subgroup Circleˣ) (rootsOfUnity n Circle)
    (((rootsOfUnitytoCircle n).toHomUnits : (a : ↥(rootsOfUnity n ℂ)) → Circleˣ) z : Circleˣ)

Tactic:
rw [mem_rootsOfUnity', MonoidHom.coe_toHomUnits, ← map_pow, ← (rootsOfUnitytoCircle n).map_one]

Premises used: rootsOfUnitytoCircle, MonoidHom.coe_toHomUnits, map_pow, MonoidHom.map_one, mem_rootsOfUnity'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
z : ↥(rootsOfUnity n ℂ)
h : z ^ n = 1
⊢ Eq (α := Circle) ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) (z ^ n) : Circle)
    ((rootsOfUnitytoCircle n : (a : ↥(rootsOfUnity n ℂ)) → Circle) 1 : Circle)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
z : ↥(rootsOfUnity n ℂ)
⊢ z ^ n = 1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
x : ↥(rootsOfUnity n Circle)
⊢ (fun (z : ↥(rootsOfUnity n ℂ)) ↦
        (Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
            (((rootsOfUnitytoCircle n).toHomUnits : (a : ↥(rootsOfUnity n ℂ)) → Circleˣ) z) ⋯ :
          ↥(rootsOfUnity n Circle)))
      (OneHom.toFun
        (↑(MonoidHom.comp (MulEquiv.toMonoidHom (rootsOfUnityUnitsMulEquiv ℂ n))
              (restrictRootsOfUnity Circle.toUnits n)) :
          OneHom ↥(rootsOfUnity n Circle) ↥(rootsOfUnity n ℂ))
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
Goal:
n : ℕ
inst : NeZero n
x : ↥(rootsOfUnity n ℂ)
⊢ OneHom.toFun (M := ↥(rootsOfUnity n Circle))
      (↑(MonoidHom.comp (MulEquiv.toMonoidHom (rootsOfUnityUnitsMulEquiv ℂ n))
            (restrictRootsOfUnity Circle.toUnits n)) :
        OneHom ↥(rootsOfUnity n Circle) ↥(rootsOfUnity n ℂ))
      ((fun (z : ↥(rootsOfUnity n ℂ)) ↦
          (Subtype.mk (p := fun (x : Circleˣ) ↦ Membership.mem (γ := Subgroup Circleˣ) (rootsOfUnity n Circle) x)
              (((rootsOfUnitytoCircle n).toHomUnits : (a : ↥(rootsOfUnity n ℂ)) → Circleˣ) z) ⋯ :
            ↥(rootsOfUnity n Circle)))
        x) =
    x

Tactic:
aesop