awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S_1 : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
L : Type u_7
inst_6 : LeftCancelMonoid L
inst_7 : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (MonoidHom.{u_7, u_4} L ↥S)
f : MonoidHom.{u_7, u_4} L Rˣ
⊢ ∀ (a : L), Membership.mem (α := Rˣ) S ((f : (a : L) → Rˣ) a : Rˣ)

Tactic:
have H a : f a ∈ S := by
    rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S_1 : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
L : Type u_7
inst_6 : LeftCancelMonoid L
inst_7 : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (MonoidHom.{u_7, u_4} L ↥S)
f : MonoidHom.{u_7, u_4} L Rˣ
H : ∀ (a : L), Membership.mem (α := Rˣ) S ((f : (a : L) → Rˣ) a : Rˣ)
x : L
⊢ Eq.{u_4 + 1} (α := Rˣ)
    ((((fun (f : MonoidHom.{u_7, u_4} L ↥S) ↦ S.subtype.comp f) (f.codRestrict S H) : MonoidHom.{u_7, u_4} L Rˣ) :
          (a : L) → Rˣ)
        x :
      Rˣ)
    ((f : (a : L) → Rˣ) x : Rˣ)

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S_1 : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
L : Type u_7
inst_6 : LeftCancelMonoid L
inst_7 : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (MonoidHom.{u_7, u_4} L ↥S)
f : MonoidHom.{u_7, u_4} L Rˣ
H : ∀ (a : L), Membership.mem (α := Rˣ) S ((f : (a : L) → Rˣ) a : Rˣ)
⊢ ∃ (a : MonoidHom.{u_7, u_4} L ↥S), (fun (f : MonoidHom.{u_7, u_4} L ↥S) ↦ S.subtype.comp f) a = f

Tactic:
exact ⟨.codRestrict f S H, MonoidHom.ext fun _ ↦ by simp⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
ζ : Rˣ
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (p ^ k * m) R) ζ ↔
    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ

Tactic:
simp only [mem_rootsOfUnity', ExpChar.pow_prime_pow_mul_eq_one_iff]

Premises used: ExpChar.pow_prime_pow_mul_eq_one_iff, mem_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
ζ : Rˣ
rw :
  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (p ^ k * m) R) ζ ↔
    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ
rw₁ rw₂ :
  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ ↔ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ
⊢ ζ ^ (p ^ k * m) = 1 ↔ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ

Tactic:
rw [← mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff]

Premises used: mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G_1
G : Type u_7
inst_3 : CommGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
G' : Type u_8
inst_4 : CommGroup G'
φ : G →* G'
⊢ Membership.mem (γ := Subgroup G'ˣ) (rootsOfUnity (Nat.card G) G') (IsUnit.unit (a := (φ : (a : G) → G') g) ⋯)

Tactic:
simp only [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec,
      ← map_pow, pow_card_eq_one', map_one, Units.val_one]

Premises used: mem_rootsOfUnity, Units.ext_iff, map_pow, pow_card_eq_one', map_one, Units.val_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G_1
G : Type u_7
inst_3 : CommGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
G' : Type u_8
inst_4 : CommGroup G'
ζ : ↥(rootsOfUnity (Nat.card G) G')
⊢ orderOf (↑(↑ζ : G'ˣ) : G') ∣ orderOf g

Tactic:
simpa only [orderOf_eq_card_of_forall_mem_zpowers hg, orderOf_dvd_iff_pow_eq_one,
      ← Units.val_pow_eq_pow_val, Units.val_eq_one] using ζ.prop

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Subtype.prop, Units.val_eq_one, Units.val_pow_eq_pow_val, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G_1
G : Type u_7
inst_3 : CommGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
G' : Type u_8
inst_4 : CommGroup G'
φ : G →* G'
⊢ Eq.{u_8 + 1} (α := G')
    (((fun (ζ : ↥(rootsOfUnity (Nat.card G) G')) ↦ monoidHomOfForallMemZpowers hg ⋯)
            ((fun (φ : G →* G') ↦
                Subtype.mk (p := fun (x : G'ˣ) ↦ Membership.mem (γ := Subgroup G'ˣ) (rootsOfUnity (Nat.card G) G') x)
                  (IsUnit.unit (a := (φ : (a : G) → G') g) ⋯) ⋯)
              φ) :
          (a : G) → G')
        g :
      G')
    ((φ : (a : G) → G') g : G')

Tactic:
simp only [IsUnit.unit_spec, monoidHomOfForallMemZpowers_apply_gen]

Premises used: monoidHomOfForallMemZpowers_apply_gen, IsUnit.unit_spec
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G_1
G : Type u_7
inst_3 : CommGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
G' : Type u_8
inst_4 : CommGroup G'
φ : ↥(rootsOfUnity (Nat.card G) G')
⊢ (↑((fun (φ : G →* G') ↦
            Subtype.mk (p := fun (x : G'ˣ) ↦ Membership.mem (γ := Subgroup G'ˣ) (rootsOfUnity (Nat.card G) G') x)
              (IsUnit.unit (a := (φ : (a : G) → G') g) ⋯) ⋯)
          ((fun (ζ : ↥(rootsOfUnity (Nat.card G) G')) ↦ monoidHomOfForallMemZpowers hg ⋯) φ)) :
      G'ˣ) =
    (↑φ : G'ˣ)

Tactic:
simp only [monoidHomOfForallMemZpowers_apply_gen, IsUnit.unit_of_val_units]

Premises used: monoidHomOfForallMemZpowers_apply_gen, IsUnit.unit_of_val_units
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G_1
G : Type u_7
inst_3 : CommGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
G' : Type u_8
inst_4 : CommGroup G'
x y : G →* G'
⊢ Subtype.mk (p := fun (x : G'ˣ) ↦ Membership.mem (γ := Subgroup G'ˣ) (rootsOfUnity (Nat.card G) G') x)
      (IsUnit.unit (a := (x * y : (a : G) → G') g) ⋯) ⋯ =
    Subtype.mk (p := fun (x : G'ˣ) ↦ Membership.mem (γ := Subgroup G'ˣ) (rootsOfUnity (Nat.card G) G') x)
        (IsUnit.unit (a := (x : (a : G) → G') g) ⋯) ⋯ *
      Subtype.mk (p := fun (x : G'ˣ) ↦ Membership.mem (γ := Subgroup G'ˣ) (rootsOfUnity (Nat.card G) G') x)
        (IsUnit.unit (a := (y : (a : G) → G') g) ⋯) ⋯

Tactic:
simp only [MonoidHom.mul_apply, MulMemClass.mk_mul_mk, Subtype.mk.injEq, Units.ext_iff,
      IsUnit.unit_spec, Units.val_mul]

Premises used: Units.ext_iff, Subtype.mk.injEq, MulMemClass.mk_mul_mk, IsUnit.unit_spec, Units.val_mul, MonoidHom.mul_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
G : Type u_7
inst : CommGroup G
inst_1 : IsCyclic G
G' : Type u_8
inst_2 : CommGroup G'
obtain :
  ∀ (g : G) (hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x),
    Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
G : Type u_7
inst : CommGroup G
inst_1 : IsCyclic G
G' : Type u_8
inst_2 : CommGroup G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

Tactic:
⟨monoidHomMulEquivRootsOfUnityOfGenerator hg G'⟩

Premises used: Nonempty.intro, IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
G : Type u_7
inst : CommGroup G
inst_1 : IsCyclic G
G' : Type u_8
inst_2 : CommGroup G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

Tactic:
exact ⟨monoidHomMulEquivRootsOfUnityOfGenerator hg G'⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
rw :
  cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ n = 1 ∧
    ∀ (l : ℕ), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ l = 1 → n ∣ l
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ))) n

Tactic:
rw [IsPrimitiveRoot.iff_def]

Premises used: IsPrimitiveRoot.iff_def
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
simp :
  (∃ (n_1 : ℤ),
      (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) ∧
    ∀ (l : ℕ),
      (∃ (n_1 : ℤ),
          (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) →
        n ∣ l
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ n = 1 ∧
    ∀ (l : ℕ), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ l = 1 → n ∣ l

Tactic:
simp only [← exp_nat_mul, exp_eq_one_iff]

Premises used: Complex.exp_nat_mul, Complex.exp_eq_one_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
left :
  ∃ (n_1 : ℤ), (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)
right :
  ∀ (l : ℕ),
    (∃ (n_1 : ℤ),
        (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) →
      n ∣ l
⊢ (∃ (n_1 : ℤ),
      (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) ∧
    ∀ (l : ℕ),
      (∃ (n_1 : ℤ),
          (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) →
        n ∣ l

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
h : (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑i : ℂ) * (2 * (↑π : ℂ) * I)
⊢ ∃ (n_1 : ℤ), (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
use i
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑i : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
simp (discharger := norm_cast) [field]
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
right :
  ∀ (l : ℕ) (x : ℤ)
    (h : (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ) * (2 * (↑π : ℂ) * I)), n ∣ l
⊢ ∀ (l : ℕ),
    (∃ (n_1 : ℤ),
        (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) →
      n ∣ l

Tactic:
simp only [forall_exists_index]

Premises used: forall_exists_index
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
have hn0 : (n : ℂ) ≠ 0 := mod_cast h0
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
l : ℕ
k : ℤ
hk : (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑k : ℂ) * (2 * (↑π : ℂ) * I)
⊢ HMul.hMul (α := ℂ) (↑l : ℂ) (↑i : ℂ) = HMul.hMul (α := ℂ) (↑n : ℂ) (↑k : ℂ)

Tactic:
field_simp at hk
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
l : ℕ
k : ℤ
hk : HMul.hMul (α := ℂ) (↑l : ℂ) (↑i : ℂ) = HMul.hMul (α := ℂ) (↑n : ℂ) (↑k : ℂ)
⊢ (↑l : ℤ) * i = (↑n : ℤ) * k

Tactic:
norm_cast at hk
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
l : ℕ
k : ℤ
hk : (↑l : ℤ) * i = (↑n : ℤ) * k
⊢ n ∣ l

Tactic:
Int.natCast_dvd_natCast.mp <| hi.symm.dvd_of_dvd_mul_right <| hk ▸ dvd_mul_right ..

Premises used: IsCoprime.symm, Eq.rec, IsCoprime.dvd_of_dvd_mul_right, Iff.mp, dvd_mul_right, Eq.symm, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
l : ℕ
k : ℤ
hk : (↑l : ℤ) * i = (↑n : ℤ) * k
⊢ n ∣ l

Tactic:
exact Int.natCast_dvd_natCast.mp <| hi.symm.dvd_of_dvd_mul_right <| hk ▸ dvd_mul_right ..

Premises used: IsCoprime.symm, IsCoprime.dvd_of_dvd_mul_right, Iff.mp, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ))) n

Tactic:
isPrimitiveRoot_exp_of_isCoprime _ _ h0 hi.isCoprime

Premises used: Complex.isPrimitiveRoot_exp_of_isCoprime, Nat.Coprime.isCoprime
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ))) q.den

Tactic:
isPrimitiveRoot_exp_of_isCoprime _ _ q.den_nz <| Int.isCoprime_iff_nat_coprime.mpr q.reduced

Premises used: Iff.mpr, Rat.reduced, Int.isCoprime_iff_nat_coprime, Complex.isPrimitiveRoot_exp_of_isCoprime, Rat.den_nz
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * (↑q : ℂ))) q.den

Tactic:
convert!
    isPrimitiveRoot_exp_of_isCoprime _ _ q.den_nz <| Int.isCoprime_iff_nat_coprime.mpr q.reduced

Premises used: Iff.mpr, Int.isCoprime_iff_nat_coprime, Complex.isPrimitiveRoot_exp_of_isCoprime, Rat.den_nz
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)

Tactic:
nth_rw 1 [← Rat.num_div_den q]

Premises used: Rat.num_div_den
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
⊢ (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
have : ∀ (n : ℤ) (hn : q.num = HSMul.hSMul (α := ℕ) 2 n), IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) q.den
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) q.den

Tactic:
have ⟨n, hn⟩ := even_iff_exists_two_nsmul _ |>.mp h
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ)))
    (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)).den

Tactic:
isPrimitiveRoot_exp_rat (n / q.den)

Premises used: Int.cast, Complex.isPrimitiveRoot_exp_rat, Rat.den, HDiv.hDiv, Nat.cast
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
h₁ : cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))
h₂ : q.den = (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)).den
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) q.den

Tactic:
convert! isPrimitiveRoot_exp_rat (n / q.den) using 1

Premises used: Int.cast, Complex.isPrimitiveRoot_exp_rat, Rat.den, HDiv.hDiv, Nat.cast
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
h₁ :
  cexp ((↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑((↑2 : ℤ) * n) : ℚ) (↑q.den : ℚ)) : ℂ)) =
    cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))
⊢ cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))

Tactic:
nth_rw 1 [← q.num_div_den, hn, Int.nsmul_eq_mul]

Premises used: Rat.num_div_den, Int.nsmul_eq_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
h₁ :
  cexp ((↑π : ℂ) * I * (HMul.hMul (α := ℂ) 2 (↑n : ℂ) / (↑q.den : ℂ))) =
    cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑n : ℂ) (↑q.den : ℂ))
⊢ cexp ((↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑((↑2 : ℤ) * n) : ℚ) (↑q.den : ℚ)) : ℂ)) =
    cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))

Tactic:
push_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ cexp ((↑π : ℂ) * I * (HMul.hMul (α := ℂ) 2 (↑n : ℂ) / (↑q.den : ℂ))) =
    cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑n : ℂ) (↑q.den : ℂ))

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ q.den ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
rw : n.natAbs.Coprime q.den
⊢ q.den = (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)).den

Tactic:
rw [← Int.cast_natCast, ← Rat.divInt_eq_div, ← Rat.mk_eq_divInt (nz := by simp)]

Premises used: Int.cast_natCast, Rat.mk_eq_divInt, Rat.divInt_eq_div
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
apply : (2 * n.natAbs).Coprime q.den
⊢ n.natAbs.Coprime q.den

Tactic:
apply Nat.Coprime.coprime_mul_left (k := 2)

Premises used: Nat.Coprime.coprime_mul_left
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ q.num.natAbs.Coprime q.den

Tactic:
q.reduced

Premises used: Rat.reduced
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
h₁ : 2 * n.natAbs = q.num.natAbs
⊢ (2 * n.natAbs).Coprime q.den

Tactic:
convert! q.reduced

Premises used: Rat.reduced
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ 2 * n.natAbs = q.num.natAbs

Tactic:
grind
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Odd q.num
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * (↑(q / 2) : ℂ))) (q / 2).den

Tactic:
isPrimitiveRoot_exp_rat (q / 2)

Premises used: Complex.isPrimitiveRoot_exp_rat, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Odd q.num
h₁ : cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(q / 2) : ℂ))
h₂ : 2 * q.den = (q / 2).den
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) (2 * q.den)

Tactic:
convert! isPrimitiveRoot_exp_rat (q / 2) using 1

Premises used: Complex.isPrimitiveRoot_exp_rat, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Odd q.num
h₁ : cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑q : ℂ) 2)
⊢ cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(q / 2) : ℂ))

Tactic:
push_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Odd q.num
⊢ cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑q : ℂ) 2)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Odd q.num
h₁ : 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
⊢ 2 * q.den = (q / 2).den

Tactic:
nth_rw 2 [← q.num_div_den]

Premises used: Rat.num_div_den
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Odd q.num
⊢ q.den * 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
q : ℚ
h : Odd q.num
h₁ : q.den * 2 = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
h₂ : q.den * 2 = ((↑q.num : ℚ) / HMul.hMul (α := ℚ) (↑q.den : ℚ) 2).den
h₃ : q.den * 2 = ((↑q.num : ℚ) / HMul.hMul (α := ℚ) (↑q.den : ℚ) (↑2 : ℚ)).den
h₄ : q.den * 2 = ((↑q.num : ℚ) / HMul.hMul (α := ℚ) (↑(↑q.den : ℤ) : ℚ) (↑2 : ℚ)).den
h₅ : q.den * 2 = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) 2) : ℚ)).den
h₆ : q.den * 2 = (Rat.divInt q.num (HMul.hMul (α := ℤ) (↑q.den : ℤ) 2)).den
h₇ : q.den * 2 = (Rat.divInt q.num (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑2 : ℤ))).den
h₈ : q.den * 2 = (Rat.divInt q.num (↑(q.den * 2) : ℤ)).den
h₉ h₁₀ : q.den * 2 = { num := q.num, den := q.den * 2, den_nz := ⋯, reduced := ⋯ }.den
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den

Tactic:
rw [mul_comm, div_div, ← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul,
      ← Rat.divInt_eq_div, ← Nat.cast_ofNat (R := ℤ), ← Nat.cast_mul,
      ← Rat.mk_eq_divInt (nz := by simp)
        (c := Nat.Coprime.mul_right q.reduced h.natAbs.coprime_two_right)]

Premises used: Nat.cast_ofNat, Int.cast_natCast, Rat.mk_eq_divInt, Rat.divInt_eq_div, Int.cast_ofNat, Int.cast_mul, Nat.cast_mul, mul_comm, div_div
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
h0 : n ≠ 0
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ))) n

Tactic:
simpa only [Nat.cast_one, one_div] using
    isPrimitiveRoot_exp_of_coprime 1 n h0 n.coprime_one_left

Premises used: Nat.coprime_one_left, Complex.isPrimitiveRoot_exp_of_coprime, one_div, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
have hn0 : (n : ℂ) ≠ 0 := mod_cast hn
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
mp :
  IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
mpr :
  (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ) →
    IsPrimitiveRoot ζ n
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
i : ℕ
hi : i.Coprime n
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ))) n

Tactic:
isPrimitiveRoot_exp_of_coprime i n hn hi

Premises used: Complex.isPrimitiveRoot_exp_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
i : ℕ
hi : i.Coprime n
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ))) n

Tactic:
exact isPrimitiveRoot_exp_of_coprime i n hn hi

Premises used: Complex.isPrimitiveRoot_exp_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : IsPrimitiveRoot ζ n
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : IsPrimitiveRoot ζ n
this : NeZero n
mp :
  ∀ (i : ℕ) (hi : i < n) (h : IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i) n),
    ∃ i_1 < n,
      ∃ (_ : i_1.Coprime n),
        cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i_1 : ℂ) (↑n : ℂ)) = cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ

Tactic:
obtain ⟨i, hi, rfl⟩ :=
    (isPrimitiveRoot_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one

Premises used: Complex.isPrimitiveRoot_exp, IsPrimitiveRoot.eq_pow_of_pow_eq_one, IsPrimitiveRoot.pow_eq_one, rfl