awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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

Tactic:
⟨i, hi, ((isPrimitiveRoot_exp n hn).pow_iff_coprime (Nat.pos_of_ne_zero hn) i).mp h, ?_⟩

Premises used: Complex.isPrimitiveRoot_exp, Nat.pos_of_ne_zero, And.intro, IsPrimitiveRoot.pow_iff_coprime, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i) n
mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i
⊢ ∃ i_1 < n,
    ∃ (_ : i_1.Coprime n),
      cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i_1 : ℂ) (↑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, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i) n
mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp ((↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ)))
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i

Tactic:
rw [← exp_nat_mul]

Premises used: Complex.exp_nat_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i) n
mp : 2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) = (↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ))
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp ((↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ)))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i) n
⊢ 2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) = (↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ))

Tactic:
ring
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
rw : (↑x : ℂ) ^ n = 1 ↔ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
⊢ Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) x ↔
    ∃ 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]

Premises used: Units.ext_iff, Complex.mem_rootsOfUnity, Units.val_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
have hn0 : (n : ℂ) ≠ 0 := mod_cast NeZero.out
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
mp : (↑x : ℂ) ^ n = 1 → ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
mpr : (∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)) → (↑x : ℂ) ^ n = 1
⊢ (↑x : ℂ) ^ n = 1 ↔ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : (↑x : ℂ) ^ n = 1
⊢ ∃ i < n, cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i = (↑x : ℂ)

Tactic:
simpa only using (isPrimitiveRoot_exp n NeZero.out).eq_pow_of_pow_eq_one h

Premises used: Complex.isPrimitiveRoot_exp, NeZero.out, IsPrimitiveRoot.eq_pow_of_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
h : (↑x : ℂ) ^ n = 1
mp :
  ∀ (i : ℕ) (hi : i < n) (H : cexp (2 * (↑π : ℂ) * I / (↑n : ℂ)) ^ i = (↑x : ℂ)),
    ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑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

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Complex.ofReal, Nat.cast, Complex.exp, OfNat.ofNat, Complex.I
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℂ)

Tactic:
⟨i, hi, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℂ)
mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
⊢ ∃ i < n, cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)

Tactic:
refine ⟨i, hi, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℂ)
mp : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp ((↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ)))
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)

Tactic:
rw [← H, ← exp_nat_mul]

Premises used: Complex.exp_nat_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℂ)
mp : 2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) = (↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ))
⊢ cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = cexp ((↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ)))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℂ)
⊢ 2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) = (↑i : ℂ) * (2 * (↑π : ℂ) * I / (↑n : ℂ))

Tactic:
ring
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
i : ℕ
left : i < n
H : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
mpr :
  ∃ (n_1 : ℤ), (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑n_1 : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (↑x : ℂ) ^ n = 1

Tactic:
rw [← H, ← exp_nat_mul, exp_eq_one_iff]

Premises used: Complex.exp_nat_mul, Complex.exp_eq_one_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
i : ℕ
left : i < n
H : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
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:
n : ℕ
inst : NeZero n
x : ℂˣ
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
i : ℕ
left : i < n
H : cexp (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑x : ℂ)
⊢ (↑n : ℂ) * (2 * (↑π : ℂ) * I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = (↑(↑i : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
simp [field]
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
inst : NeZero n
⊢ Fintype.card ↥(rootsOfUnity n ℂ) = n

Tactic:
(isPrimitiveRoot_exp n NeZero.out).card_rootsOfUnity

Premises used: IsPrimitiveRoot.card_rootsOfUnity, Complex.isPrimitiveRoot_exp, NeZero.out
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
k : ℕ
pos : ∀ (h : k = 0), (primitiveRoots k ℂ).card = φ k
neg : ∀ (h : ¬k = 0), (primitiveRoots k ℂ).card = φ k
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
by_cases h : k = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
k : ℕ
h : k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
k : ℕ
h : ¬k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
(isPrimitiveRoot_exp k h).card_primitiveRoots

Premises used: IsPrimitiveRoot.card_primitiveRoots, Complex.isPrimitiveRoot_exp
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
k : ℕ
h : ¬k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
exact (isPrimitiveRoot_exp k h).card_primitiveRoots

Premises used: IsPrimitiveRoot.card_primitiveRoots, Complex.isPrimitiveRoot_exp
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂ
n : ℕ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ‖ζ‖ = 1

Tactic:
Complex.norm_eq_one_of_pow_eq_one h.pow_eq_one hn

Premises used: IsPrimitiveRoot.pow_eq_one, Complex.norm_eq_one_of_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂ
n : ℕ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ‖ζ‖₊ = 1

Tactic:
Subtype.ext <| h.norm'_eq_one hn

Premises used: NNReal, IsPrimitiveRoot.norm'_eq_one, Subtype.ext
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n m : ℕ
ζ μ : ℂ
hζ : IsPrimitiveRoot ζ n
hμ : IsPrimitiveRoot μ m
hn : n ≠ 0
hm : m ≠ 0
h : ζ.arg = μ.arg
⊢ ζ = μ

Tactic:
Complex.ext_norm_arg ((hζ.norm'_eq_one hn).trans (hμ.norm'_eq_one hm).symm) h

Premises used: Complex.ext_norm_arg, IsPrimitiveRoot.norm'_eq_one, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ζ.arg = 0 ↔ ζ = 1

Tactic:
⟨fun h => hζ.arg_ext IsPrimitiveRoot.one hn one_ne_zero (h.trans Complex.arg_one.symm), fun h =>
    h.symm ▸ Complex.arg_one⟩

Premises used: IsPrimitiveRoot.arg_ext, Complex.arg_one, IsPrimitiveRoot.one, Eq.rec, Iff.intro, one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ζ.arg = Real.pi ↔ ζ = -1

Tactic:
⟨fun h =>
    hζ.arg_ext (IsPrimitiveRoot.neg_one 0 two_ne_zero.symm) hn two_ne_zero
      (h.trans Complex.arg_neg_one.symm),
    fun h => h.symm ▸ Complex.arg_neg_one⟩

Premises used: IsPrimitiveRoot.arg_ext, Eq.rec, Ne.symm, two_ne_zero, Complex.arg_neg_one, Iff.intro, IsPrimitiveRoot.neg_one, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
ζ : ℂ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ

Tactic:
rw [Complex.isPrimitiveRoot_iff _ _ hn] at h

Premises used: Complex.isPrimitiveRoot_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
ζ : ℂ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
h₁ :
  ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
⊢ n ≠ 0

Tactic:
rw [Complex.isPrimitiveRoot_iff _ _ hn] at h

Premises used: Complex.isPrimitiveRoot_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
ζ : ℂ
h :
  ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I * HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ)) = ζ
hn : n ≠ 0
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
⊢ ∃ (i : ℤ), ζ.arg = HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧ IsCoprime i (↑n : ℤ) ∧ i.natAbs < n

Tactic:
obtain ⟨i, h, hin, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
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
⊢ ∃ (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:
rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]

Premises used: mul_assoc, mul_comm, Complex.exp_mul_I
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ (if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)).natAbs < n

Tactic:
lia
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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)
refine₁ : IsCoprime (if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑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

Tactic:
refine ⟨if i * 2 ≤ n then i else i - n, ?_, ?isCoprime, by lia⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)

Tactic:
replace hin := Nat.isCoprime_iff_coprime.mpr hin
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
pos : i * 2 ≤ n → IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
neg : ¬i * 2 ≤ n → IsCoprime (HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)
⊢ IsCoprime (if i * 2 ≤ n then (↑i : ℤ) else HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
h_1 : i * 2 ≤ n
⊢ IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)

Tactic:
hin
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
h_1 : i * 2 ≤ n
⊢ IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)

Tactic:
exact hin
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
h_1 : ¬i * 2 ≤ n
⊢ IsCoprime ((↑i : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) (-1)) (↑n : ℤ)

Tactic:
hin.add_mul_left_left (-1)

Premises used: OfNat.ofNat, Neg.neg, IsCoprime.add_mul_left_left
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime (R := ℤ) (↑i : ℤ) (↑n : ℤ)
h_1 : ¬i * 2 ≤ n
h₁ : HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ) = (↑i : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) (-1)
⊢ IsCoprime (HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) (↑n : ℤ)

Tactic:
convert! hin.add_mul_left_left (-1) using 1

Premises used: OfNat.ofNat, Neg.neg, IsCoprime.add_mul_left_left
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℤ))
h₂ h₃ : HAdd.hAdd (α := ℤ) (↑i : ℤ) (-(↑n : ℤ)) = HAdd.hAdd (α := ℤ) (↑i : ℤ) (-(↑n : ℤ))
⊢ HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ) = (↑i : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) (-1)

Tactic:
rw [mul_neg_one, sub_eq_add_neg]

Premises used: sub_eq_add_neg, mul_neg_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℤ)

Tactic:
case isCoprime =>
    replace hin := Nat.isCoprime_iff_coprime.mpr hin
    split_ifs
    · exact hin
    · convert! hin.add_mul_left_left (-1) using 1
      rw [mul_neg_one, sub_eq_add_neg]

Premises used: sub_eq_add_neg, mul_neg_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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)
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)
⊢ (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:
split_ifs with h₂
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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)

Tactic:
Complex.arg_cos_add_sin_mul_I _

Premises used: Complex.arg_cos_add_sin_mul_I
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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)) : ℂ)
pos : HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) 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)

Tactic:
convert! Complex.arg_cos_add_sin_mul_I _

Premises used: Complex.arg_cos_add_sin_mul_I
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
h₁ :
  HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) =
    HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ))
⊢ HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) =
    (↑(HDiv.hDiv (α := ℝ) (↑(↑i : ℤ) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 : ℂ))

Tactic:
rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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

Tactic:
⟨(neg_lt_neg Real.pi_pos).trans_le ?_, ?_⟩

Premises used: neg_lt_neg, Real.pi_pos, LT.lt.trans_le, And.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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)
pos₁ : HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
⊢ -Real.pi < HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ∧
    HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi

Tactic:
refine ⟨(neg_lt_neg Real.pi_pos).trans_le ?_, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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)
⊢ -0 ≤ HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi)

Tactic:
rw [neg_zero]

Premises used: neg_zero
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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)

Tactic:
positivity
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
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 * (HMul.hMul (α := ℝ) (↑i : ℝ) 2 / (↑n : ℝ))

Tactic:
ring
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
pos : Real.pi * (HMul.hMul (α := ℝ) (↑i : ℝ) 2 / (↑n : ℝ)) ≤ Real.pi
⊢ HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi

Tactic:
refine Eq.trans_le (b := Real.pi * (i * 2 / n)) (by ring) ?_

Premises used: Eq.trans_le
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ i * 2 ≤ n * 1

Tactic:
rw [← mul_one n] at h₂

Premises used: mul_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n * 1
⊢ Real.pi * (HMul.hMul (α := ℝ) (↑i : ℝ) 2 / (↑n : ℝ)) ≤ Real.pi

Tactic:
mul_le_of_le_one_right Real.pi_pos.le
      ((div_le_iff₀' <| mod_cast pos_of_gt h).mpr <| mod_cast h₂)

Premises used: Nat.cast_mul._simp_1, Iff.mpr, HMul.hMul, congrArg, cast, mul_le_of_le_one_right, Real.pi_pos, LT.lt.le, Nat.cast_le._simp_1, LE.le, Nat.cast, congr, OfNat.ofNat, Eq.symm, div_le_iff₀', Nat.cast_one, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n * 1
⊢ Real.pi * (HMul.hMul (α := ℝ) (↑i : ℝ) 2 / (↑n : ℝ)) ≤ Real.pi

Tactic:
exact mul_le_of_le_one_right Real.pi_pos.le
      ((div_le_iff₀' <| mod_cast pos_of_gt h).mpr <| mod_cast h₂)

Premises used: Iff.mpr, mul_le_of_le_one_right, Real.pi_pos, LT.lt.le, div_le_iff₀'
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
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)
⊢ (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:
rw [← Complex.cos_sub_two_pi, ← Complex.sin_sub_two_pi]

Premises used: Complex.cos_sub_two_pi, Complex.sin_sub_two_pi
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (Complex.cos (↑(HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ) +
        Complex.sin (↑(HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ) *
          Complex.I).arg =
    HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)

Tactic:
Complex.arg_cos_add_sin_mul_I _

Premises used: Complex.arg_cos_add_sin_mul_I