awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_3} Rˣ R'ˣ
S : Submonoid R
h :
  ∀ (x : (↥S)ˣ),
    Eq.{u_3 + 1} (α := R') ((restrict S (ofUnitHom f) : (a : ↥S) → R') (↑x : ↥S) : R')
      ((ofUnitHom (MonoidHom.comp (f.restrict S.units) (↑S.unitsEquivUnitsType.symm : (↥S)ˣ →* ↥S.units)) :
            (a : ↥S) → R')
          (↑x : ↥S) :
        R')
⊢ restrict S (ofUnitHom f) =
    ofUnitHom (MonoidHom.comp (f.restrict S.units) (↑S.unitsEquivUnitsType.symm : (↥S)ˣ →* ↥S.units))

Tactic:
ext x
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_3} Rˣ R'ˣ
S : Submonoid R
x : (↥S)ˣ
h :
  Eq (α := R')
    ((((Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') f : MulChar R R') : (a : R) → R') (↑(↑x : ↥S) : R) :
      R')
    ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')
⊢ Eq.{u_3 + 1} (α := R') ((restrict S (ofUnitHom f) : (a : ↥S) → R') (↑x : ↥S) : R')
    ((ofUnitHom (MonoidHom.comp (f.restrict S.units) (↑S.unitsEquivUnitsType.symm : (↥S)ˣ →* ↥S.units)) : (a : ↥S) → R')
        (↑x : ↥S) :
      R')

Tactic:
simp only [ofUnitHom_eq, restrict_apply, Units.isUnit, reduceIte, equivToUnitHom_symm_coe,
    MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, MonoidHom.restrict_apply]

Premises used: MonoidHom.coe_comp, MulChar.equivToUnitHom_symm_coe, MonoidHom.coe_coe, MonoidHom.restrict_apply, MulChar.ofUnitHom_eq, MulChar.restrict_apply, reduceIte, Function.comp_apply, Units.isUnit
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_3} Rˣ R'ˣ
S : Submonoid R
x : (↥S)ˣ
h :
  Eq (α := R')
    ((((Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') f : MulChar R R') : (a : R) → R')
        (↑(↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ) : R) :
      R')
    ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')
h₁ h₂ :
  Eq (α := R') ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')
    ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')
⊢ Eq (α := R')
    ((((Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') f : MulChar R R') : (a : R) → R') (↑(↑x : ↥S) : R) :
      R')
    ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')

Tactic:
rw [← Submonoid.val_unitsEquivUnitsType_symm_apply_coe S x, equivToUnitHom_symm_coe]

Premises used: MulChar.equivToUnitHom_symm_coe, Submonoid.val_unitsEquivUnitsType_symm_apply_coe
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
S : Type u_2
inst_1 : SetLike S R
inst_2 : SubmonoidClass S R
T : S
R' : Type u_3
inst_3 : CommMonoidWithZero R'
h :
  ∀ (x : (↥T)ˣ),
    Eq.{u_3 + 1} (α := R') ((restrict T 1 : (a : ↥T) → R') (↑x : ↥T) : R') ((1 : (a : ↥T) → R') (↑x : ↥T) : R')
⊢ Eq (α := MulChar.{u_1, u_3} (↥T) R') (restrict T 1) 1

Tactic:
ext x
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
S : Type u_2
inst_1 : SetLike S R
inst_2 : SubmonoidClass S R
T : S
R' : Type u_3
inst_3 : CommMonoidWithZero R'
x : (↥T)ˣ
h :
  Eq.{u_3 + 1} (α := R') (if IsUnit (↑x : ↥T) then (1 : (a : R) → R') (↑(↑x : ↥T) : R) else 0 : R')
    ((1 : (a : ↥T) → R') (↑x : ↥T) : R')
h₁ : Eq.{u_3 + 1} (α := R') ((1 : (a : R) → R') (↑(↑x : ↥T) : R) : R') ((1 : (a : ↥T) → R') (↑x : ↥T) : R')
h₂ : Eq.{u_3 + 1} (α := R') (1 : R') ((1 : (a : ↥T) → R') (↑x : ↥T) : R')
h₃ h₄ : Eq.{u_3 + 1} (α := R') 1 1
⊢ Eq.{u_3 + 1} (α := R') ((restrict T 1 : (a : ↥T) → R') (↑x : ↥T) : R') ((1 : (a : ↥T) → R') (↑x : ↥T) : R')

Tactic:
rw [restrict_apply, if_pos x.isUnit, MulChar.one_apply x.isUnit.coe, one_apply_coe]

Premises used: MulChar.one_apply_coe, if_pos, MulChar.one_apply, MulChar.restrict_apply, Units.isUnit, IsUnit.coe
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
S : Type u_2
inst_1 : SetLike S R
inst_2 : SubmonoidClass S R
T : S
R' : Type u_3
inst_3 : CommMonoidWithZero R'
x x_1 : MulChar R R'
h :
  ∀ (a : (↥T)ˣ),
    Eq.{u_3 + 1} (α := R') ((restrict T (x * x_1) : (a : ↥T) → R') (↑a : ↥T) : R')
      ((HMul.hMul (α := MulChar.{u_1, u_3} (↥T) R') (restrict T x) (restrict T x_1) : (a : ↥T) → R') (↑a : ↥T) : R')
⊢ restrict T (x * x_1) = HMul.hMul (α := MulChar.{u_1, u_3} (↥T) R') (restrict T x) (restrict T x_1)

Tactic:
ext
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
S : Type u_2
inst_1 : SetLike S R
inst_2 : SubmonoidClass S R
T : S
R' : Type u_3
inst_3 : CommMonoidWithZero R'
x x_1 : MulChar R R'
a : (↥T)ˣ
⊢ Eq.{u_3 + 1} (α := R') ((restrict T (x * x_1) : (a : ↥T) → R') (↑a : ↥T) : R')
    ((HMul.hMul (α := MulChar.{u_1, u_3} (↥T) R') (restrict T x) (restrict T x_1) : (a : ↥T) → R') (↑a : ↥T) : R')

Tactic:
simp
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : StarRing R'
χ : MulChar R R'
h :
  ∀ (a : Rˣ),
    Eq.{u_2 + 1} (α := R') ((χ.starComp.starComp : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')
⊢ χ.starComp.starComp = χ

Tactic:
ext1
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : StarRing R'
χ : MulChar R R'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((χ.starComp.starComp : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')

Tactic:
simp only [starComp_apply, RingHomCompTriple.comp_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, MulChar.starComp_apply, RingHomCompTriple.comp_apply
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : StarRing R'
χ χ' : MulChar R R'
h :
  ∀ (a : Rˣ),
    Eq.{u_2 + 1} (α := R') (((χ * χ').starComp : (a : R) → R') (↑a : R) : R')
      ((χ'.starComp * χ.starComp : (a : R) → R') (↑a : R) : R')
⊢ (χ * χ').starComp = χ'.starComp * χ.starComp

Tactic:
ext1
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : StarRing R'
χ χ' : MulChar R R'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') (((χ * χ').starComp : (a : R) → R') (↑a : R) : R')
    ((χ'.starComp * χ.starComp : (a : R) → R') (↑a : R) : R')

Tactic:
simp only [starComp_apply, starRingEnd, coeToFun_mul, Pi.mul_apply, map_mul, RingHom.coe_coe,
      starRingAut_apply, mul_comm]

Premises used: Pi.mul_apply, RingHom.coe_coe, starRingAut_apply, MulChar.starComp_apply, map_mul, mul_comm, starRingEnd, MulChar.coeToFun_mul
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : StarRing R'
χ : MulChar R R'
a : R
⊢ Eq.{u_2 + 1} (α := R') ((star χ : (a : R) → R') a : R') (star ((χ : (a : R) → R') a) : R')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Fintype Rˣ
a : Rˣ
χ : MulChar R R'
rw :
  HPow.hPow (α := R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a : R'ˣ)
      (Fintype.card.{u_1} Rˣ) =
    1
rw₁ :
  Eq.{u_2 + 1} (α := R'ˣ)
    ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ)
        (a ^ Fintype.card.{u_1} Rˣ) :
      R'ˣ)
    (1 : R'ˣ)
rw₂ :
  Eq.{u_2 + 1} (α := R'ˣ)
    ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ)
        (a ^ Fintype.card.{u_1} Rˣ) :
      R'ˣ)
    ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) 1 : R'ˣ)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := R'ˣ)
    ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) 1)
    ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) 1)
⊢ Membership.mem (α := R'ˣ) (γ := Subgroup R'ˣ) (rootsOfUnity (Fintype.card.{u_1} Rˣ) R')
    ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a : R'ˣ)

Tactic:
rw [mem_rootsOfUnity, ← map_pow, ← (equivToUnitHom χ).map_one, pow_card_eq_one]

Premises used: pow_card_eq_one, mem_rootsOfUnity, map_pow, MulChar.equivToUnitHom, MonoidHom.map_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} Rˣ
χ : MulChar R ℂ
intro : ∀ (val : Fintype Rˣ), star χ = χ⁻¹
⊢ star χ = χ⁻¹

Tactic:
cases nonempty_fintype Rˣ

Premises used: Units, nonempty_fintype
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} Rˣ
χ : MulChar R ℂ
val : Fintype Rˣ
intro : ∀ (a : Rˣ), Eq (α := ℂ) ((star χ : (a : R) → ℂ) (↑a : R) : ℂ) ((χ⁻¹ : (a : R) → ℂ) (↑a : R) : ℂ)
⊢ star χ = χ⁻¹

Tactic:
ext1 a
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} Rˣ
χ : MulChar R ℂ
val : Fintype Rˣ
a : Rˣ
intro : Eq (α := ℂ) ((star χ : (a : R) → ℂ) (↑a : R) : ℂ) (((χ : (a : R) → ℂ) (↑a : R))⁻¹ : ℂ)
⊢ Eq (α := ℂ) ((star χ : (a : R) → ℂ) (↑a : R) : ℂ) ((χ⁻¹ : (a : R) → ℂ) (↑a : R) : ℂ)

Tactic:
simp only [inv_apply_eq_inv']

Premises used: MulChar.inv_apply_eq_inv'
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} Rˣ
χ : MulChar R ℂ
val : Fintype Rˣ
a : Rˣ
⊢ Eq (α := ℂ) ((star χ : (a : R) → ℂ) (↑a : R) : ℂ) (((χ : (a : R) → ℂ) (↑a : R))⁻¹ : ℂ)

Tactic:
(inv_eq_conj <| norm_eq_one_of_mem_rootsOfUnity <| χ.apply_mem_rootsOfUnity a).symm

Premises used: Complex.norm_eq_one_of_mem_rootsOfUnity, Complex.inv_eq_conj, Eq.symm, MulChar.apply_mem_rootsOfUnity
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} Rˣ
χ : MulChar R ℂ
val : Fintype Rˣ
a : Rˣ
⊢ Eq (α := ℂ) ((star χ : (a : R) → ℂ) (↑a : R) : ℂ) (((χ : (a : R) → ℂ) (↑a : R))⁻¹ : ℂ)

Tactic:
exact (inv_eq_conj <| norm_eq_one_of_mem_rootsOfUnity <| χ.apply_mem_rootsOfUnity a).symm

Premises used: Complex.norm_eq_one_of_mem_rootsOfUnity, Complex.inv_eq_conj, Eq.symm, MulChar.apply_mem_rootsOfUnity
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} Rˣ
χ : MulChar R ℂ
a : R
⊢ Eq (α := ℂ) (star ((χ : (a : R) → ℂ) a) : ℂ) ((χ⁻¹ : (a : R) → ℂ) a : ℂ)

Tactic:
simp only [RCLike.star_def, ← star_eq_inv, star_apply]

Premises used: RCLike.star_def, MulChar.star_apply, MulChar.star_eq_inv
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
ζ : Rˣ
hζ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) ζ
g : Mˣ
hg : ∀ (x : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers g) x
⊢ orderOf ζ ∣ Fintype.card.{u_1} Mˣ

Tactic:
have : orderOf ζ ∣ Fintype.card Mˣ :=
    orderOf_dvd_iff_pow_eq_one.mpr <| (mem_rootsOfUnity _ ζ).mp hζ
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
ζ : Rˣ
hζ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) ζ
g : Mˣ
hg : ∀ (x : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers g) x
this : orderOf ζ ∣ Fintype.card.{u_1} Mˣ
refine : Fintype.card.{u_1} Mˣ = orderOf g
⊢ MulChar M R

Tactic:
refine ofUnitHom <| monoidHomOfForallMemZpowers hg <| this.trans <| dvd_of_eq ?_

Premises used: monoidHomOfForallMemZpowers, MulChar.ofUnitHom, dvd_of_eq, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
ζ : Rˣ
hζ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) ζ
g : Mˣ
hg : ∀ (x : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers g) x
this : orderOf ζ ∣ Fintype.card.{u_1} Mˣ
rw : Fintype.card.{u_1} Mˣ = Nat.card.{u_1} Mˣ
rw₁ rw₂ : Fintype.card.{u_1} Mˣ = Fintype.card.{u_1} Mˣ
⊢ Fintype.card.{u_1} Mˣ = orderOf g

Tactic:
rw [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
ζ : Rˣ
hζ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) ζ
g : Mˣ
hg : ∀ (x : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers g) x
⊢ (ofRootOfUnity hζ hg : (a : M) → R) (↑g : M) = (↑ζ : R)

Tactic:
simp only [ofRootOfUnity, ofUnitHom_eq, equivToUnitHom_symm_coe,
    monoidHomOfForallMemZpowers_apply_gen]

Premises used: monoidHomOfForallMemZpowers_apply_gen, MulChar.ofRootOfUnity, MulChar.equivToUnitHom_symm_coe, MulChar.ofUnitHom_eq
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
inst_cyc : IsCyclic.{u_1} Mˣ
χ : MulChar M R
⊢ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R)
    ((χ.toUnitHom : (a : Mˣ) → Rˣ)
      (Classical.choose (p := fun (x : Mˣ) ↦ ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1)
        ⋯))

Tactic:
simp only [toUnitHom_eq, mem_rootsOfUnity, ← map_pow, pow_card_eq_one, map_one]

Premises used: pow_card_eq_one, mem_rootsOfUnity, MulChar.toUnitHom_eq, map_pow, map_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
inst_cyc : IsCyclic.{u_1} Mˣ
χ : MulChar M R
⊢ (fun (ζ : ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)) ↦
        ofRootOfUnity ⋯ (g :=
          Classical.choose (p := fun (x : Mˣ) ↦
            ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯)
          ⋯)
      ((fun (χ : MulChar M R) ↦
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) x)
              ((χ.toUnitHom : (a : Mˣ) → Rˣ)
                (Classical.choose (p := fun (x : Mˣ) ↦
                  ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯))
              ⋯ :
            ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)))
        χ) =
    χ

Tactic:
simp only [toUnitHom_eq, eq_iff <| Classical.choose_spec inst_cyc.exists_generator,
      ofRootOfUnity_spec, coe_equivToUnitHom]

Premises used: MulChar.eq_iff, MulChar.toUnitHom_eq, IsCyclic.exists_generator, Classical.choose_spec, MulChar.ofRootOfUnity_spec, MulChar.coe_equivToUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
inst_cyc : IsCyclic.{u_1} Mˣ
ζ : ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)
a :
  (↑(↑((fun (χ : MulChar M R) ↦
                (Subtype.mk (p := fun (x : Rˣ) ↦
                    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) x)
                    ((χ.toUnitHom : (a : Mˣ) → Rˣ)
                      (Classical.choose (p := fun (x : Mˣ) ↦
                        ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯))
                    ⋯ :
                  ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)))
              ((fun (ζ : ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)) ↦
                  ofRootOfUnity ⋯ (g :=
                    Classical.choose (p := fun (x : Mˣ) ↦
                      ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯)
                    ⋯)
                ζ)) :
          Rˣ) :
      R) =
    (↑(↑ζ : Rˣ) : R)
⊢ (fun (χ : MulChar M R) ↦
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) x)
            ((χ.toUnitHom : (a : Mˣ) → Rˣ)
              (Classical.choose (p := fun (x : Mˣ) ↦
                ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯))
            ⋯ :
          ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)))
      ((fun (ζ : ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)) ↦
          ofRootOfUnity ⋯ (g :=
            Classical.choose (p := fun (x : Mˣ) ↦
              ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯)
            ⋯)
        ζ) =
    ζ

Tactic:
ext
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
inst_cyc : IsCyclic.{u_1} Mˣ
ζ : ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)
⊢ (↑(↑((fun (χ : MulChar M R) ↦
                (Subtype.mk (p := fun (x : Rˣ) ↦
                    Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) x)
                    ((χ.toUnitHom : (a : Mˣ) → Rˣ)
                      (Classical.choose (p := fun (x : Mˣ) ↦
                        ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯))
                    ⋯ :
                  ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)))
              ((fun (ζ : ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R)) ↦
                  ofRootOfUnity ⋯ (g :=
                    Classical.choose (p := fun (x : Mˣ) ↦
                      ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯)
                    ⋯)
                ζ)) :
          Rˣ) :
      R) =
    (↑(↑ζ : Rˣ) : R)

Tactic:
simp only [toUnitHom_eq, coe_equivToUnitHom, ofRootOfUnity_spec]

Premises used: MulChar.toUnitHom_eq, MulChar.ofRootOfUnity_spec, MulChar.coe_equivToUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Fintype M
inst_2 : DecidableEq M
R : Type u_2
inst_3 : CommMonoidWithZero R
inst_cyc : IsCyclic.{u_1} Mˣ
x y : MulChar M R
⊢ Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) x)
      (((x * y).toUnitHom : (a : Mˣ) → Rˣ)
        (Classical.choose (p := fun (x : Mˣ) ↦ ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1)
          ⋯))
      ⋯ =
    HMul.hMul (α := ↥(rootsOfUnity (Fintype.card.{u_1} Mˣ) R))
      (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) x)
        ((x.toUnitHom : (a : Mˣ) → Rˣ)
          (Classical.choose (p := fun (x : Mˣ) ↦
            ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯))
        ⋯)
      (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Mˣ) R) x)
        ((y.toUnitHom : (a : Mˣ) → Rˣ)
          (Classical.choose (p := fun (x : Mˣ) ↦
            ∀ (x_1 : Mˣ), Membership.mem (γ := Subgroup Mˣ) (Subgroup.zpowers x) x_1) ⋯))
        ⋯)

Tactic:
simp only [toUnitHom_eq, equivToUnitHom_mul_apply, MulMemClass.mk_mul_mk]

Premises used: MulChar.equivToUnitHom_mul_apply, MulChar.toUnitHom_eq, MulMemClass.mk_mul_mk
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ 0 < n

Tactic:
Nat.pos_of_ne_zero fun hn ↦ ?_

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
refine : ∀ (hn : n = 0), False
⊢ 0 < n

Tactic:
refine Nat.pos_of_ne_zero fun hn ↦ ?_

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn : n = 0
⊢ Fintype.card F ≤ 1

Tactic:
simp only [hn, zero_dvd_iff, Nat.sub_eq_zero_iff_le] at h

Premises used: zero_dvd_iff, Nat.sub_eq_zero_iff_le
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
hn : n = 0
h : Fintype.card F ≤ 1
⊢ False

Tactic:
(Fintype.one_lt_card.trans_le h).false

Premises used: Fintype.one_lt_card, LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
hn : n = 0
h : Fintype.card F ≤ 1
⊢ False

Tactic:
exact (Fintype.one_lt_card.trans_le h).false

Premises used: Fintype.one_lt_card, LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ 0 < n

Tactic:
have hn₀ : 0 < n := by
    refine Nat.pos_of_ne_zero fun hn ↦ ?_
    simp only [hn, zero_dvd_iff, Nat.sub_eq_zero_iff_le] at h
    exact (Fintype.one_lt_card.trans_le h).false
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
⊢ ζ' ^ Fintype.card.{u_1} Fˣ = 1

Tactic:
have h' : ζ' ^ (Fintype.card Fˣ : ℕ) = 1 :=
    Units.ext_iff.mpr <| (hζ.pow_eq_one_iff_dvd _).mpr <| Fintype.card_units (α := F) ▸ h
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
h₁ :
  orderOf (G := MulChar F R)
      ((e.symm : (a : ↥(rootsOfUnity (Fintype.card Fˣ) R)) → MulChar F R)
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x)
            ζ' ⋯) :
        MulChar F R) =
    n
⊢ ∃ (χ : MulChar F R), orderOf χ = n

Tactic:
use e.symm ⟨ζ', (mem_rootsOfUnity (Fintype.card Fˣ) ζ').mpr h'⟩

Premises used: Iff.mpr, mem_rootsOfUnity, Units, Fintype.card, Subtype.mk, MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card.{u_1} Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card.{u_1} Fˣ = 1
h₁ :
  Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ' ⋯ ^
        n =
      1 ∧
    ∀ m < n,
      0 < m →
        Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x) ζ'
              ⋯ ^
            m ≠
          1
⊢ orderOf (G := MulChar F R)
      ((e.symm : (a : ↥(rootsOfUnity (Fintype.card Fˣ) R)) → MulChar F R)
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity (Fintype.card.{u_1} Fˣ) R) x)
            ζ' ⋯) :
        MulChar F R) =
    n

Tactic:
rw [e.symm.orderOf_eq, orderOf_eq_iff hn₀]

Premises used: orderOf_eq_iff, MulEquiv.orderOf_eq, MulEquiv.symm