awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Basic (goal)
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
rw : HPow.hPow (α := Rˣ) ((f : (a : L) → Rˣ) a : Rˣ) (Monoid.exponent L) = 1
rw₁ : Eq.{u_4 + 1} (α := Rˣ) ((f : (a : L) → Rˣ) (a ^ Monoid.exponent L) : Rˣ) (1 : Rˣ)
⊢ Membership.mem (α := Rˣ) S ((f : (a : L) → Rˣ) a : Rˣ)
have rw₂ : Eq.{u_4 + 1} (α := Rˣ) ((f : (a : L) → Rˣ) 1) 1
Tactic: rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Basic (goal)
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
rw : HPow.hPow (α := Rˣ) ((f : (a : L) → Rˣ) a : Rˣ) (Monoid.exponent L) = 1
rw₁ : Eq.{u_4 + 1} (α := Rˣ) ((f : (a : L) → Rˣ) (a ^ Monoid.exponent L) : Rˣ) (1 : Rˣ)
rw₂ : Eq.{u_4 + 1} (α := Rˣ) ((f : (a : L) → Rˣ) 1) 1
⊢ Membership.mem (α := Rˣ) S ((f : (a : L) → Rˣ) a : Rˣ)
have rw₃ : Eq.{u_4 + 1} (α := Rˣ) 1 1
Tactic: rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Basic (hypothesis)
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 : MonoidHom.{u_7, u_4} L ↥S), (fun (f : MonoidHom.{u_7, u_4} L ↥S) ↦ S.subtype.comp f) a = f
have H : ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
ζ : Rˣ
⊢ ζ ^ (p ^ k * m) = 1 ↔ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ
have rw : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (p ^ k * m) R) ζ ↔
  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ
Tactic: rw [← mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Basic (goal)
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) ζ
⊢ ζ ^ (p ^ k * m) = 1 ↔ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ
have rw₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ ↔ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity m R) ζ
Tactic: rw [← mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
inst_1 : IsCyclic G
G' : Type u_8
inst_2 : CommGroup G'
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))
have obtain : ∀ (g : G) (hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x),
  Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ))) n
have rw : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ n = 1 ∧
  ∀ (l : ℕ), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ l = 1 → n ∣ l
Tactic: rw [IsPrimitiveRoot.iff_def]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ n = 1 ∧
    ∀ (l : ℕ), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) ^ l = 1 → n ∣ l
have 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
Tactic: simp only [← exp_nat_mul, exp_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ (∃ (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
have left : ∃ (n_1 : ℤ), (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
left :
  ∃ (n_1 : ℤ), (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (∃ (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
have right : ∀ (l : ℕ),
  (∃ (n_1 : ℤ),
      (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) →
    n ∣ l
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ ∃ (n_1 : ℤ), (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)
have h : (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑i : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: use i
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ ∀ (l : ℕ),
    (∃ (n_1 : ℤ),
        (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)) →
      n ∣ l
have right : ∀ (l : ℕ) (x : ℤ)
  (h : (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ) * (2 * (↑π : ℂ) * I)), n ∣ l
Tactic: simp only [forall_exists_index]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i (↑n : ℤ)
⊢ ∀ (l : ℕ) (x : ℤ)
    (h : (↑l : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ) * (2 * (↑π : ℂ) * I)), n ∣ l
have hn0 : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: have hn0 : (n : ℂ) ≠ 0 := mod_cast h0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
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)
⊢ n ∣ l
have hk₁ : HMul.hMul (α := ℂ) (↑l : ℂ) (↑i : ℂ) = HMul.hMul (α := ℂ) (↑n : ℂ) (↑k : ℂ)
Tactic: field_simp at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
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 : ℂ)
⊢ n ∣ l
have hk₁ : (↑l : ℤ) * i = (↑n : ℤ) * k
Tactic: norm_cast at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
⊢ IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I * (↑q : ℂ))) q.den
have h : (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
Tactic: convert!
    isPrimitiveRoot_exp_of_isCoprime _ _ q.den_nz <| Int.isCoprime_iff_nat_coprime.mpr q.reduced
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
have h : (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)
Tactic: nth_rw 1 [← Rat.num_div_den q]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Even q.num
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) q.den
have have : ∀ (n : ℤ) (hn : q.num = HSMul.hSMul (α := ℕ) 2 n), IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) q.den
Tactic: have ⟨n, hn⟩ := even_iff_exists_two_nsmul _ |>.mp h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) q.den
have h₁ : cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))
Tactic: convert! isPrimitiveRoot_exp_rat (n / q.den) using 1
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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 : ℚ)) : ℂ))
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) q.den
have h₂ : q.den = (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)).den
Tactic: convert! isPrimitiveRoot_exp_rat (n / q.den) using 1
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))
have h₁ : cexp ((↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑((↑2 : ℤ) * n) : ℚ) (↑q.den : ℚ)) : ℂ)) =
  cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))
Tactic: nth_rw 1 [← q.num_div_den, hn, Int.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ cexp ((↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑((↑2 : ℤ) * n) : ℚ) (↑q.den : ℚ)) : ℂ)) =
    cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)) : ℂ))
have h₁ : cexp ((↑π : ℂ) * I * (HMul.hMul (α := ℂ) 2 (↑n : ℂ) / (↑q.den : ℂ))) =
  cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑n : ℂ) (↑q.den : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ q.den = (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑q.den : ℚ)).den
have rw : n.natAbs.Coprime q.den
Tactic: rw [← Int.cast_natCast, ← Rat.divInt_eq_div, ← Rat.mk_eq_divInt (nz := by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ n.natAbs.Coprime q.den
have apply : (2 * n.natAbs).Coprime q.den
Tactic: apply Nat.Coprime.coprime_mul_left (k := 2)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = HSMul.hSMul (α := ℕ) 2 n
⊢ (2 * n.natAbs).Coprime q.den
have h₁ : 2 * n.natAbs = q.num.natAbs
Tactic: convert! q.reduced
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Odd q.num
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) (2 * q.den)
have h₁ : cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(q / 2) : ℂ))
Tactic: convert! isPrimitiveRoot_exp_rat (q / 2) using 1
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Odd q.num
h₁ : cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(q / 2) : ℂ))
⊢ IsPrimitiveRoot (cexp ((↑π : ℂ) * I * (↑q : ℂ))) (2 * q.den)
have h₂ : 2 * q.den = (q / 2).den
Tactic: convert! isPrimitiveRoot_exp_rat (q / 2) using 1
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Odd q.num
⊢ cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑(q / 2) : ℂ))
have h₁ : cexp ((↑π : ℂ) * I * (↑q : ℂ)) = cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑q : ℂ) 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (q / 2).den
have h₁ : 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
Tactic: nth_rw 2 [← q.num_div_den]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₁ : q.den * 2 = (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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
q : ℚ
h : Odd q.num
h₁ : q.den * 2 = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₂ : q.den * 2 = ((↑q.num : ℚ) / HMul.hMul (α := ℚ) (↑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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₃ : q.den * 2 = ((↑q.num : ℚ) / HMul.hMul (α := ℚ) (↑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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₄ : q.den * 2 = ((↑q.num : ℚ) / HMul.hMul (α := ℚ) (↑(↑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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₅ : q.den * 2 = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑(HMul.hMul (α := ℤ) (↑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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₆ : q.den * 2 = (Rat.divInt q.num (HMul.hMul (α := ℤ) (↑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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₇ : q.den * 2 = (Rat.divInt q.num (HMul.hMul (α := ℤ) (↑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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₈ : q.den * 2 = (Rat.divInt 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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
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
⊢ 2 * q.den = (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) / 2).den
have h₉ : q.den * 2 = { num := q.num, den := q.den * 2, den_nz := sorry, reduced := sorry }.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)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
have hn0 : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: have hn0 : (n : ℂ) ≠ 0 := mod_cast hn
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
have mp : IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
mp :
  IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
have mpr : (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ) → IsPrimitiveRoot ζ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : IsPrimitiveRoot ζ n
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
have this : NeZero n
Tactic: have : NeZero n := ⟨hn⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : IsPrimitiveRoot ζ n
this : NeZero n
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
have 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
Tactic: obtain ⟨i, hi, rfl⟩ :=
    (isPrimitiveRoot_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one
Cleared hypotheses: ζ, h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
this : NeZero n
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
have mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i
Tactic: refine ⟨i, hi, ((isPrimitiveRoot_exp n hn).pow_iff_coprime (Nat.pos_of_ne_zero hn) i).mp h, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i) n
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i
have mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp ((↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ)))
Tactic: rw [← exp_nat_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i) n
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp ((↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ)))
have mp : 2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) = (↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ))
Tactic: congr 1