awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ)) - 2 * (↑Real.pi : ℂ) =
    (↑(HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi)) : ℂ)
neg :
  HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) 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)

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 : ℂ)) - 2 * (↑Real.pi : ℂ) =
    HSub.hSub (α := ℂ) (↑i : ℂ) (↑n : ℂ) / (↑n : ℂ) * (2 * (↑Real.pi : ℂ))
⊢ HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ) =
    (↑(HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑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
h₁ : Ne (α := ℂ) (↑n : ℂ) 0
⊢ HDiv.hDiv (α := ℂ) (↑i : ℂ) (↑n : ℂ) * (2 * (↑Real.pi : ℂ)) - 2 * (↑Real.pi : ℂ) =
    HSub.hSub (α := ℂ) (↑i : ℂ) (↑n : ℂ) / (↑n : ℂ) * (2 * (↑Real.pi : ℂ))

Tactic:
rw [← sub_one_mul, sub_div, div_self]

Premises used: sub_div, div_self, sub_one_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
mod_cast hn

Premises used: congrArg, cast, Ne, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
exact mod_cast hn
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
neg :
  -Real.pi < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ∧
    HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi
⊢ HDiv.hDiv (α := ℝ) (↑(HSub.hSub (α := ℤ) (↑i : ℤ) (↑n : ℤ)) : ℝ) (↑n : ℝ) * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi

Tactic:
simp only [Int.cast_sub, Int.cast_natCast, Set.mem_Ioc]

Premises used: Int.cast_natCast, Int.cast_sub, Set.mem_Ioc
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
neg : -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ∧ HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)
⊢ -Real.pi < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ∧
    HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) / (↑n : ℝ) * (2 * Real.pi) ≤ Real.pi

Tactic:
field_simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
neg : -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2
neg₁ : HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)
⊢ -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ∧ HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ n < i * 2

Tactic:
push Not at h₂

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

Tactic:
rify at h₂
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : (↑n : ℝ) < HMul.hMul (α := ℝ) (↑i : ℝ) 2
⊢ -(↑n : ℝ) < HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2

Tactic:
linear_combination h₂
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ LT.lt (α := ℝ) (↑i : ℝ) (↑n : ℝ)

Tactic:
rify at h
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
n : ℕ
hn : n ≠ 0
i : ℕ
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
h : LT.lt (α := ℝ) (↑i : ℝ) (↑n : ℝ)
⊢ HSub.hSub (α := ℝ) (↑i : ℝ) (↑n : ℝ) * 2 ≤ (↑n : ℝ)

Tactic:
linear_combination 2 * h + (n : ℝ) * one_pos (α := ℝ)

Premises used: Nat.cast, one_pos
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
⊢ ‖(↑ζ : ℂ)‖ = 1

Tactic:
norm_eq_one_of_pow_eq_one ?_ <| NeZero.ne n

Premises used: Complex.norm_eq_one_of_pow_eq_one, NeZero.ne
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
refine : (↑ζ : ℂ) ^ n = 1
⊢ ‖(↑ζ : ℂ)‖ = 1

Tactic:
refine norm_eq_one_of_pow_eq_one ?_ <| NeZero.ne n

Premises used: Complex.norm_eq_one_of_pow_eq_one, NeZero.ne
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
⊢ ζ ^ n = 1

Tactic:
rw [_root_.mem_rootsOfUnity] at hζ

Premises used: mem_rootsOfUnity
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : ζ ^ n = 1
rw : Eq (α := ℂ) (↑1 : ℂ) 1
rw₁ rw₂ : Eq (α := ℂ) 1 1
⊢ (↑(ζ ^ n) : ℂ) = 1

Tactic:
rw [hζ, Units.val_one]

Premises used: Units.val_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Complex
Goal:
ζ : ℂˣ
n : ℕ
inst : NeZero n
hζ : Membership.mem (γ := Subgroup ℂˣ) (rootsOfUnity n ℂ) ζ
rw : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) : ℂ) (↑ζ : ℂ) = 1
rw₁ : HPow.hPow (β := ℕ) (↑‖(↑ζ : ℂ)‖ : ℂ) 2 = 1
rw₂ : HPow.hPow (β := ℕ) (↑1 : ℂ) 2 = 1
rw₃ : HPow.hPow (α := ℂ) (β := ℕ) 1 2 = 1
rw₄ rw₅ : Eq (α := ℂ) 1 1
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (↑ζ : ℂ) = (↑ζ⁻¹ : ℂ)

Tactic:
rw [← Units.mul_eq_one_iff_eq_inv, conj_mul', norm_eq_one_of_mem_rootsOfUnity hζ, ofReal_one,
    one_pow]

Premises used: one_pow, Complex.ofReal_one, Complex.conj_mul', Units.mul_eq_one_iff_eq_inv, Complex.norm_eq_one_of_mem_rootsOfUnity
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hj : j.Coprime n
⊢ Associated (ζ - 1) (ζ ^ j - 1)

Tactic:
associated_of_dvd_dvd ⟨∑ i ∈ range j, ζ ^ i, (mul_geom_sum _ _).symm⟩ ?_

Premises used: associated_of_dvd_dvd, Finset.range, mul_geom_sum, HPow.hPow, Exists.intro, Eq.symm, Finset.sum
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hj : j.Coprime n
refine : ζ ^ j - 1 ∣ ζ - 1
⊢ Associated (ζ - 1) (ζ ^ j - 1)

Tactic:
refine associated_of_dvd_dvd ⟨∑ i ∈ range j, ζ ^ i, (mul_geom_sum _ _).symm⟩ ?_

Premises used: associated_of_dvd_dvd, Finset.range, mul_geom_sum, HPow.hPow, Exists.intro, Eq.symm, Finset.sum
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ 0
hj : j.Coprime 0
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ 1
hj : j.Coprime 1
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n_1 j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
⊢ 1 < n + 2

Tactic:
lia
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n_1 j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
obtain : ∀ (m : ℕ) (hm : j * m % (n + 2) = 1), ζ ^ j - 1 ∣ ζ - 1
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hj (by lia)

Premises used: Nat.exists_mul_mod_eq_one_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n_1 j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
m : ℕ
hm : j * m % (n + 2) = 1
h : ζ - 1 = (ζ ^ j - 1) * ∑ i ∈ range m, (ζ ^ j) ^ i
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
use ∑ i ∈ range m, (ζ ^ j) ^ i

Premises used: Finset.range, HPow.hPow
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n_1 j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
m : ℕ
hm : j * m % (n + 2) = 1
h : ζ - 1 = (ζ ^ j) ^ m - 1
h₁ : ζ - 1 = ζ ^ (j * m) - 1
h₂ : ζ - 1 = ζ ^ (j * m % orderOf ζ) - 1
h₃ : ζ - 1 = ζ ^ (j * m % (n + 2)) - 1
h₄ : ζ - 1 = HPow.hPow (β := ℕ) ζ 1 - 1
h₅ h₆ : ζ - 1 = ζ - 1
⊢ ζ - 1 = (ζ ^ j - 1) * ∑ i ∈ range m, (ζ ^ j) ^ i

Tactic:
rw [mul_geom_sum, ← pow_mul, ← pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]

Premises used: IsPrimitiveRoot.eq_orderOf, pow_mod_orderOf, pow_mul, mul_geom_sum, pow_one
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hj : j.Coprime n
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
match n with
  | 0 => simp_all
  | 1 => simp_all
  | n + 2 =>
      obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hj (by lia)
      use ∑ i ∈ range m, (ζ ^ j) ^ i
      rw [mul_geom_sum, ← pow_mul, ← pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n i j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
this : ∀ {j : ℕ}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1)
⊢ Associated (ζ ^ j - 1) (ζ ^ i - 1)

Tactic:
grind [Associated.trans, Associated.symm]

Premises used: Associated.trans, Associated.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n i j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
suffices : ∀ {j : ℕ}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1)
⊢ Associated (ζ ^ j - 1) (ζ ^ i - 1)

Tactic:
suffices ∀ {j}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1) by
    grind [Associated.trans, Associated.symm]
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n i j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
j_1 : ℕ
⊢ j_1.Coprime n → Associated (ζ - 1) (ζ ^ j_1 - 1)

Tactic:
hζ.associated_sub_one_pow_sub_one_of_coprime

Premises used: IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n i j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1)

Tactic:
exact hζ.associated_sub_one_pow_sub_one_of_coprime

Premises used: IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
rw :
  Associated (ζ - 1)
    (ζ ^ ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n) -
      1)
⊢ Associated (ζ - 1) ((σ : (a : A) → A) (ζ - 1))

Tactic:
rw [map_sub, map_one, ← hζ.autToPow_spec R σ]

Premises used: map_sub, map_one, IsPrimitiveRoot.autToPow_spec
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
apply :
  (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n)).Coprime
    n
⊢ Associated (ζ - 1)
    (ζ ^ ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n) -
      1)

Tactic:
apply hζ.associated_sub_one_pow_sub_one_of_coprime

Premises used: IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
⊢ (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n)).Coprime
    n

Tactic:
ZMod.val_coe_unit_coprime ((autToPow R hζ) σ)

Premises used: ZMod.val_coe_unit_coprime, IsPrimitiveRoot.autToPow, DFunLike.coe
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
⊢ (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n)).Coprime
    n

Tactic:
exact ZMod.val_coe_unit_coprime ((autToPow R hζ) σ)

Premises used: ZMod.val_coe_unit_coprime, IsPrimitiveRoot.autToPow, DFunLike.coe
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
rw :
  Associated
    (ζ ^ ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n) -
      1)
    (ζ ^ ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) τ) : ZMod n) -
      1)
⊢ Associated (M := A) ((σ : (a : A) → A) (ζ - 1) : A) ((τ : (a : A) → A) (ζ - 1) : A)

Tactic:
rw [map_sub, map_sub, map_one, map_one, ← hζ.autToPow_spec R σ, ← hζ.autToPow_spec R τ]

Premises used: map_sub, map_one, IsPrimitiveRoot.autToPow_spec
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
hi :
  (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) τ) : ZMod n)).Coprime
    n
hj :
  (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n)).Coprime
    n
⊢ Associated
    (ζ ^ ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n) -
      1)
    (ζ ^ ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) τ) : ZMod n) -
      1)

Tactic:
apply hζ.associated_pow_sub_one_pow_of_coprime

Premises used: IsPrimitiveRoot.associated_pow_sub_one_pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) τ) : ZMod n)).Coprime
    n

Tactic:
ZMod.val_coe_unit_coprime ((autToPow R hζ) _)

Premises used: ZMod.val_coe_unit_coprime, IsPrimitiveRoot.autToPow, DFunLike.coe
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) τ) : ZMod n)).Coprime
    n

Tactic:
exact ZMod.val_coe_unit_coprime ((autToPow R hζ) _)

Premises used: ZMod.val_coe_unit_coprime, IsPrimitiveRoot.autToPow, DFunLike.coe
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n)).Coprime
    n

Tactic:
ZMod.val_coe_unit_coprime ((autToPow R hζ) _)

Premises used: ZMod.val_coe_unit_coprime, IsPrimitiveRoot.autToPow, DFunLike.coe
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
R : Type u_3
inst_2 : CommRing R
inst_3 : Algebra R A
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (ZMod.val (n := n) (↑(((autToPow R hζ : (A ≃ₐ[R] A) →* (ZMod n)ˣ) : (a : A ≃ₐ[R] A) → (ZMod n)ˣ) σ) : ZMod n)).Coprime
    n

Tactic:
exact ZMod.val_coe_unit_coprime ((autToPow R hζ) _)

Premises used: ZMod.val_coe_unit_coprime, IsPrimitiveRoot.autToPow, DFunLike.coe
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hj : j.Coprime n
obtain :
  ∀ (u : Aˣ) (hu : (HPow.hPow (β := ℕ) ζ 1 - 1) * (↑u : A) = ζ ^ j - 1), IsUnit.{u_1} (M := A) (∑ i ∈ range j, ζ ^ i)
⊢ IsUnit.{u_1} (M := A) (∑ i ∈ range j, ζ ^ i)

Tactic:
obtain ⟨u, hu⟩ := hζ.associated_pow_sub_one_pow_of_coprime hj (coprime_one_left n)

Premises used: Nat.coprime_one_left, IsPrimitiveRoot.associated_pow_sub_one_pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hj : j.Coprime n
u : Aˣ
hu : (HPow.hPow (β := ℕ) ζ 1 - 1) * (↑u : A) = ζ ^ j - 1
⊢ IsUnit (↑u : A)

Tactic:
u.isUnit

Premises used: Units.isUnit
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hj : j.Coprime n
u : Aˣ
hu : (HPow.hPow (β := ℕ) ζ 1 - 1) * (↑u : A) = ζ ^ j - 1
h : ∑ i ∈ range j, ζ ^ i = (↑u : A)
⊢ IsUnit.{u_1} (M := A) (∑ i ∈ range j, ζ ^ i)

Tactic:
convert! u.isUnit

Premises used: Units.isUnit
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hj : j.Coprime n
u : Aˣ
hu : (HPow.hPow (β := ℕ) ζ 1 - 1) * (↑u : A) = ζ ^ j - 1
⊢ 1 - ζ ≠ 0

Tactic:
grind [sub_one_ne_zero]

Premises used: IsPrimitiveRoot.sub_one_ne_zero
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hj : j.Coprime n
u : Aˣ
hu : (HPow.hPow (β := ℕ) ζ 1 - 1) * (↑u : A) = ζ ^ j - 1
h : Eq.{u_1 + 1} (α := A) ((fun (x : A) ↦ (1 - ζ) * x) (∑ i ∈ range j, ζ ^ i)) ((fun (x : A) ↦ (1 - ζ) * x) (↑u : A))
⊢ ∑ i ∈ range j, ζ ^ i = (↑u : A)

Tactic:
apply mul_right_injective₀ (show 1 - ζ ≠ 0 by grind [sub_one_ne_zero])

Premises used: mul_right_injective₀
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hj : j.Coprime n
u : Aˣ
hu : (HPow.hPow (β := ℕ) ζ 1 - 1) * (↑u : A) = ζ ^ j - 1
⊢ Eq.{u_1 + 1} (α := A) ((fun (x : A) ↦ (1 - ζ) * x) (∑ i ∈ range j, ζ ^ i)) ((fun (x : A) ↦ (1 - ζ) * x) (↑u : A))

Tactic:
grind [mul_neg_geom_sum]

Premises used: mul_neg_geom_sum
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hj_Unit : IsUnit.{u_1} (M := A) (↑j : A)
hζ : IsPrimitiveRoot ζ 0
hj : j.Coprime 0
⊢ IsUnit.{u_1} (M := A) (∑ i ∈ range j, ζ ^ i)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hj_Unit : IsUnit.{u_1} (M := A) (↑j : A)
hζ : IsPrimitiveRoot ζ 1
hj : j.Coprime 1
⊢ IsUnit.{u_1} (M := A) (∑ i ∈ range j, ζ ^ i)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n_1 j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hj_Unit : IsUnit.{u_1} (M := A) (↑j : A)
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
linarith : n + 2 < 2 → -1 + HSub.hSub (α := ℤ) 0 (↑n : ℤ) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1 - 2) = 0
⊢ 2 ≤ n + 2

Tactic:
linarith
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n_1 j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hj_Unit : IsUnit.{u_1} (M := A) (↑j : A)
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
⊢ IsUnit.{u_1} (M := A) (∑ i ∈ range j, ζ ^ i)

Tactic:
exact geom_sum_isUnit hζ (by linarith) hj

Premises used: IsPrimitiveRoot.geom_sum_isUnit
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hj : j.Coprime n
hj_Unit : IsUnit.{u_1} (M := A) (↑j : A)
⊢ IsUnit.{u_1} (M := A) (∑ i ∈ range j, ζ ^ i)

Tactic:
match n with
  | 0 => simp_all
  | 1 => simp_all
  | n + 2 => exact geom_sum_isUnit hζ (by linarith) hj
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n i j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hi : i.Coprime n
hj : j.Coprime n
⊢ ζ ^ j - 1 = (↑⋯.unit : A) * (↑⋯.unit⁻¹ : A) * (ζ ^ i - 1)

Tactic:
grind [IsUnit.mul_val_inv, pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum, IsUnit.unit_spec]

Premises used: IsUnit.mul_val_inv, pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum, IsUnit.unit_spec
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
i : ℕ
hjn : j.Coprime n
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
i : ℕ
hjn : j.Coprime n
h : (ζ - 1) * (↑(⋯.unit ^ i * ⋯.unit) : A) = ζ ^ (i + j) - ζ ^ i
⊢ Associated (ζ - 1) (ζ ^ (i + j) - ζ ^ i)

Tactic:
use (hζ.isUnit (by lia)).unit ^ i * (hζ.geom_sum_isUnit hn hjn).unit

Premises used: IsPrimitiveRoot.geom_sum_isUnit, IsPrimitiveRoot.isUnit, IsUnit.unit
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
i : ℕ
hjn : j.Coprime n
this : (ζ - 1) * ζ ^ i * ∑ i ∈ range j, ζ ^ i = ζ ^ (i + j) - ζ ^ i
⊢ (ζ - 1) * (↑(⋯.unit ^ i * ⋯.unit) : A) = ζ ^ (i + j) - ζ ^ i

Tactic:
simp [← this, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
i : ℕ
hjn : j.Coprime n
h : (ζ - 1) * ζ ^ i * ∑ i ∈ range j, ζ ^ i = ζ ^ (i + j) - ζ ^ i
⊢ (ζ - 1) * (↑(⋯.unit ^ i * ⋯.unit) : A) = ζ ^ (i + j) - ζ ^ i

Tactic:
suffices (ζ - 1) * ζ ^ i * ∑ i ∈ range j, ζ ^ i = (ζ ^ (i + j) - ζ ^ i) by
    simp [← this, mul_assoc]
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
n j : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
i : ℕ
hjn : j.Coprime n
⊢ (ζ - 1) * ζ ^ i * ∑ i ∈ range j, ζ ^ i = ζ ^ (i + j) - ζ ^ i

Tactic:
grind [mul_geom_sum]

Premises used: mul_geom_sum
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ (↑(nthRootsFinset p 1) : Set A)
η₂ : A
hη₂ : η₂ ∈ (↑(nthRootsFinset p 1) : Set A)
e : η₁ ≠ η₂
⊢ NeZero p

Tactic:
have : NeZero p := ⟨hp.ne_zero⟩