awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommMonoid R
inst_4 : CommMonoid S
inst_5 : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
a :
  (↑(↑(((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
              (((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                  (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
                ξ)) :
          Sˣ) :
      S) =
    (↑(↑ξ : Sˣ) : S)
⊢ ((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
        (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
      (((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
          (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
        ξ) =
    ξ

Tactic:
ext
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommMonoid R
inst_4 : CommMonoid S
inst_5 : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
⊢ (↑(↑(((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
              (((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                  (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
                ξ)) :
          Sˣ) :
      S) =
    (↑(↑ξ : Sˣ) : S)

Tactic:
σ.apply_symm_apply _

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommMonoid R
inst_4 : CommMonoid S
inst_5 : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
⊢ (↑(↑(((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
              (((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                  (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
                ξ)) :
          Sˣ) :
      S) =
    (↑(↑ξ : Sˣ) : S)

Tactic:
exact σ.apply_symm_apply _

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
S : Type u_5
k : ℕ
inst : CommMonoid R
inst_1 : CommMonoid S
σ : R ≃* S
ζ : ↥(rootsOfUnity k R)
⊢ Eq.{u_5 + 1} (α := S)
    ((↑(↑((σ.restrictRootsOfUnity k : (a : ↥(rootsOfUnity k R)) → ↥(rootsOfUnity k S)) ζ) : Sˣ) : S) : S)
    ((σ : (a : R) → S) (↑(↑ζ : Rˣ) : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
S : Type u_5
k : ℕ
inst : CommMonoid R
inst_1 : CommMonoid S
σ : R ≃* S
⊢ (σ.restrictRootsOfUnity k).symm = σ.symm.restrictRootsOfUnity k

Tactic:
rfl

Premises used: MulEquiv.restrictRootsOfUnity, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : CommMonoid R
inst_1 : NeZero k
h : ∀ (x : R), x ∈ val '' (↑(rootsOfUnity k R) : Set Rˣ) ↔ Membership.mem (γ := Set R) {z : R | z ^ k = 1} x
⊢ val '' (↑(rootsOfUnity k R) : Set Rˣ) = {z : R | z ^ k = 1}

Tactic:
ext x
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : CommMonoid R
inst_1 : NeZero k
x : R
h : x ∈ val '' (↑(rootsOfUnity k R) : Set Rˣ)
y : Rˣ
hy1 : y ∈ (↑(rootsOfUnity k R) : Set Rˣ)
hy2 : (↑y : R) = x
rw : Membership.mem (γ := Set R) {z : R | z ^ k = 1} (↑y : R)
⊢ Membership.mem (γ := Set R) {z : R | z ^ k = 1} x

Tactic:
rw [← hy2]
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : CommMonoid R
inst_1 : NeZero k
x : R
h : x ∈ val '' (↑(rootsOfUnity k R) : Set Rˣ)
y : Rˣ
hy1 : y ∈ (↑(rootsOfUnity k R) : Set Rˣ)
hy2 : (↑y : R) = x
⊢ Membership.mem (γ := Set R) {z : R | z ^ k = 1} (↑y : R)

Tactic:
(mem_rootsOfUnity' k y).mp hy1

Premises used: Set.Mem, setOf, Iff.mp, mem_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : CommMonoid R
inst_1 : NeZero k
x : R
h : x ∈ val '' (↑(rootsOfUnity k R) : Set Rˣ)
y : Rˣ
hy1 : y ∈ (↑(rootsOfUnity k R) : Set Rˣ)
hy2 : (↑y : R) = x
⊢ Membership.mem (γ := Set R) {z : R | z ^ k = 1} (↑y : R)

Tactic:
exact (mem_rootsOfUnity' k y).mp hy1

Premises used: Iff.mp, mem_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : CommMonoid R
inst_1 : NeZero k
x : R
⊢ x ∈ val '' (↑(rootsOfUnity k R) : Set Rˣ) ↔ Membership.mem (γ := Set R) {z : R | z ^ k = 1} x

Tactic:
exact ⟨fun ⟨y,hy1,hy2⟩ => by rw [← hy2]; exact (mem_rootsOfUnity' k y).mp hy1,
    fun h ↦ ⟨(rootsOfUnity.mkOfPowEq x h), ⟨Subtype.coe_prop (rootsOfUnity.mkOfPowEq x h), rfl⟩⟩⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
inst : CommMonoid R
⊢ val '' (↑(rootsOfUnity 1 R) : Set Rˣ) = {1}

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
inst : CommRing R
inst_1 : NoZeroDivisors R
h : ∀ (x : R), x ∈ val '' (↑(rootsOfUnity 2 R) : Set Rˣ) ↔ Membership.mem (γ := Set R) {1, -1} x
⊢ val '' (↑(rootsOfUnity 2 R) : Set Rˣ) = {1, -1}

Tactic:
ext x
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
inst : CommRing R
inst_1 : NoZeroDivisors R
x : R
⊢ x ∈ val '' (↑(rootsOfUnity 2 R) : Set Rˣ) ↔ Membership.mem (γ := Set R) {1, -1} x

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
inst : CommRing R
k : ℕ
ζ : Rˣ
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) ζ ↔ (HPow.hPow (α := R[X]) X k - 1).IsRoot (↑ζ : R)

Tactic:
simp [-mem_rootsOfUnity, mem_rootsOfUnity', sub_eq_zero]

Premises used: mem_rootsOfUnity, sub_eq_zero, mem_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
ζ : Rˣ
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) ζ ↔ Membership.mem (γ := Multiset R) (nthRoots k 1) (↑ζ : R)

Tactic:
simp only [mem_rootsOfUnity, mem_nthRoots (NeZero.pos k), Units.ext_iff, Units.val_one,
    Units.val_pow_eq_pow_val]

Premises used: mem_rootsOfUnity, Units.ext_iff, Units.val_one, NeZero.pos, Units.val_pow_eq_pow_val, Polynomial.mem_nthRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x }
refine_1 : (↑x : R) * (↑x : R) ^ (k - 1) = 1
refine_2 : (↑x : R) ^ (k - 1) * (↑x : R) = 1
refine_3 :
  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R)
    { val := (↑x : R), inv := (↑x : R) ^ (k - 1), val_inv := ⋯, inv_val := ⋯ }
⊢ ↥(rootsOfUnity k R)

Tactic:
refine ⟨⟨x, ↑x ^ (k - 1 : ℕ), ?_, ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x }
refine_1 :
  ∀ (x : R) (hx : Membership.mem (γ := Multiset R) (nthRoots k 1) x),
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx) : R) *
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx) : R) ^ (k - 1) =
      1
⊢ (↑x : R) * (↑x : R) ^ (k - 1) = 1

Tactic:
rcases x with ⟨x, hx⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : R
hx : Membership.mem (γ := Multiset R) (nthRoots k 1) x
⊢ x ^ k = 1

Tactic:
rw [mem_nthRoots <| NeZero.pos k] at hx

Premises used: NeZero.pos, Polynomial.mem_nthRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : R
hx_1 : Membership.mem (γ := Multiset R) (nthRoots k 1) x
hx : x ^ k = 1
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx_1) : R) *
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx_1) : R) ^ (k - 1) =
    1

Tactic:
simp only [← pow_succ, ← pow_succ', hx, tsub_add_cancel_of_le NeZero.one_le]

Premises used: pow_succ, tsub_add_cancel_of_le, NeZero.one_le, pow_succ'
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x }
refine_2 :
  ∀ (x : R) (hx : Membership.mem (γ := Multiset R) (nthRoots k 1) x),
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx) : R) ^ (k - 1) *
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx) : R) =
      1
⊢ (↑x : R) ^ (k - 1) * (↑x : R) = 1

Tactic:
rcases x with ⟨x, hx⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : R
hx_1 : Membership.mem (γ := Multiset R) (nthRoots k 1) x
hx : x ^ k = 1
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx_1) : R) ^ (k - 1) *
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx_1) : R) =
    1

Tactic:
simp only [← pow_succ, ← pow_succ', hx, tsub_add_cancel_of_le NeZero.one_le]

Premises used: pow_succ, tsub_add_cancel_of_le, NeZero.one_le, pow_succ'
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x }
refine_3 :
  ∀ (x : R) (hx : Membership.mem (γ := Multiset R) (nthRoots k 1) x),
    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R)
      { val := (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx) : R),
        inv :=
          (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx) : R) ^ (k - 1),
        val_inv := ⋯, inv_val := ⋯ }
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R)
    { val := (↑x : R), inv := (↑x : R) ^ (k - 1), val_inv := ⋯, inv_val := ⋯ }

Tactic:
rcases x with ⟨x, hx⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : R
hx_1 : Membership.mem (γ := Multiset R) (nthRoots k 1) x
hx : x ^ k = 1
refine_3 :
  Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) { val := x, inv := x ^ (k - 1), val_inv := ⋯, inv_val := ⋯ }
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R)
    { val := (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx_1) : R),
      inv :=
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Multiset R) (nthRoots k 1) x) x hx_1) : R) ^ (k - 1),
      val_inv := ⋯, inv_val := ⋯ }

Tactic:
simp only [← pow_succ, ← pow_succ', hx, tsub_add_cancel_of_le NeZero.one_le]

Premises used: pow_succ, tsub_add_cancel_of_le, NeZero.one_le, pow_succ'
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
x : R
hx_1 : Membership.mem (γ := Multiset R) (nthRoots k 1) x
hx : x ^ k = 1
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) { val := x, inv := x ^ (k - 1), val_inv := ⋯, inv_val := ⋯ }

Tactic:
simp only [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, hx, Units.val_one]

Premises used: mem_rootsOfUnity, Units.ext_iff, Units.val_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
x : ↥(rootsOfUnity k R)
⊢ (↑((rootsOfUnityEquivNthRoots R k : (a : ↥(rootsOfUnity k R)) → { x : R // x ∈ nthRoots k 1 }) x) : R) =
    (↑(↑x : Rˣ) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
x : { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x }
⊢ (↑(↑((Equiv.symm (rootsOfUnityEquivNthRoots R k) : (a : { x : R // x ∈ nthRoots k 1 }) → ↥(rootsOfUnity k R)) x) :
          Rˣ) :
      R) =
    (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
⊢ Fintype ↥(rootsOfUnity k R)

Tactic:
exact Fintype.ofEquiv { x // x ∈ nthRoots k (1 : R) } (rootsOfUnityEquivNthRoots R k).symm

Premises used: Membership.mem, Subtype, Fintype.ofEquiv, Polynomial.nthRoots, rootsOfUnityEquivNthRoots, Equiv.symm, OfNat.ofNat
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
⊢ Fintype ↥(rootsOfUnity k R)

Tactic:
classical
  exact Fintype.ofEquiv { x // x ∈ nthRoots k (1 : R) } (rootsOfUnityEquivNthRoots R k).symm
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
⊢ IsCyclic.{u_4} ↥(rootsOfUnity k R)

Tactic:
isCyclic_of_injective_ringHom ((Units.coeHom R).comp (rootsOfUnity k R).subtype) coe_injective

Premises used: Units.coeHom, rootsOfUnity.coe_injective, Subgroup.subtype, MonoidHom.comp, rootsOfUnity, isCyclic_of_injective_ringHom
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
⊢ Fintype.card.{u_4} ↥(rootsOfUnity k R) =
    Fintype.card.{u_4} { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x }

Tactic:
Fintype.card_congr (rootsOfUnityEquivNthRoots R k)

Premises used: Fintype.card_congr, rootsOfUnityEquivNthRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
⊢ Fintype.card.{u_4} { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x } ≤
    Multiset.card.{u_4} (α := { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x })
      (Multiset.attach (nthRoots k 1))

Tactic:
Multiset.card_le_card (Multiset.dedup_le _)

Premises used: Multiset.card_le_card, Fintype.card, Multiset.dedup_le, Finset.card
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
⊢ Multiset.card.{u_4} (α := { x : R // Membership.mem (γ := Multiset R) (nthRoots k 1) x })
      (Multiset.attach (nthRoots k 1)) =
    Multiset.card.{u_4} (α := R) (nthRoots k 1)

Tactic:
Multiset.card_attach

Premises used: Multiset.card_attach
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
⊢ Multiset.card.{u_4} (α := R) (nthRoots k 1) ≤ k

Tactic:
card_nthRoots k 1

Premises used: Polynomial.card_nthRoots, OfNat.ofNat
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
⊢ Fintype.card.{u_4} ↥(rootsOfUnity k R) ≤ k

Tactic:
calc
    Fintype.card (rootsOfUnity k R) = Fintype.card { x // x ∈ nthRoots k (1 : R) } :=
      Fintype.card_congr (rootsOfUnityEquivNthRoots R k)
    _ ≤ Multiset.card (nthRoots k (1 : R)).attach := Multiset.card_le_card (Multiset.dedup_le _)
    _ = Multiset.card (nthRoots k (1 : R)) := Multiset.card_attach
    _ ≤ k := card_nthRoots k 1

Premises used: Fintype.card_congr, Multiset.card_le_card, Membership.mem, Polynomial.card_nthRoots, Fintype.card, Subtype, Multiset.card_attach, rootsOfUnity, Polynomial.nthRoots, Multiset.dedup_le, rootsOfUnityEquivNthRoots, Multiset.card, OfNat.ofNat, Multiset.attach
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
⊢ Fintype.card.{u_4} ↥(rootsOfUnity k R) ≤ k

Tactic:
classical
  calc
    Fintype.card (rootsOfUnity k R) = Fintype.card { x // x ∈ nthRoots k (1 : R) } :=
      Fintype.card_congr (rootsOfUnityEquivNthRoots R k)
    _ ≤ Multiset.card (nthRoots k (1 : R)).attach := Multiset.card_le_card (Multiset.dedup_le _)
    _ = Multiset.card (nthRoots k (1 : R)) := Multiset.card_attach
    _ ≤ k := card_nthRoots k 1

Premises used: Multiset.card_le_card, Membership.mem, Polynomial.card_nthRoots, Fintype.card, Subtype, Multiset.card_attach, rootsOfUnity, Polynomial.nthRoots, Multiset.dedup_le, Multiset.card, OfNat.ofNat, Multiset.attach
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
F : Type u_6
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike F R R
inst_4 : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
obtain :
  ∀ (m : ℤ)
    (hm :
      ∀ (g : ↥(rootsOfUnity k R)),
        (restrictRootsOfUnity σ k : (a : ↥(rootsOfUnity k R)) → ↥(rootsOfUnity k R)) g = g ^ m),
    ∃ (m : ℕ), (σ : (a : R) → R) (↑(↑ζ : Rˣ) : R) = (↑(↑ζ : Rˣ) : R) ^ m
⊢ ∃ (m : ℕ), (σ : (a : R) → R) (↑(↑ζ : Rˣ) : R) = (↑(↑ζ : Rˣ) : R) ^ m

Tactic:
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k)

Premises used: MonoidHom.map_cyclic, restrictRootsOfUnity
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
F : Type u_6
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike F R R
inst_4 : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k : (a : ↥(rootsOfUnity k R)) → ↥(rootsOfUnity k R)) g = g ^ m
rw : ∃ (m_1 : ℕ), (↑(↑ζ : Rˣ) : R) ^ (m % (↑(orderOf ζ) : ℤ)).toNat = (↑(↑ζ : Rˣ) : R) ^ m_1
⊢ ∃ (m : ℕ), (σ : (a : R) → R) (↑(↑ζ : Rˣ) : R) = (↑(↑ζ : Rˣ) : R) ^ m

Tactic:
rw [← restrictRootsOfUnity_coe_apply, hm, ← zpow_mod_orderOf, ← Int.toNat_of_nonneg
      (m.emod_nonneg (Int.natCast_ne_zero.mpr (pos_iff_ne_zero.mp (orderOf_pos ζ)))),
    zpow_natCast, rootsOfUnity.coe_pow]

Premises used: zpow_natCast, Iff.mpr, Int.natCast_ne_zero, zpow_mod_orderOf, Int.toNat_of_nonneg, Iff.mp, rootsOfUnity.coe_pow, restrictRootsOfUnity_coe_apply, orderOf_pos, pos_iff_ne_zero, Int.emod_nonneg
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
F : Type u_6
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike F R R
inst_4 : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k : (a : ↥(rootsOfUnity k R)) → ↥(rootsOfUnity k R)) g = g ^ m
⊢ ∃ (m_1 : ℕ), (↑(↑ζ : Rˣ) : R) ^ (m % (↑(orderOf ζ) : ℤ)).toNat = (↑(↑ζ : Rˣ) : R) ^ m_1

Tactic:
⟨(m % orderOf ζ).toNat, rfl⟩

Premises used: Nat.cast, orderOf, HMod.hMod, Exists.intro, Int.toNat, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
F : Type u_6
k : ℕ
inst : NeZero k
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike F R R
inst_4 : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k : (a : ↥(rootsOfUnity k R)) → ↥(rootsOfUnity k R)) g = g ^ m
⊢ ∃ (m_1 : ℕ), (↑(↑ζ : Rˣ) : R) ^ (m % (↑(orderOf ζ) : ℤ)).toNat = (↑(↑ζ : Rˣ) : R) ^ m_1

Tactic:
exact ⟨(m % orderOf ζ).toNat, rfl⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S_1 : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
L : Type u_7
inst_6 : LeftCancelMonoid L
inst_7 : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
⊢ Finite (MonoidHom.{u_7, u_4} L ↥S)

Tactic:
have : Finite (L →* S) := .of_injective _ DFunLike.coe_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S_1 : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
L : Type u_7
inst_6 : LeftCancelMonoid L
inst_7 : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (MonoidHom.{u_7, u_4} L ↥S)
⊢ Finite (MonoidHom.{u_7, u_4} L Rˣ)

Tactic:
.of_surjective (fun f : L →* S ↦ (Subgroup.subtype _).comp f) fun f ↦ ?_

Premises used: Subgroup.subtype, MonoidHom.comp, Finite.of_surjective
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S_1 : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
L : Type u_7
inst_6 : LeftCancelMonoid L
inst_7 : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (MonoidHom.{u_7, u_4} L ↥S)
refine :
  ∀ (f : MonoidHom.{u_7, u_4} L Rˣ),
    ∃ (a : MonoidHom.{u_7, u_4} L ↥S), (fun (f : MonoidHom.{u_7, u_4} L ↥S) ↦ S.subtype.comp f) a = f
⊢ Finite (MonoidHom.{u_7, u_4} L Rˣ)

Tactic:
refine .of_surjective (fun f : L →* S ↦ (Subgroup.subtype _).comp f) fun f ↦ ?_
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S_1 : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : NeZero k
inst_4 : CommRing R
inst_5 : IsDomain R
L : Type u_7
inst_6 : LeftCancelMonoid L
inst_7 : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (MonoidHom.{u_7, u_4} L ↥S)
f : MonoidHom.{u_7, u_4} L Rˣ
a : L
rw : HPow.hPow (α := Rˣ) ((f : (a : L) → Rˣ) a : Rˣ) (Monoid.exponent L) = 1
rw₁ : Eq.{u_4 + 1} (α := Rˣ) ((f : (a : L) → Rˣ) (a ^ Monoid.exponent L) : Rˣ) (1 : Rˣ)
rw₂ : Eq.{u_4 + 1} (α := Rˣ) ((f : (a : L) → Rˣ) 1) 1
rw₃ rw₄ : Eq.{u_4 + 1} (α := Rˣ) 1 1
⊢ Membership.mem (α := Rˣ) S ((f : (a : L) → Rˣ) a : Rˣ)

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