awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ :
  (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) ^
          aux g (p ^ (k + i))) :
      L)
H₂ :
  (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) ⋯.unit ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) ⋯.unit ⋯) :
            Lˣ) ^
          aux g (p ^ k)) :
      L)
⊢ HPow.hPow (α := L) ((g : (a : L) → L) ζ : L) (p ^ i) = (↑(⋯.unit ^ aux g (p ^ k)) : L)

Tactic:
simp only [IsUnit.unit_spec, map_pow] at H₁ H₂

Premises used: map_pow, IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : HPow.hPow (α := L) ((g : (a : L) → L) ζ : L) (p ^ i) = (↑(⋯.unit ^ aux g (p ^ k)) : L)
⊢ (⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i / (⋯.unit ^ p ^ i) ^ aux g (p ^ k) = 1

Tactic:
rw [H₁, ← Units.val_pow_eq_pow_val, ← Units.ext_iff, h_unit, ← div_eq_one] at H₂

Premises used: Units.ext_iff, div_eq_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : (⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i / (⋯.unit ^ p ^ i) ^ aux g (p ^ k) = 1
⊢ ⋯.unit ^ (aux g (p ^ (k + i)) * (↑(p ^ i) : ℤ) - (↑(p ^ i) : ℤ) * aux g (p ^ k)) = 1

Tactic:
simp only [← zpow_natCast, ← zpow_mul, div_eq_mul_inv, ← zpow_sub] at H₂

Premises used: zpow_natCast, zpow_mul, div_eq_mul_inv, zpow_sub
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : ⋯.unit ^ (aux g (p ^ (k + i)) * (↑(p ^ i) : ℤ) - (↑(p ^ i) : ℤ) * aux g (p ^ k)) = 1
⊢ (↑(p ^ (k + i)) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))

Tactic:
rw [(hζ.isUnit_unit NeZero.out).zpow_eq_one_iff_dvd, mul_comm, ← mul_sub] at H₂

Premises used: mul_sub, IsPrimitiveRoot.isUnit_unit, NeZero.out, mul_comm, IsPrimitiveRoot.zpow_eq_one_iff_dvd
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : (↑(p ^ (k + i)) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
rw : HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ)
| (↑(p ^ (k + i)) : ℤ)

Tactic:
rw [Nat.pow_add', Nat.cast_mul]

Premises used: Nat.cast_mul, Nat.pow_add'
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : (↑(p ^ (k + i)) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))

Tactic:
conv_lhs at H₂ => rw [Nat.pow_add', Nat.cast_mul]

Premises used: Nat.cast_mul, Nat.pow_add'
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ Ne (α := ℤ) (↑(p ^ i) : ℤ) 0

Tactic:
simp [NeZero.ne p]

Premises used: NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : (g : (a : L) → L) ζ = (↑(⋯.unit ^ aux g (p ^ (k + i))) : L)
H₂ : HMul.hMul (α := ℤ) (↑(p ^ i) : ℤ) (↑(p ^ k) : ℤ) ∣ (↑(p ^ i) : ℤ) * (aux g (p ^ (k + i)) - aux g (p ^ k))
rwa :
  ∀ (H₂ : (↑(p ^ k) : ℤ) ∣ aux g (p ^ (k + i)) - aux g (p ^ k)),
    HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (H₂ : HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)),
    HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
rwa [mul_dvd_mul_iff_left (by simp [NeZero.ne p]), Nat.cast_pow] at H₂

Premises used: mul_dvd_mul_iff_left, Nat.cast_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
rw : (↑(↑(t ^ aux g n) : Lˣ) : L) = (↑((↑t : Lˣ) ^ (aux g n % (↑(Fintype.card.{u} ↥(rootsOfUnity n L)) : ℤ))) : L)
⊢ (g : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)

Tactic:
rw [modularCyclotomicCharacter.aux_spec g n t, ← zpow_natCast, modularCyclotomicCharacter.toFun,
    ZMod.val_intCast, ← Subgroup.coe_zpow]

Premises used: zpow_natCast, modularCyclotomicCharacter.toFun, Subgroup.coe_zpow, ZMod.val_intCast, modularCyclotomicCharacter.aux_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
⊢ (↑(↑(t ^ aux g n) : Lˣ) : L) = (↑((↑t : Lˣ) ^ (aux g n % (↑(Fintype.card.{u} ↥(rootsOfUnity n L)) : ℤ))) : L)

Tactic:
Units.ext_iff.1 <| SetCoe.ext_iff.2 <|
    zpow_eq_zpow_emod _ pow_card_eq_one (G := rootsOfUnity n L)

Premises used: Iff.mpr, Units.ext_iff, Iff.mp, SetCoe.ext_iff, zpow_eq_zpow_emod
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
⊢ (↑(↑(t ^ aux g n) : Lˣ) : L) = (↑((↑t : Lˣ) ^ (aux g n % (↑(Fintype.card.{u} ↥(rootsOfUnity n L)) : ℤ))) : L)

Tactic:
exact Units.ext_iff.1 <| SetCoe.ext_iff.2 <|
    zpow_eq_zpow_emod _ pow_card_eq_one (G := rootsOfUnity n L)

Premises used: Iff.mpr, Units.ext_iff, Iff.mp, SetCoe.ext_iff, zpow_eq_zpow_emod
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
n : ℕ
inst_2 : NeZero n
t : Lˣ
ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t
⊢ (g : (a : L) → L) (↑t : L) = (↑t : L) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)

Tactic:
toFun_spec g ⟨t, ht⟩

Premises used: modularCyclotomicCharacter.toFun_spec, Subtype.mk
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
n : ℕ
inst_2 : NeZero n
t : L
ht : IsPrimitiveRoot t n
⊢ (g : (a : L) → L) t = t ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)

Tactic:
toFun_spec' g (SetLike.coe_mem ht.toRootsOfUnity)

Premises used: IsPrimitiveRoot.toRootsOfUnity, SetLike.coe_mem, modularCyclotomicCharacter.toFun_spec'
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ c.val) : L)
apply : ∀ (ζ : ↥(rootsOfUnity n L)), ζ ^ c.val = ζ ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)
⊢ c = χ₀ n g

Tactic:
apply IsCyclic.ext Nat.card_eq_fintype_card (fun ζ ↦ ?_)

Premises used: IsCyclic.ext, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ c.val) : L)
ζ : ↥(rootsOfUnity n L)
⊢ (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)

Tactic:
specialize hc ζ
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
this : (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)
⊢ ζ ^ c.val = ζ ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)

Tactic:
exact_mod_cast this
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
suffices :
  (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)
⊢ ζ ^ c.val = ζ ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)

Tactic:
suffices ((ζ ^ c.val : Lˣ) : L) = (ζ ^ (χ₀ n g).val : Lˣ) by exact_mod_cast this
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : (g : (a : L) → L) (↑(↑ζ : Lˣ) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
rw : (↑((↑ζ : Lˣ) ^ c.val) : L) = (g : (a : L) → L) (↑(↑ζ : Lˣ) : L)
rw₁ rw₂ : (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ c.val) : L)
⊢ (↑((↑ζ : Lˣ) ^ c.val) : L) = (↑((↑ζ : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) : L)

Tactic:
rw [← toFun_spec g ζ, hc]

Premises used: modularCyclotomicCharacter.toFun_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
hc : ∀ (t : Lˣ), Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t → (g : (a : L) → L) (↑t : L) = (↑t : L) ^ c.val
⊢ c = χ₀ n g

Tactic:
toFun_unique n g c (fun ⟨_, ht⟩ ↦ hc _ ht)

Premises used: Units.val, Subtype.mk, HPow.hPow, _private.0.modularCyclotomicCharacter.toFun_unique'.match_1, modularCyclotomicCharacter.toFun_unique, Subtype.val, Eq, DFunLike.coe, ZMod.val
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
⊢ Eq (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n (RingEquiv.refl L)) 1

Tactic:
(toFun_unique n (RingEquiv.refl L) 1 <| fun t ↦ ?_).symm

Premises used: RingEquiv.refl, modularCyclotomicCharacter.toFun_unique, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
refine :
  ∀ (t : ↥(rootsOfUnity n L)),
    (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
      (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
⊢ Eq (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n (RingEquiv.refl L)) 1

Tactic:
refine (toFun_unique n (RingEquiv.refl L) 1 <| fun t ↦ ?_).symm

Premises used: RingEquiv.refl, modularCyclotomicCharacter.toFun_unique, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
⊢ 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)

Tactic:
have : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L } := Fin.size_positive'
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
inl :
  ∀ (h : 1 < Fintype.card.{u} ↥(rootsOfUnity n L)),
    (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
      (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
inr :
  ∀ (h : 1 = Fintype.card.{u} ↥(rootsOfUnity n L)),
    (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
      (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)

Tactic:
obtain (h | h) := this.lt_or_eq

Premises used: LE.le.lt_or_eq
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 < Fintype.card.{u} ↥(rootsOfUnity n L)
⊢ Fact (1 < Fintype.card.{u} ↥(rootsOfUnity n L))

Tactic:
have := Fact.mk h
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this_1 : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 < Fintype.card.{u} ↥(rootsOfUnity n L)
this : Fact (1 < Fintype.card.{u} ↥(rootsOfUnity n L))
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)

Tactic:
simp [ZMod.val_one]

Premises used: ZMod.val_one
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 = Fintype.card.{u} ↥(rootsOfUnity n L)
⊢ Subsingleton.{u + 1} ↥(rootsOfUnity n L)

Tactic:
have := Fintype.card_le_one_iff_subsingleton.mp h.ge
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this_1 : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 = Fintype.card.{u} ↥(rootsOfUnity n L)
this : Subsingleton.{u + 1} ↥(rootsOfUnity n L)
⊢ t = 1

Tactic:
Subsingleton.elim t 1

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
t : ↥(rootsOfUnity n L)
this_1 : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 = Fintype.card.{u} ↥(rootsOfUnity n L)
this : Subsingleton.{u + 1} ↥(rootsOfUnity n L)
inr :
  (RingEquiv.refl L : (a : L) → L) (↑(↑1 : Lˣ) : L) =
    (↑(HPow.hPow (α := Lˣ) (↑1 : Lˣ) (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1)) : L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)

Tactic:
obtain rfl : t = 1 := Subsingleton.elim t 1

Premises used: Subsingleton.elim, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
this_1 : 1 ≤ Fintype.card.{u} ↥(rootsOfUnity n L)
h : 1 = Fintype.card.{u} ↥(rootsOfUnity n L)
this : Subsingleton.{u + 1} ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑1 : Lˣ) : L) =
    (↑(HPow.hPow (α := Lˣ) (↑1 : Lˣ) (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1)) : L)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
⊢ χ₀ n (g * h) = HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n g) (χ₀ n h)

Tactic:
(toFun_unique n (g * h) _ <| fun ζ ↦ ?_).symm

Premises used: HMul.hMul, modularCyclotomicCharacter.toFun_unique, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
refine :
  ∀ (ζ : ↥(rootsOfUnity n L)),
    (g * h : (a : L) → L) (↑(↑ζ : Lˣ) : L) =
      (↑((↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n g) (χ₀ n h)).val) : L)
⊢ χ₀ n (g * h) = HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n g) (χ₀ n h)

Tactic:
refine (toFun_unique n (g * h) _ <| fun ζ ↦ ?_).symm

Premises used: HMul.hMul, modularCyclotomicCharacter.toFun_unique, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
change :
  (g : (a : L) → L) ((h : (a : L) → L) (↑(↑ζ : Lˣ) : L) : L) =
    (↑((↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n g) (χ₀ n h)).val) : L)
⊢ (g * h : (a : L) → L) (↑(↑ζ : Lˣ) : L) =
    (↑((↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n g) (χ₀ n h)).val) : L)

Tactic:
change g (h (ζ : Lˣ)) = _

Premises used: Units.val, Subtype.val, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
rw :
  (↑(↑(ζ ^
              (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n h) *
                ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g))) :
          Lˣ) :
      L) =
    (↑((↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val) : L)
⊢ (g : (a : L) → L) ((h : (a : L) → L) (↑(↑ζ : Lˣ) : L) : L) =
    (↑((↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n g) (χ₀ n h)).val) : L)

Tactic:
rw [toFun_spec, ← Subgroup.coe_pow, toFun_spec, mul_comm, Subgroup.coe_pow, ← pow_mul,
    ← Subgroup.coe_pow]

Premises used: Subgroup.coe_pow, modularCyclotomicCharacter.toFun_spec, pow_mul, mul_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
e_self :
  (↑(ζ ^
          (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n h) *
            ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g))) :
      Lˣ) =
    (↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val
⊢ (↑(↑(ζ ^
              (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n h) *
                ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g))) :
          Lˣ) :
      L) =
    (↑((↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val) : L)

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
e_self :
  ζ ^
      (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n h) *
        ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) =
    ζ ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val
⊢ (↑(ζ ^
          (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n h) *
            ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g))) :
      Lˣ) =
    (↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ζ ^
      (ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n h) *
        ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (χ₀ n g)) =
    ζ ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val

Tactic:
simp only [pow_eq_pow_iff_modEq, ← ZMod.natCast_eq_natCast_iff,
    ZMod.natCast_val, Nat.cast_mul, ZMod.cast_mul (m := orderOf ζ) orderOf_dvd_card]

Premises used: pow_eq_pow_iff_modEq, orderOf_dvd_card, ZMod.natCast_val, Nat.cast_mul, ZMod.natCast_eq_natCast_iff, ZMod.cast_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
t : Lˣ
ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t
⊢ (g : (a : L) → L) (↑t : L) =
    (↑t : L) ^
      ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L))
        (↑(((modularCyclotomicCharacter' L n : (L ≃+* L) →* (ZMod (Fintype.card.{u} ↥(rootsOfUnity n L)))ˣ) :
                (a : L ≃+* L) → (ZMod (Fintype.card ↥(rootsOfUnity n L)))ˣ)
              g) :
          ZMod (Fintype.card ↥(rootsOfUnity n L)))

Tactic:
modularCyclotomicCharacter.toFun_spec' g ht

Premises used: Polynomial.roots, modularCyclotomicCharacter.toFun, modularCyclotomicCharacter.toFun_spec', dite, Polynomial.nthRoots
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))
hc : ∀ (t : Lˣ), Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t → (g : (a : L) → L) (↑t : L) = (↑t : L) ^ c.val
⊢ c =
    (↑(((modularCyclotomicCharacter' L n : (L ≃+* L) →* (ZMod (Fintype.card.{u} ↥(rootsOfUnity n L)))ˣ) :
            (a : L ≃+* L) → (ZMod (Fintype.card ↥(rootsOfUnity n L)))ˣ)
          g) :
      ZMod (Fintype.card ↥(rootsOfUnity n L)))

Tactic:
modularCyclotomicCharacter.toFun_unique' _ _ _ hc

Premises used: Polynomial.roots, modularCyclotomicCharacter.toFun_unique', modularCyclotomicCharacter.toFun, dite, Polynomial.nthRoots
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
hn : Fintype.card.{u} ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t
rw :
  (↑t : L) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (toFun n g) =
    (↑t : L) ^ ZMod.val (n := n) (↑((modularCyclotomicCharacter L hn : (a : L ≃+* L) → (ZMod n)ˣ) g) : ZMod n)
⊢ (g : (a : L) → L) (↑t : L) =
    (↑t : L) ^ ZMod.val (n := n) (↑((modularCyclotomicCharacter L hn : (a : L ≃+* L) → (ZMod n)ˣ) g) : ZMod n)

Tactic:
rw [toFun_spec' g ht]

Premises used: modularCyclotomicCharacter.toFun_spec'