awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingInvo
Goal:
R : Type u_2
inst : Semiring R
f : RingInvo R
a : R
⊢ Eq (α := Rᵐᵒᵖ) ((f.toRingEquiv : (a : R) → Rᵐᵒᵖ) a : Rᵐᵒᵖ) ((f : (a : R) → Rᵐᵒᵖ) a : Rᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.RingInvo
Goal:
R : Type u_2
inst : Semiring R
f : RingInvo R
x : R
⊢ Eq (α := Rᵐᵒᵖ) ((f : (a : R) → Rᵐᵒᵖ) x : Rᵐᵒᵖ) (0 : Rᵐᵒᵖ) ↔ x = 0

Tactic:
f.toRingEquiv.map_eq_zero_iff

Premises used: RingEquiv.map_eq_zero_iff, RingInvo.toRingEquiv
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
inst_2 : IsSepClosed F
⊢ NeZero n

Tactic:
have : NeZero n := .of_neZero_natCast F
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
inst_2 : IsSepClosed F
this : NeZero n
⊢ IsCyclotomicExtension {n} F F

Tactic:
have := isCyclotomicExtension {n} F fun _ h _ ↦ Set.mem_singleton_iff.mp h ▸ ‹NeZero (n : F)›
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
inst_2 : IsSepClosed F
this_1 : NeZero n
this : IsCyclotomicExtension {n} F F
⊢ ∃ (m : F), IsPrimitiveRoot m n

Tactic:
IsCyclotomicExtension.exists_isPrimitiveRoot (S := {n}) F _ rfl (NeZero.ne _)

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot, rfl, NeZero.ne
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
inst_2 : IsSepClosed F
this_1 : NeZero n
this : IsCyclotomicExtension {n} F F
⊢ ∃ (m : F), IsPrimitiveRoot m n

Tactic:
exact IsCyclotomicExtension.exists_isPrimitiveRoot (S := {n}) F _ rfl (NeZero.ne _)

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot, rfl, NeZero.ne
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
inst_2 : IsSepClosed F
⊢ NeZero.{u_1} (R := F) (↑(n ^ k) : F)

Tactic:
exact_mod_cast ‹NeZero (n : F)›.pow

Premises used: NeZero.pow
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
⊢ HasEnoughRootsOfUnity.{u_1} (AlgebraicClosure F) n

Tactic:
have : NeZero (n : AlgebraicClosure F) :=
    ‹NeZero (n : F)›.of_injective (algebraMap F (AlgebraicClosure F)).injective
  inferInstance

Premises used: Algebra.algebraMap, inferInstance, RingHom.injective, NeZero.of_injective, AlgebraicClosure
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
⊢ HasEnoughRootsOfUnity.{u_1} (AlgebraicClosure F) (n ^ k)

Tactic:
have : NeZero (n : AlgebraicClosure F) :=
    ‹NeZero (n : F)›.of_injective (algebraMap F (AlgebraicClosure F)).injective
  inferInstance

Premises used: Algebra.algebraMap, inferInstance, RingHom.injective, NeZero.of_injective, AlgebraicClosure
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
⊢ HasEnoughRootsOfUnity.{u_1} (SeparableClosure F) n

Tactic:
have : NeZero (n : SeparableClosure F) :=
    ‹NeZero (n : F)›.of_injective (algebraMap F (SeparableClosure F)).injective
  inferInstance

Premises used: Algebra.algebraMap, inferInstance, RingHom.injective, NeZero.of_injective, SeparableClosure
-- Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Goal:
F : Type u_1
inst : Field F
n k : ℕ
inst_1 : NeZero.{u_1} (R := F) (↑n : F)
⊢ HasEnoughRootsOfUnity.{u_1} (SeparableClosure F) (n ^ k)

Tactic:
have : NeZero (n : SeparableClosure F) :=
    ‹NeZero (n : F)›.of_injective (algebraMap F (SeparableClosure F)).injective
  inferInstance

Premises used: Algebra.algebraMap, inferInstance, RingHom.injective, NeZero.of_injective, SeparableClosure
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k_1 l k : ℕ
M : Type u_7
inst_3 : CommMonoid M
a b : Mˣ
h : Membership.mem (γ := Set Mˣ) {ζ : Mˣ | ζ ^ k = 1} a
h_1 : Membership.mem (γ := Set Mˣ) {ζ : Mˣ | ζ ^ k = 1} b
⊢ Membership.mem (γ := Set Mˣ) {ζ : Mˣ | ζ ^ k = 1} (a * b)

Tactic:
simp_all only [Set.mem_setOf_eq, mul_pow, one_mul]

Premises used: Set.mem_setOf_eq, mul_pow, one_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k_1 l k : ℕ
M : Type u_7
inst_3 : CommMonoid M
x : Mˣ
h : Membership.mem (γ := Set Mˣ) {ζ : Mˣ | ζ ^ k = 1} x
⊢ Membership.mem (γ := Set Mˣ) {ζ : Mˣ | ζ ^ k = 1} x⁻¹

Tactic:
simp_all only [Set.mem_setOf_eq, inv_pow, inv_one]

Premises used: inv_one, Set.mem_setOf_eq, inv_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity k M) ζ ↔ ζ ^ k = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
⊢ Eq (α := Subgroup Mˣ) (rootsOfUnity k M) (MonoidHom.ker (powMonoidHom k))

Tactic:
rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
k : ℤ
h :
  ∀ (x : Mˣ),
    Membership.mem (γ := Subgroup Mˣ) (MonoidHom.ker (zpowGroupHom k)) x ↔
      Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity k.natAbs M) x
⊢ Eq (α := Subgroup Mˣ) (MonoidHom.ker (zpowGroupHom k)) (rootsOfUnity k.natAbs M)

Tactic:
ext
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
k : ℤ
x : Mˣ
⊢ Membership.mem (γ := Subgroup Mˣ) (MonoidHom.ker (zpowGroupHom k)) x ↔
    Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity k.natAbs M) x

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : Mˣ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ζ ^ k = 1 ↔ ζ ^ k = 1
⊢ ζ ^ k = 1 ↔ (↑ζ : M) ^ k = 1

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_7
inst : CommMonoid M
h : ∀ (x : Mˣ), Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity 1 M) x ↔ Membership.mem (γ := Subgroup Mˣ) ⊥ x
⊢ Eq (α := Subgroup Mˣ) (rootsOfUnity 1 M) ⊥

Tactic:
ext1
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_7
inst : CommMonoid M
x : Mˣ
⊢ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity 1 M) x ↔ Membership.mem (γ := Subgroup Mˣ) ⊥ x

Tactic:
simp only [mem_rootsOfUnity, pow_one, Subgroup.mem_bot]

Premises used: mem_rootsOfUnity, pow_one, Subgroup.mem_bot
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_7
inst : CommMonoid M
h : ∀ (x : Mˣ), Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity 0 M) x ↔ Membership.mem (γ := Subgroup Mˣ) ⊤ x
⊢ Eq (α := Subgroup Mˣ) (rootsOfUnity 0 M) ⊤

Tactic:
ext1
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_7
inst : CommMonoid M
x : Mˣ
⊢ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity 0 M) x ↔ Membership.mem (γ := Subgroup Mˣ) ⊤ x

Tactic:
simp only [mem_rootsOfUnity, pow_zero, Subgroup.mem_top]

Premises used: mem_rootsOfUnity, pow_zero, Subgroup.mem_top
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
⊢ Function.Injective (β := M) fun (x : ↥(rootsOfUnity n M)) ↦ (↑(↑x : Mˣ) : M)

Tactic:
Units.val_injective.comp Subtype.val_injective

Premises used: Subtype.val_injective, Function.Injective.comp, Units.val_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
n : ℕ
inst_1 : NeZero n
h : ζ ^ n = 1
⊢ (↑(↑(mkOfPowEq ζ h) : Mˣ) : M) = ζ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
k l : ℕ
h : k ∣ l
obtain : ∀ (d : ℕ), LE.le (α := Subgroup Mˣ) (rootsOfUnity k M) (rootsOfUnity (k * d) M)
⊢ LE.le (α := Subgroup Mˣ) (rootsOfUnity k M) (rootsOfUnity l M)

Tactic:
obtain ⟨d, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
k d : ℕ
ζ : Mˣ
h : Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity k M) ζ
⊢ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity (k * d) M) ζ

Tactic:
simp_all only [mem_rootsOfUnity, pow_mul, one_pow]

Premises used: mem_rootsOfUnity, one_pow, pow_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
inst_1 : CommMonoid N
f : MonoidHom.{u_1, u_2} Mˣ Nˣ
k : ℕ
ζ : Mˣ
h : ζ ∈ (↑(rootsOfUnity k M) : Set Mˣ)
⊢ Membership.mem (α := Nˣ) (γ := Subgroup Nˣ) (rootsOfUnity k N) ((f : (a : Mˣ) → Nˣ) ζ : Nˣ)

Tactic:
simp_all only [← map_pow, mem_rootsOfUnity, SetLike.mem_coe, map_one]

Premises used: mem_rootsOfUnity, map_pow, map_one, SetLike.mem_coe
-- 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 : ℕ
⊢ Subsingleton.{u_1 + 1} ↥(rootsOfUnity 1 M)

Tactic:
simp [subsingleton_iff]

Premises used: subsingleton_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
m n : ℕ
h :
  ∀ (x : Mˣ),
    Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity m M ⊓ rootsOfUnity n M) x ↔
      Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity (m.gcd n) M) x
⊢ Eq (α := Subgroup Mˣ) (rootsOfUnity m M ⊓ rootsOfUnity n M) (rootsOfUnity (m.gcd n) M)

Tactic:
ext
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
m n : ℕ
x : Mˣ
⊢ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity m M ⊓ rootsOfUnity n M) x ↔
    Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity (m.gcd n) M) x

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M : Type u_1
inst : CommMonoid M
m n : ℕ
h : m.Coprime n
⊢ Disjoint (α := Subgroup Mˣ) (rootsOfUnity m M) (rootsOfUnity n M)

Tactic:
simp [disjoint_iff_inf_le, rootsOfUnity_inf_rootsOfUnity, Nat.coprime_iff_gcd_eq_one.mp h]

Premises used: rootsOfUnity_inf_rootsOfUnity, Nat.coprime_iff_gcd_eq_one, Iff.mp, disjoint_iff_inf_le
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
k : ℕ
inst : CommMonoid R
ζ : ↥(rootsOfUnity k R)
m : ℕ
rw : (↑((↑ζ : Rˣ) ^ m) : R) = (↑(↑ζ : Rˣ) : R) ^ m
rw₁ rw₂ : (↑(↑ζ : Rˣ) : R) ^ m = (↑(↑ζ : Rˣ) : R) ^ m
⊢ (↑(↑(ζ ^ m) : Rˣ) : R) = (↑(↑ζ : Rˣ) : R) ^ m

Tactic:
rw [Subgroup.coe_pow, Units.val_pow_eq_pow_val]

Premises used: Subgroup.coe_pow, Units.val_pow_eq_pow_val
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
M : Type u_7
inst_3 : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
simp : (↑ζ : Mˣ) ^ n = 1
⊢ Membership.mem (α := Mˣˣ) (γ := Subgroup Mˣˣ) (rootsOfUnity n Mˣ) ((toUnits : (a : Mˣ) → Mˣˣ) (↑ζ : Mˣ) : Mˣˣ)

Tactic:
simp only [mem_rootsOfUnity, ← map_pow, EmbeddingLike.map_eq_one_iff]

Premises used: mem_rootsOfUnity, EmbeddingLike.map_eq_one_iff, map_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
M : Type u_7
inst_3 : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
⊢ (↑ζ : Mˣ) ^ n = 1

Tactic:
(mem_rootsOfUnity ..).mp ζ.prop

Premises used: mem_rootsOfUnity, Subtype.prop, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
M : Type u_7
inst_3 : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
⊢ (↑ζ : Mˣ) ^ n = 1

Tactic:
exact (mem_rootsOfUnity ..).mp ζ.prop

Premises used: mem_rootsOfUnity, Subtype.prop, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
M : Type u_7
inst_3 : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n Mˣ)
⊢ (fun (ζ : ↥(rootsOfUnity n M)) ↦
        (Subtype.mk (p := fun (x : Mˣˣ) ↦ Membership.mem (γ := Subgroup Mˣˣ) (rootsOfUnity n Mˣ) x)
            ((toUnits : (a : Mˣ) → Mˣˣ) (↑ζ : Mˣ)) ⋯ :
          ↥(rootsOfUnity n Mˣ)))
      ((fun (ζ : ↥(rootsOfUnity n Mˣ)) ↦
          Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) (↑(↑ζ : Mˣˣ) : Mˣ) ⋯)
        ζ) =
    ζ

Tactic:
simp only [toUnits_val_apply, Subtype.coe_eta]

Premises used: Subtype.coe_eta, toUnits_val_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
M : Type u_7
inst_3 : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
⊢ (fun (ζ : ↥(rootsOfUnity n Mˣ)) ↦
        Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) (↑(↑ζ : Mˣˣ) : Mˣ) ⋯)
      ((fun (ζ : ↥(rootsOfUnity n M)) ↦
          (Subtype.mk (p := fun (x : Mˣˣ) ↦ Membership.mem (γ := Subgroup Mˣˣ) (rootsOfUnity n Mˣ) x)
              ((toUnits : (a : Mˣ) → Mˣˣ) (↑ζ : Mˣ)) ⋯ :
            ↥(rootsOfUnity n Mˣ)))
        ζ) =
    ζ

Tactic:
simp only [val_toUnits_apply, Subtype.coe_eta]

Premises used: val_toUnits_apply, Subtype.coe_eta
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
M_1 : 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_1
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
M : Type u_7
inst_3 : CommMonoid M
n : ℕ
ζ ζ' : ↥(rootsOfUnity n Mˣ)
⊢ Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) (↑(↑(ζ * ζ') : Mˣˣ) : Mˣ) ⋯ =
    Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) (↑(↑ζ : Mˣˣ) : Mˣ) ⋯ *
      Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) (↑(↑ζ' : Mˣˣ) : Mˣ) ⋯

Tactic:
simp only [Subgroup.coe_mul, Units.val_mul, MulMemClass.mk_mul_mk]

Premises used: Subgroup.coe_mul, MulMemClass.mk_mul_mk, Units.val_mul
-- 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
inst_6 : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
rw : Eq.{u_5 + 1} (α := S) (((↑σ : R →* S) : (a : R) → S) (↑1 : R) : S) ((↑1 : S) : S)
⊢ Membership.mem (α := Sˣ) (γ := Subgroup Sˣ) (rootsOfUnity n S)
    (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑ξ : Rˣ) : Sˣ)

Tactic:
rw [mem_rootsOfUnity, ← map_pow, Units.ext_iff, Units.coe_map, ξ.prop]

Premises used: mem_rootsOfUnity, Units.ext_iff, Units.coe_map, map_pow, Subtype.prop
-- 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
inst_6 : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ Eq.{u_5 + 1} (α := S) (((↑σ : R →* S) : (a : R) → S) (↑1 : R) : S) ((↑1 : S) : S)

Tactic:
map_one σ

Premises used: map_one
-- 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
inst_6 : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ Eq.{u_5 + 1} (α := S) (((↑σ : R →* S) : (a : R) → S) (↑1 : R) : S) ((↑1 : S) : S)

Tactic:
exact map_one σ

Premises used: map_one
-- 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
inst_6 : MonoidHomClass F R S
σ : F
n : ℕ
a :
  Eq (α := Sˣ)
    (↑(Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
          (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑1 : Rˣ)) ⋯) :
      Sˣ)
    (↑1 : Sˣ)
⊢ Eq (α := ↥(rootsOfUnity n S))
    (Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
      (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑1 : Rˣ)) ⋯)
    1

Tactic:
ext1
-- 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
inst_6 : MonoidHomClass F R S
σ : F
n : ℕ
⊢ Eq (α := Sˣ)
    (↑(Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
          (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑1 : Rˣ)) ⋯) :
      Sˣ)
    (↑1 : Sˣ)

Tactic:
simp only [OneMemClass.coe_one, map_one]

Premises used: OneMemClass.coe_one, map_one
-- 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
inst_6 : MonoidHomClass F R S
σ : F
n : ℕ
ξ₁ ξ₂ : ↥(rootsOfUnity n R)
a :
  (↑(Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
          (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑(ξ₁ * ξ₂) : Rˣ)) ⋯) :
      Sˣ) =
    (↑(HMul.hMul (α := ↥(rootsOfUnity n S)) (β := ↥(rootsOfUnity n S))
          (Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
              (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑ξ₁ : Rˣ)) ⋯ :
            ↥(rootsOfUnity n S))
          (Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
              (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑ξ₂ : Rˣ)) ⋯ :
            ↥(rootsOfUnity n S))) :
      Sˣ)
⊢ Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
      (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑(ξ₁ * ξ₂) : Rˣ)) ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity n S)) (β := ↥(rootsOfUnity n S))
      (Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
          (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑ξ₁ : Rˣ)) ⋯ :
        ↥(rootsOfUnity n S))
      (Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
          (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑ξ₂ : Rˣ)) ⋯ :
        ↥(rootsOfUnity n S))

Tactic:
ext1
-- 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
inst_6 : MonoidHomClass F R S
σ : F
n : ℕ
ξ₁ ξ₂ : ↥(rootsOfUnity n R)
⊢ (↑(Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
          (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑(ξ₁ * ξ₂) : Rˣ)) ⋯) :
      Sˣ) =
    (↑(HMul.hMul (α := ↥(rootsOfUnity n S)) (β := ↥(rootsOfUnity n S))
          (Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
              (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑ξ₁ : Rˣ)) ⋯ :
            ↥(rootsOfUnity n S))
          (Subtype.mk (p := fun (x : Sˣ) ↦ Membership.mem (γ := Subgroup Sˣ) (rootsOfUnity n S) x)
              (((Units.map (↑σ : R →* S) : MonoidHom.{u_4, u_5} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (↑ξ₂ : Rˣ)) ⋯ :
            ↥(rootsOfUnity n S))) :
      Sˣ)

Tactic:
simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]

Premises used: Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk
-- Module: Mathlib.RingTheory.RootsOfUnity.Basic
Goal:
R : Type u_4
S : Type u_5
F : Type u_6
k : ℕ
inst : CommMonoid R
inst_1 : CommMonoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
σ : F
ζ : ↥(rootsOfUnity k R)
⊢ Eq.{u_5 + 1} (α := S)
    ((↑(↑(((restrictRootsOfUnity σ k : MonoidHom.{u_4, u_5} ↥(rootsOfUnity k R) ↥(rootsOfUnity k S)) :
                  (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:
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 R)
a :
  (↑(↑(((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
              (((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                  (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                ξ)) :
          Rˣ) :
      R) =
    (↑(↑ξ : Rˣ) : R)
⊢ ((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
        (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
      (((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
          (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
        ξ) =
    ξ

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 R)
⊢ (↑(↑(((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
              (((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                  (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                ξ)) :
          Rˣ) :
      R) =
    (↑(↑ξ : Rˣ) : R)

Tactic:
σ.symm_apply_apply _

Premises used: MulEquiv.symm_apply_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 R)
⊢ (↑(↑(((_root_.restrictRootsOfUnity σ.symm n : MonoidHom.{u_5, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
              (((_root_.restrictRootsOfUnity σ n : MonoidHom.{u_4, u_5} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                  (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                ξ)) :
          Rˣ) :
      R) =
    (↑(↑ξ : Rˣ) : R)

Tactic:
exact σ.symm_apply_apply _

Premises used: MulEquiv.symm_apply_apply