awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e_a :
  ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (toFun n g) =
    ZMod.val (n := n) (↑((modularCyclotomicCharacter L hn : (a : L ≃+* L) → (ZMod n)ˣ) g) : ZMod n)
⊢ (↑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)

Tactic:
congr 1
-- 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
⊢ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (toFun n g) =
    ZMod.val (n := n) (↑((modularCyclotomicCharacter L hn : (a : L ≃+* L) → (ZMod n)ˣ) g) : ZMod n)

Tactic:
(ZMod.ringEquivCongr_val _ _).symm

Premises used: Polynomial.roots, modularCyclotomicCharacter.toFun, dite, Polynomial.nthRoots, Eq.symm, ZMod.ringEquivCongr_val
-- 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
⊢ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) (toFun n g) =
    ZMod.val (n := n) (↑((modularCyclotomicCharacter L hn : (a : L ≃+* L) → (ZMod n)ˣ) g) : ZMod n)

Tactic:
exact (ZMod.ringEquivCongr_val _ _).symm

Premises used: Eq.symm, ZMod.ringEquivCongr_val
-- 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
c : ZMod n
hc : ∀ (t : Lˣ), Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t → (g : (a : L) → L) (↑t : L) = (↑t : L) ^ c.val
t : Lˣ
ht : Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t
rw :
  (↑t : L) ^ c.val =
    (↑t : L) ^
      ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L))
        ((ZMod.ringEquivCongr ⋯ : (a : ZMod n) → ZMod (Fintype.card ↥(rootsOfUnity n L))) c)
rw₁ rw₂ : (↑t : L) ^ c.val = (↑t : L) ^ c.val
⊢ (g : (a : L) → L) (↑t : L) =
    (↑t : L) ^
      ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L))
        ((ZMod.ringEquivCongr ⋯ : (a : ZMod n) → ZMod (Fintype.card ↥(rootsOfUnity n L))) c)

Tactic:
rw [hc t ht, ZMod.ringEquivCongr_val]

Premises used: ZMod.ringEquivCongr_val
-- 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
c : ZMod n
hc : ∀ (t : Lˣ), Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t → (g : (a : L) → L) (↑t : L) = (↑t : L) ^ c.val
rw :
  c =
    (ZMod.ringEquivCongr hn : (a : ZMod (Fintype.card ↥(rootsOfUnity n L))) → ZMod n)
      ((ZMod.ringEquivCongr ⋯ : (a : ZMod n) → ZMod (Fintype.card ↥(rootsOfUnity n L))) c)
rw₁ :
  c =
    (ZMod.ringEquivCongr hn : (a : ZMod (Fintype.card ↥(rootsOfUnity n L))) → ZMod n)
      (((ZMod.ringEquivCongr hn).symm : (a : ZMod n) → ZMod (Fintype.card ↥(rootsOfUnity n L))) c)
rw₂ rw₃ : c = c
⊢ c = (ZMod.ringEquivCongr hn : (a : ZMod (Fintype.card ↥(rootsOfUnity n L))) → ZMod n) (toFun n g)

Tactic:
rw [← toFun_unique' n g (ZMod.ringEquivCongr hn.symm c)
    (fun t ht ↦ by rw [hc t ht, ZMod.ringEquivCongr_val]), ← ZMod.ringEquivCongr_symm hn,
    RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, modularCyclotomicCharacter.toFun_unique', ZMod.ringEquivCongr, ZMod.ringEquivCongr_symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
R : Type u_1
inst_3 : CommRing R
inst_4 : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
huv :
  Eq (α := ZMod n) (↑(((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g) : ZMod n)
    (↑((modularCyclotomicCharacter L ⋯ : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)
⊢ Eq (α := (ZMod n)ˣ) (((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
    ((modularCyclotomicCharacter L ⋯ : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv : (ZMod n)ˣ)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
R : Type u_1
inst_3 : CommRing R
inst_4 : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
huv :
  ZMod.val (n := n) (↑(((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g) : ZMod n) =
    ZMod.val (n := n) (↑((modularCyclotomicCharacter L ⋯ : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)
⊢ Eq (α := ZMod n) (↑(((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g) : ZMod n)
    (↑((modularCyclotomicCharacter L ⋯ : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)

Tactic:
apply ZMod.val_injective

Premises used: ZMod.val_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
R : Type u_1
inst_3 : CommRing R
inst_4 : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
huv :
  μ ^ ZMod.val (n := n) (↑(((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g) : ZMod n) =
    μ ^ ZMod.val (n := n) (↑((modularCyclotomicCharacter L ⋯ : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)
⊢ ZMod.val (n := n) (↑(((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g) : ZMod n) =
    ZMod.val (n := n) (↑((modularCyclotomicCharacter L ⋯ : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)

Tactic:
apply hμ.pow_inj (ZMod.val_lt _) (ZMod.val_lt _)

Premises used: IsPrimitiveRoot.pow_inj, ZMod.val_lt
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
R : Type u_1
inst_3 : CommRing R
inst_4 : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ μ ^ ZMod.val (n := n) (↑(((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g) : ZMod n) =
    μ ^ ZMod.val (n := n) (↑((modularCyclotomicCharacter L ⋯ : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)

Tactic:
simpa only [autToPow_spec R hμ g, modularCyclotomicCharacter, RingEquiv.toMulEquiv_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, modularCyclotomicCharacter', MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply, Units.coe_mapEquiv, MonoidHom.coe_toHomUnits, MonoidHom.coe_mk,
    OneHom.coe_mk, RingEquiv.coe_toMulEquiv, ZMod.ringEquivCongr_val, AlgEquiv.coe_ringEquiv]
    using modularCyclotomicCharacter.toFun_spec'' g hμ

Premises used: MonoidHom.coe_comp, MulEquiv.toMonoidHom_eq_coe, modularCyclotomicCharacter', RingEquiv.coe_toMulEquiv, OneHom.coe_mk, modularCyclotomicCharacter, MonoidHom.coe_toHomUnits, MonoidHom.coe_coe, AlgEquiv.coe_ringEquiv, MonoidHom.coe_mk, RingEquiv.toMulEquiv_eq_coe, Function.comp_apply, IsPrimitiveRoot.autToPow_spec, ZMod.ringEquivCongr_val, Units.coe_mapEquiv, modularCyclotomicCharacter.toFun_spec''
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
g : L ≃+* L
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
⊢ Eq (α := ℤ_[p]) (χ p g) (PadicInt.ofIntSeq (fun (x : ℕ) ↦ aux g (p ^ x)) ⋯)

Tactic:
dif_pos fun _ ↦ HasEnoughRootsOfUnity.exists_primitiveRoot _ _

Premises used: dif_pos, cyclotomicCharacter.toFun, HasEnoughRootsOfUnity.exists_primitiveRoot
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
g : L ≃+* L
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
rw :
  Eq (α := ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (PadicInt.ofIntSeq (fun (x : ℕ) ↦ aux g (p ^ x)) ⋯) :
      ZMod (p ^ n))
    ((↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
        ZMod (p ^ n)) :
      ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (χ p g) : ZMod (p ^ n))
    ((↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
        ZMod (p ^ n)) :
      ZMod (p ^ n))

Tactic:
rw [toFun_apply]

Premises used: cyclotomicCharacter.toFun_apply
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
g : L ≃+* L
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ Eq (α := ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (PadicInt.ofIntSeq (fun (x : ℕ) ↦ aux g (p ^ x)) ⋯) :
      ZMod (p ^ n))
    ((↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
        ZMod (p ^ n)) :
      ZMod (p ^ n))

Tactic:
(PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub (aux g <| p ^ ·) _ (fun i ↦
    pow_dvd_aux_pow_sub_aux_pow g p i.le_succ) n).trans ?_

Premises used: modularCyclotomicCharacter.aux, modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow, PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub, Nat.le_succ, HPow.hPow, Eq.trans
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
g : L ≃+* L
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
refine :
  Eq (α := ZMod (p ^ n)) (↑(aux g (p ^ n)) : ZMod (p ^ n))
    (↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
      ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (PadicInt.ofIntSeq (fun (x : ℕ) ↦ aux g (p ^ x)) ⋯) :
      ZMod (p ^ n))
    ((↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
        ZMod (p ^ n)) :
      ZMod (p ^ n))

Tactic:
refine (PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub (aux g <| p ^ ·) _ (fun i ↦
    pow_dvd_aux_pow_sub_aux_pow g p i.le_succ) n).trans ?_

Premises used: modularCyclotomicCharacter.aux, modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow, PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub, Nat.le_succ, HPow.hPow, Eq.trans
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
g : L ≃+* L
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ Eq (α := ZMod (p ^ n)) (↑(aux g (p ^ n)) : ZMod (p ^ n))
    (↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
      ZMod (p ^ n))

Tactic:
simp [modularCyclotomicCharacter, modularCyclotomicCharacter', modularCyclotomicCharacter.toFun]

Premises used: modularCyclotomicCharacter.toFun, modularCyclotomicCharacter', modularCyclotomicCharacter
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
g : L ≃+* L
n : ℕ
t : ↥(rootsOfUnity (p ^ n) L)
rw :
  (g : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑(↑t : Lˣ) : L) ^
      ZMod.val (n := p ^ n)
        (↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
          ZMod (p ^ n))
rw₁ rw₂ : Eq (α := L) ((g : (a : L) → L) (↑(↑t : Lˣ) : L) : L) ((g : (a : L) → L) (↑(↑t : Lˣ) : L) : L)
⊢ (g : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑(↑t : Lˣ) : L) ^ ZMod.val (n := p ^ n) ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (χ p g))

Tactic:
rw [toZModPow_toFun, ← modularCyclotomicCharacter.spec (ht := t.2)]

Premises used: modularCyclotomicCharacter.spec, cyclotomicCharacter.toZModPow_toFun, Subtype.property
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
pos :
  ∀ (H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
    Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1
neg :
  ∀ (H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
    Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1
⊢ Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
⊢ ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)

Tactic:
haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
⊢ Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1

Tactic:
PadicInt.ext_of_toZModPow.mp fun n ↦ ?_

Premises used: PadicInt.ext_of_toZModPow, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
pos :
  ∀ (n : ℕ),
    Eq (α := ZMod (p ^ n))
      ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (cyclotomicCharacter.toFun.{u} (L := L) p 1) : ZMod (p ^ n))
      ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) 1 : ZMod (p ^ n))
⊢ Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1

Tactic:
refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_

Premises used: PadicInt.ext_of_toZModPow, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n_1 : ℕ
inst_2 : NeZero n_1
p : ℕ
inst_3 : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ Eq (α := ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (cyclotomicCharacter.toFun.{u} (L := L) p 1) : ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) 1 : ZMod (p ^ n))

Tactic:
simp [cyclotomicCharacter.toZModPow_toFun]

Premises used: cyclotomicCharacter.toZModPow_toFun
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
⊢ Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1

Tactic:
simp [cyclotomicCharacter.toFun, dif_neg H]

Premises used: cyclotomicCharacter.toFun, dif_neg
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
f g : L ≃+* L
pos :
  ∀ (H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
    cyclotomicCharacter.toFun p (f * g) =
      HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)
neg :
  ∀ (H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
    cyclotomicCharacter.toFun p (f * g) =
      HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)
⊢ cyclotomicCharacter.toFun p (f * g) =
    HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
⊢ ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)

Tactic:
haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) =
    HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)

Tactic:
PadicInt.ext_of_toZModPow.mp fun n ↦ ?_

Premises used: PadicInt.ext_of_toZModPow, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
pos :
  ∀ (n : ℕ),
    Eq (α := ZMod (p ^ n))
      ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (cyclotomicCharacter.toFun p (f * g)) : ZMod (p ^ n))
      ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
          (HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)) :
        ZMod (p ^ n))
⊢ cyclotomicCharacter.toFun p (f * g) =
    HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)

Tactic:
refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_

Premises used: PadicInt.ext_of_toZModPow, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n_1 : ℕ
inst_2 : NeZero n_1
p : ℕ
inst_3 : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
h : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ Eq (α := ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (cyclotomicCharacter.toFun p (f * g)) : ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
        (HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)) :
      ZMod (p ^ n))

Tactic:
simp [cyclotomicCharacter.toZModPow_toFun]

Premises used: cyclotomicCharacter.toZModPow_toFun
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
f g : L ≃+* L
H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) =
    HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)

Tactic:
simp [cyclotomicCharacter.toFun, dif_neg H]

Premises used: cyclotomicCharacter.toFun, dif_neg
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
n : ℕ
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
g : L ≃+* L
t : L
ht : t ^ p ^ n = 1
⊢ (g : (a : L) → L) t =
    t ^
      ZMod.val (n := p ^ n)
        ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
          (↑(((cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ) : (a : L ≃+* L) → ℤ_[p]ˣ) g) : ℤ_[p]))

Tactic:
toFun_spec p g (rootsOfUnity.mkOfPowEq _ ht)

Premises used: cyclotomicCharacter.toFun, dite, rootsOfUnity.mkOfPowEq, cyclotomicCharacter.toFun_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
p : ℕ
inst_2 : Fact (Nat.Prime p)
n : ℕ
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
g : L ≃+* L
⊢ Eq (α := ZMod (p ^ n))
    ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
      (↑(((cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ) : (a : L ≃+* L) → ℤ_[p]ˣ) g) : ℤ_[p]))
    (↑(((modularCyclotomicCharacter L ⋯ : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
      ZMod (p ^ n))

Tactic:
toZModPow_toFun _ _ _

Premises used: cyclotomicCharacter.toFun, dite, cyclotomicCharacter.toZModPow_toFun
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
pos :
  ∀ (H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
    Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
      (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
        (a : Gal(L/K)) → ℤ_[p]ˣ)
neg :
  ∀ (H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
    Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
      (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
        (a : Gal(L/K)) → ℤ_[p]ˣ)
⊢ Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
      (a : Gal(L/K)) → ℤ_[p]ˣ)

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
neg :
  Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (Function.comp (β := L ≃+* L)
      (⇑(MonoidHom.toHomUnits { toFun := fun (g : L ≃+* L) ↦ 1, map_one' := ⋯, map_mul' := ⋯ }) :
        (a : L ≃+* L) → ℤ_[p]ˣ)
      (⇑(MulSemiringAction.toRingAut Gal(L/K) L) : (a : Gal(L/K)) → L ≃+* L))
⊢ Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
      (a : Gal(L/K)) → ℤ_[p]ˣ)

Tactic:
simp only [cyclotomicCharacter, cyclotomicCharacter.toFun, dif_neg H, MonoidHom.coe_comp]

Premises used: MonoidHom.coe_comp, cyclotomicCharacter.toFun, dif_neg, cyclotomicCharacter
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (Function.comp (β := L ≃+* L)
      (⇑(MonoidHom.toHomUnits { toFun := fun (g : L ≃+* L) ↦ 1, map_one' := ⋯, map_mul' := ⋯ }) :
        (a : L ≃+* L) → ℤ_[p]ˣ)
      (⇑(MulSemiringAction.toRingAut Gal(L/K) L) : (a : Gal(L/K)) → L ≃+* L))

Tactic:
continuous_const (y := 1)

Premises used: continuous_const
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
    (Function.comp (β := L ≃+* L)
      (⇑(MonoidHom.toHomUnits { toFun := fun (g : L ≃+* L) ↦ 1, map_one' := ⋯, map_mul' := ⋯ }) :
        (a : L ≃+* L) → ℤ_[p]ˣ)
      (⇑(MulSemiringAction.toRingAut Gal(L/K) L) : (a : Gal(L/K)) → L ≃+* L))

Tactic:
exact continuous_const (y := 1)

Premises used: continuous_const
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)
⊢ ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)

Tactic:
haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩