awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
⊢ Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) x ↔
    ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
have rw : (↑x : ℂ) ^ n = 1 ↔ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
Tactic: rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
⊢ (↑x : ℂ) ^ n = 1 ↔ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
have hn0 : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: have hn0 : (n : ℂ) ≠ 0 := mod_cast NeZero.out
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
⊢ (↑x : ℂ) ^ n = 1 ↔ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
have mp : (↑x : ℂ) ^ n = 1 → ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
mp : (↑x : ℂ) ^ n = 1 → ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
⊢ (↑x : ℂ) ^ n = 1 ↔ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
have mpr : (∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)) → (↑x : ℂ) ^ n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : (↑x : ℂ) ^ n = 1
⊢ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
have mp : ∀ (i : ℕ) (hi : i < n) (H : cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i = (↑x : ℂ)),
  ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
Tactic: obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x := by
      simpa only using (isPrimitiveRoot_exp n NeZero.out).eq_pow_of_pow_eq_one h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : (↑x : ℂ) ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i = (↑x : ℂ)
⊢ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
have mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
Tactic: refine ⟨i, hi, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : (↑x : ℂ) ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i = (↑x : ℂ)
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
have mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp ((↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ)))
Tactic: rw [← H, ← exp_nat_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : (↑x : ℂ) ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i = (↑x : ℂ)
⊢ 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
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
i : ℕ
left : i < n
H : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
⊢ (↑x : ℂ) ^ n = 1
have mpr : ∃ (n_1 : ℤ), (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: rw [← H, ← exp_nat_mul, exp_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
i : ℕ
left : i < n
H : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
⊢ ∃ (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:
k : ℕ
⊢ (primitiveRoots k ℂ).card = φ k
have pos : ∀ (h : k = 0), (primitiveRoots k ℂ).card = φ k
Tactic: by_cases h : k = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
k : ℕ
pos : ∀ (h : k = 0), (primitiveRoots k ℂ).card = φ k
⊢ (primitiveRoots k ℂ).card = φ k
have neg : ∀ (h : ¬k = 0), (primitiveRoots k ℂ).card = φ k
Tactic: by_cases h : k = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
n : ℕ
ζ : ℂ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ∃ (i : ℤ), ζ.arg = HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧ IsCoprime i (↑n : ℤ) ∧ i.natAbs < n
have h₁ : ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
Tactic: rw [Complex.isPrimitiveRoot_iff _ _ hn] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
ζ : ℂ
h :
  ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
hn : n ≠ 0
⊢ ∃ (i : ℤ), ζ.arg = HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧ IsCoprime i (↑n : ℤ) ∧ i.natAbs < n
have obtain : ∀ (i : ℕ) (h : i < n) (hin : i.Coprime n),
  ∃ (i_1 : ℤ),
    (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ))).arg =
        HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
      IsCoprime i_1 (↑n : ℤ) ∧ i_1.natAbs < n
Tactic: obtain ⟨i, h, hin, rfl⟩ := h
Cleared hypotheses: ζ, h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ ∃ (i_1 : ℤ),
    (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ))).arg =
        HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
      IsCoprime i_1 (↑n : ℤ) ∧ i_1.natAbs < n
have rw : ∃ (i_1 : ℤ),
  (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
          Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
      HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
    IsCoprime i_1 (↑n : ℤ) ∧ i_1.natAbs < n
Tactic: rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ ∃ (i_1 : ℤ),
    (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
            Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
        HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
      IsCoprime i_1 (↑n : ℤ) ∧ i_1.natAbs < n
have refine : (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
      Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
  HDiv.hDiv (α := ℝ) (↑(if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) *
    (2 * Real.pi)
Tactic: refine ⟨if i * 2 ≤ n then i else i - n, ?_, ?isCoprime, by lia⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
refine :
  (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) *
      (2 * Real.pi)
⊢ ∃ (i_1 : ℤ),
    (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
            Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
        HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
      IsCoprime i_1 (↑n : ℤ) ∧ i_1.natAbs < n
have refine₁ : IsCoprime (if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)
Tactic: refine ⟨if i * 2 ≤ n then i else i - n, ?_, ?isCoprime, by lia⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ IsCoprime (if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)
have hin₁ : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
Tactic: replace hin := Nat.isCoprime_iff_coprime.mpr hin
Cleared hypotheses: hin
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
⊢ IsCoprime (if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)
have pos : i * 2 ≤ n → IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
pos : i * 2 ≤ n → IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
⊢ IsCoprime (if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)
have neg : ¬i * 2 ≤ n → IsCoprime (HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
h_1 : ¬i * 2 ≤ n
⊢ IsCoprime (HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)
have h₁ : HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ) = (↑i : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) (-1)
Tactic: convert! hin.add_mul_left_left (-1) using 1
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
h_1 : ¬i * 2 ≤ n
⊢ HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ) = (↑i : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) (-1)
have h₁ : HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ) = HAdd.hAdd (α := ℤ) (↑i : ℤ) (-(↑n : ℤ))
Tactic: rw [mul_neg_one, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
h_1 : ¬i * 2 ≤ n
h₁ : HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ) = HAdd.hAdd (α := ℤ) (↑i : ℤ) (-(↑n : ℤ))
⊢ HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ) = (↑i : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) (-1)
have h₂ : HAdd.hAdd (α := ℤ) (↑i : ℤ) (-(↑n : ℤ)) = HAdd.hAdd (α := ℤ) (↑i : ℤ) (-(↑n : ℤ))
Tactic: rw [mul_neg_one, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) *
      (2 * Real.pi)
have pos : ∀ (h₂ : i * 2 ≤ n),
  (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)
Tactic: split_ifs with h₂
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
pos :
  ∀ (h₂ : i * 2 ≤ n),
    (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
          Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
      HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)
⊢ (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) *
      (2 * Real.pi)
have neg : ∀ (h₂ : ¬i * 2 ≤ n),
  (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)
Tactic: split_ifs with h₂
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)
have h₁ : HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) =
  (↑(HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)
Tactic: convert! Complex.arg_cos_add_sin_mul_I _
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
h₁ h₃ :
  HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) =
    (↑(HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)
⊢ (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)
have pos : HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
Tactic: convert! Complex.arg_cos_add_sin_mul_I _
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) =
    (↑(HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)
have h₁ : HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) =
  HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ -Real.pi < HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
    HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
have pos : -0 ≤ HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi)
Tactic: refine ⟨(neg_lt_neg Real.pi_pos).trans_le ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
pos : -0 ≤ HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi)
⊢ -Real.pi < HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
    HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
have pos₁ : HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
Tactic: refine ⟨(neg_lt_neg Real.pi_pos).trans_le ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ -0 ≤ HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi)
have pos : 0 ≤ HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi)
Tactic: rw [neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
have pos : Real.pi * (HMul.hMul (α := ℝ) (↑i : ℝ) 2 / (↑n : ℝ)) ≤ Real.pi
Tactic: refine Eq.trans_le (b := Real.pi * (i * 2 / n)) (by ring) ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ Real.pi * (HMul.hMul (α := ℝ) (↑i : ℝ) 2 / (↑n : ℝ)) ≤ Real.pi
have h₃ : i * 2 ≤ n * 1
Tactic: rw [← mul_one n] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))) * Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)
have neg : (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ)) +
      Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ)) * Complex.I).arg =
  HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)
Tactic: rw [← Complex.cos_sub_two_pi, ← Complex.sin_sub_two_pi]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ)) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ)) *
          Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)
have h₁ : HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ) =
  (↑(HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)
Tactic: convert! Complex.arg_cos_add_sin_mul_I _
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
h₁ h₃ :
  HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ) =
    (↑(HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)
⊢ (Complex.cos (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ)) +
        Complex.sin (HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ)) *
          Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)
have neg : HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
Tactic: convert! Complex.arg_cos_add_sin_mul_I _
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ) =
    (↑(HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)
have h₁ : HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ) =
  HSub.hSub (α := ℂ) (↑i : ℂ) (↑n : ℂ) / (↑n : ℂ) * (2 * (↑Real.pi : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ) =
    HSub.hSub (α := ℂ) (↑i : ℂ) (↑n : ℂ) / (↑n : ℂ) * (2 * (↑Real.pi : ℂ))
have h₁ : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: rw [← sub_one_mul, sub_div, div_self]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
have neg : -Real.pi < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ∧
  HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
Tactic: simp only [Int.cast_sub, Int.cast_natCast, Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ∧
    HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
have neg : -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ∧ HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ∧ HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)
have neg : -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
neg : -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2
⊢ -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ∧ HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)
have neg₁ : HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2
have h₃ : n < i * 2
Tactic: push Not at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : n < i * 2
⊢ -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2
have h₃ : (↑n : ℝ) < HMul.hMul (α := ℝ) (↑i : ℝ) 2
Tactic: rify at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)
have h₁ : LT.lt (α := ℝ) (↑i : ℝ) (↑n : ℝ)
Tactic: rify at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
⊢ ‖(↑ζ : ℂ)‖ = 1
have refine : (↑ζ : ℂ) ^ n = 1
Tactic: refine norm_eq_one_of_pow_eq_one ?_ <| NeZero.ne n
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (hypothesis)
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
⊢ (↑(ζ ^ n) : ℂ) = 1
have hζ₁ : ζ ^ n = 1
Tactic: rw [_root_.mem_rootsOfUnity] at hζ
Cleared hypotheses: hζ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : ζ ^ n = 1
⊢ (↑(ζ ^ n) : ℂ) = 1
have rw : Eq (α := ℂ) (↑1 : ℂ) 1
Tactic: rw [hζ, Units.val_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : ζ ^ n = 1
rw : Eq (α := ℂ) (↑1 : ℂ) 1
⊢ (↑(ζ ^ n) : ℂ) = 1
have rw₁ : Eq (α := ℂ) 1 1
Tactic: rw [hζ, Units.val_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) = (↑ζ⁻¹ : ℂ)
have rw : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) : ℂ) (↑ζ : ℂ) = 1
Tactic: rw [← Units.mul_eq_one_iff_eq_inv, conj_mul', norm_eq_one_of_mem_rootsOfUnity hζ, ofReal_one,
    one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
rw : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) : ℂ) (↑ζ : ℂ) = 1
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) = (↑ζ⁻¹ : ℂ)
have rw₁ : HPow.hPow (β := ℕ) (↑‖(↑ζ : ℂ)‖ : ℂ) 2 = 1
Tactic: rw [← Units.mul_eq_one_iff_eq_inv, conj_mul', norm_eq_one_of_mem_rootsOfUnity hζ, ofReal_one,
    one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Complex (goal)
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
rw : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) : ℂ) (↑ζ : ℂ) = 1
rw₁ : HPow.hPow (β := ℕ) (↑‖(↑ζ : ℂ)‖ : ℂ) 2 = 1
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) = (↑ζ⁻¹ : ℂ)
have rw₂ : HPow.hPow (β := ℕ) (↑1 : ℂ) 2 = 1
Tactic: rw [← Units.mul_eq_one_iff_eq_inv, conj_mul', norm_eq_one_of_mem_rootsOfUnity hζ, ofReal_one,
    one_pow]