awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : CommMonoid M
inst_3 : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
⊢ Finite (MonoidHom.{u_1, u_2} G ↥S)

Tactic:
have : Finite (G →* S) := .of_injective _ DFunLike.coe_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : CommMonoid M
inst_3 : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (MonoidHom.{u_1, u_2} G ↥S)
⊢ Finite (MonoidHom.{u_1, u_2} G Mˣ)

Tactic:
.of_surjective S.subtype.comp fun f ↦ ?_

Premises used: Subgroup.subtype, MonoidHom.comp, Finite.of_surjective
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : CommMonoid M
inst_3 : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (MonoidHom.{u_1, u_2} G ↥S)
refine : ∀ (f : MonoidHom.{u_1, u_2} G Mˣ), ∃ (a : MonoidHom.{u_1, u_2} G ↥S), S.subtype.comp a = f
⊢ Finite (MonoidHom.{u_1, u_2} G Mˣ)

Tactic:
refine .of_surjective S.subtype.comp fun f ↦ ?_
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : CommMonoid M
inst_3 : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (MonoidHom.{u_1, u_2} G ↥S)
f : MonoidHom.{u_1, u_2} G Mˣ
a : G
rw : HPow.hPow (α := Mˣ) ((f : (a : G) → Mˣ) a : Mˣ) (Monoid.exponent G) = 1
rw₁ : Eq.{u_2 + 1} (α := Mˣ) ((f : (a : G) → Mˣ) (a ^ Monoid.exponent G) : Mˣ) (1 : Mˣ)
rw₂ : Eq.{u_2 + 1} (α := Mˣ) ((f : (a : G) → Mˣ) 1) 1
rw₃ rw₄ : Eq.{u_2 + 1} (α := Mˣ) 1 1
⊢ Membership.mem (α := Mˣ) S ((f : (a : G) → Mˣ) a : Mˣ)

Tactic:
rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]

Premises used: mem_rootsOfUnity, map_pow, map_one, Monoid.pow_exponent_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : CommMonoid M
inst_3 : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (MonoidHom.{u_1, u_2} G ↥S)
f : MonoidHom.{u_1, u_2} G Mˣ
⊢ ∀ (a : G), Membership.mem (α := Mˣ) S ((f : (a : G) → Mˣ) a : Mˣ)

Tactic:
have H a : f a ∈ S := by
    rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : CommMonoid M
inst_3 : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (MonoidHom.{u_1, u_2} G ↥S)
f : MonoidHom.{u_1, u_2} G Mˣ
H : ∀ (a : G), Membership.mem (α := Mˣ) S ((f : (a : G) → Mˣ) a : Mˣ)
x : G
⊢ Eq.{u_2 + 1} (α := Mˣ) ((S.subtype.comp (f.codRestrict S H) : (a : G) → Mˣ) x : Mˣ) ((f : (a : G) → Mˣ) x : Mˣ)

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : CommMonoid M
inst_3 : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (MonoidHom.{u_1, u_2} G ↥S)
f : MonoidHom.{u_1, u_2} G Mˣ
H : ∀ (a : G), Membership.mem (α := Mˣ) S ((f : (a : G) → Mˣ) a : Mˣ)
⊢ ∃ (a : MonoidHom.{u_1, u_2} G ↥S), S.subtype.comp a = f

Tactic:
exact ⟨.codRestrict f S H, MonoidHom.ext fun _ ↦ by simp⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
⊢ HPow.hPow (α := R[X]) X (n + 1) - (C : (a : R) → R[X]) 1 =
    ∏ i ∈ range (n + 1), HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ i * 1) : R[X])

Tactic:
have := X_pow_sub_C_eq_prod hμ n.zero_lt_succ (one_pow (n + 1))
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this :
  HPow.hPow (α := R[X]) X (n + 1) - (C : (a : R) → R[X]) 1 =
    ∏ i ∈ range (n + 1), HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ i * 1) : R[X])
⊢ (∏ k ∈ range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ (k + 1) * 1) : R[X])) *
      HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1) =
    (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i) * HSub.hSub (α := R[X]) X 1

Tactic:
rw [C_1, ← mul_geom_sum, prod_range_succ', pow_zero, mul_one, mul_comm, eq_comm] at this

Premises used: Finset.prod_range_succ', Polynomial.C_1, eq_comm, pow_zero, mul_geom_sum, mul_comm, mul_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this :
  (∏ k ∈ range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ (k + 1) * 1) : R[X])) *
      HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1) =
    (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i) * HSub.hSub (α := R[X]) X 1
⊢ Eq.{u_1 + 1} (α := R[X])
    (∏ k ∈ range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ (k + 1) * 1) : R[X]))
    (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i)

Tactic:
replace this := mul_right_cancel₀ (Polynomial.X_sub_C_ne_zero 1) this
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this :
  Eq.{u_1 + 1} (α := R[X])
    (∏ k ∈ range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ (k + 1) * 1) : R[X]))
    (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i)
⊢ Eq.{u_1 + 1} (α := R)
    (eval 1 (∏ k ∈ range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ (k + 1) * 1) : R[X])))
    (eval 1 (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i))

Tactic:
apply_fun Polynomial.eval 1 at this

Premises used: Polynomial.eval, OfNat.ofNat
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this :
  Eq.{u_1 + 1} (α := R)
    (eval 1 (∏ k ∈ range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (μ ^ (k + 1) * 1) : R[X])))
    (eval 1 (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i))
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
simpa only [mul_one, map_pow, eval_prod, eval_sub, eval_X, eval_pow, eval_C, eval_geom_sum,
    one_pow, sum_const, card_range, nsmul_eq_mul, Nat.cast_add, Nat.cast_one] using this

Premises used: one_pow, Polynomial.eval_prod, Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_pow, Finset.card_range, map_pow, Nat.cast_add, nsmul_eq_mul, mul_one, Polynomial.eval_sub, Nat.cast_one, Finset.sum_const, Polynomial.eval_geom_sum
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
rw : HPow.hPow (α := R) (-1) n = HPow.hPow (α := R) (-1) #(range n)
rw₁ rw₂ : HPow.hPow (α := R) (-1) n = HPow.hPow (α := R) (-1) n
⊢ HPow.hPow (α := R) (-1) n = ∏ k ∈ range n, -1

Tactic:
rw [prod_const, card_range]

Premises used: Finset.card_range, Finset.prod_const
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
⊢ HPow.hPow (α := R) (-1) n = ∏ k ∈ range n, -1

Tactic:
have : (-1 : R) ^ n = ∏ k ∈ range n, -1 := by rw [prod_const, card_range]
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : HPow.hPow (α := R) (-1) n = ∏ k ∈ range n, -1
⊢ HPow.hPow (α := R) (-1) n * ∏ k ∈ range n, (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
simp only [this, ← prod_mul_distrib, neg_one_mul, neg_sub, ← prod_one_sub_pow_eq_order hμ]

Premises used: Finset.prod_mul_distrib, neg_sub, IsPrimitiveRoot.prod_one_sub_pow_eq_order, neg_one_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
hn : k < n
μ : R
hμ : IsPrimitiveRoot μ n
let :
  ∀ (n' : ℕ) (hn : k < n' + 1) (hμ : IsPrimitiveRoot μ (n' + 1)),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ (↑(n' + 1) : R) = z * (μ - 1) ^ k
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ (↑n : R) = z * (μ - 1) ^ k

Tactic:
let n' + 1 := n
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
n' : ℕ
hn : k < n' + 1
hμ : IsPrimitiveRoot μ (n' + 1)
obtain :
  ∀ (m : ℕ) (hn : k < m + k + 1) (hμ : IsPrimitiveRoot μ (m + k + 1)),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ (↑(m + k + 1) : R) = z * (μ - 1) ^ k
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ (↑(n' + 1) : R) = z * (μ - 1) ^ k

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.le_of_lt_succ hn)

Premises used: Nat.exists_eq_add_of_le', Nat.le_of_lt_succ, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k_1 n : ℕ
μ : R
m : ℕ
hn : k_1 < m + k_1 + 1
hμ : IsPrimitiveRoot μ (m + k_1 + 1)
k : ℕ
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)

Tactic:
⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩

Premises used: geom_sum_mul, Finset.range, HPow.hPow, And.intro, Exists.intro, Eq.symm, Finset.sum
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k_1 n : ℕ
μ : R
m : ℕ
hn : k_1 < m + k_1 + 1
hμ : IsPrimitiveRoot μ (m + k_1 + 1)
k : ℕ
refine : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∑ x ∈ range k, μ ^ x)
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)

Tactic:
refine ⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k_1 n : ℕ
μ : R
m : ℕ
hn : k_1 < m + k_1 + 1
hμ : IsPrimitiveRoot μ (m + k_1 + 1)
k : ℕ
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∑ x ∈ range k, μ ^ x)

Tactic:
Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _

Premises used: Set.Mem, Algebra.adjoin, Subalgebra.sum_mem, Int, Subalgebra.pow_mem, Singleton.singleton, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k_1 n : ℕ
μ : R
m : ℕ
hn : k_1 < m + k_1 + 1
hμ : IsPrimitiveRoot μ (m + k_1 + 1)
k : ℕ
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∑ x ∈ range k, μ ^ x)

Tactic:
exact Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _

Premises used: Algebra.adjoin, Subalgebra.sum_mem, Subalgebra.pow_mem, Singleton.singleton, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
⊢ ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)

Tactic:
have hdvd k : ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1) := by
    refine ⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩
    exact Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
⊢ ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)

Tactic:
have Zdef k : Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1) :=
    Classical.choose_spec <| hdvd k
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ (↑(m + k + 1) : R) = z * (μ - 1) ^ k

Tactic:
⟨(-1) ^ (m + k) * (∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1),
    ?_, ?_⟩

Premises used: HMul.hMul, HSub.hSub, Finset.Ico, Finset.prod, Finset.range, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
refine_1 :
  Membership.mem (γ := Subalgebra ℤ R) ℤ[μ]
    ((HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))
refine_2 :
  (↑(m + k + 1) : R) =
    ((HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) *
      (μ - 1) ^ k
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ (↑(m + k + 1) : R) = z * (μ - 1) ^ k

Tactic:
refine ⟨(-1) ^ (m + k) * (∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1),
    ?_, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
refine_1 : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1))
refine_1₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ]
    ((HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))

Tactic:
apply Subalgebra.mul_mem

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
refine_1 : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (HPow.hPow (α := R) (-1) (m + k))
refine_1₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ range k, Z (j + 1))
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1))

Tactic:
apply Subalgebra.mul_mem

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (HPow.hPow (α := R) (-1) (m + k))

Tactic:
Subalgebra.pow_mem _ (Subalgebra.neg_mem _ <| Subalgebra.one_mem _) _

Premises used: Set.Mem, Subalgebra.neg_mem, Subalgebra.pow_mem, Subalgebra.one_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (HPow.hPow (α := R) (-1) (m + k))

Tactic:
exact Subalgebra.pow_mem _ (Subalgebra.neg_mem _ <| Subalgebra.one_mem _) _

Premises used: Subalgebra.neg_mem, Subalgebra.pow_mem, Subalgebra.one_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ range k, Z (j + 1))

Tactic:
Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1

Premises used: Set.Mem, Subalgebra.prod_mem, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ range k, Z (j + 1))

Tactic:
exact Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1

Premises used: Subalgebra.prod_mem, And.left
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))

Tactic:
Subalgebra.prod_mem _ fun _ _ ↦ ?_

Premises used: Set.Mem, Subalgebra.prod_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
refine_1 : ∀ x ∈ Ico k (m + k), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1) - 1)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))

Tactic:
refine Subalgebra.prod_mem _ fun _ _ ↦ ?_

Premises used: Subalgebra.prod_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
x : ℕ
h : x ∈ Ico k (m + k)
refine_1 : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1))
refine_1₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] 1
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1) - 1)

Tactic:
apply Subalgebra.sub_mem

Premises used: Subalgebra.sub_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
x : ℕ
h : x ∈ Ico k (m + k)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1))

Tactic:
Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _

Premises used: Set.Mem, Int, Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
x : ℕ
h : x ∈ Ico k (m + k)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1))

Tactic:
exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _

Premises used: Int, Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
x : ℕ
h : x ∈ Ico k (m + k)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] 1

Tactic:
Subalgebra.one_mem _

Premises used: Set.Mem, Subalgebra.one_mem
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
x : ℕ
h : x ∈ Ico k (m + k)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] 1

Tactic:
exact Subalgebra.one_mem _

Premises used: Subalgebra.one_mem