awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
⊢ (RingEquiv.refl L : (a : L) → L) (↑(↑t : Lˣ) : L) =
    (↑((↑t : Lˣ) ^ ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L)) 1) : L)
have 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)
Tactic: obtain rfl : t = 1 := Subsingleton.elim t 1
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
have 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)
Tactic: refine (toFun_unique n (g * h) _ <| fun ζ ↦ ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
ζ : ↥(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)
have 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)
Tactic: change g (h (ζ : Lˣ)) = _
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n 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)
have 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)
Tactic: rw [toFun_spec, ← Subgroup.coe_pow, toFun_spec, mul_comm, Subgroup.coe_pow, ← pow_mul,
    ← Subgroup.coe_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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))) :
          Lˣ) :
      L) =
    (↑((↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val) : L)
have 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
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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))) :
      Lˣ) =
    (↑ζ : Lˣ) ^ (HMul.hMul (α := ZMod (Fintype.card.{u} ↥(rootsOfUnity n L))) (χ₀ n h) (χ₀ n g)).val
have 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
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ (g : (a : L) → L) (↑t : L) =
    (↑t : L) ^ ZMod.val (n := n) (↑((modularCyclotomicCharacter L hn : (a : L ≃+* L) → (ZMod n)ˣ) g) : ZMod n)
have 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)
Tactic: rw [toFun_spec' g ht]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ (↑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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ (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)
have rw : (↑t : L) ^ c.val =
  (↑t : L) ^
    ZMod.val (n := Fintype.card.{u} ↥(rootsOfUnity n L))
      ((ZMod.ringEquivCongr sorry : (a : ZMod n) → ZMod (Fintype.card ↥(rootsOfUnity n L))) c)
Tactic: rw [hc t ht, ZMod.ringEquivCongr_val]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
⊢ (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)
have rw₁ : (↑t : L) ^ c.val = (↑t : L) ^ c.val
Tactic: rw [hc t ht, ZMod.ringEquivCongr_val]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ c = (ZMod.ringEquivCongr hn : (a : ZMod (Fintype.card ↥(rootsOfUnity n L))) → ZMod n) (toFun n g)
have rw : c =
  (ZMod.ringEquivCongr hn : (a : ZMod (Fintype.card ↥(rootsOfUnity n L))) → ZMod n)
    ((ZMod.ringEquivCongr sorry : (a : ZMod n) → ZMod (Fintype.card ↥(rootsOfUnity n L))) c)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
⊢ c = (ZMod.ringEquivCongr hn : (a : ZMod (Fintype.card ↥(rootsOfUnity n L))) → ZMod n) (toFun n g)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
⊢ c = (ZMod.ringEquivCongr hn : (a : ZMod (Fintype.card ↥(rootsOfUnity n L))) → ZMod n) (toFun n g)
have rw₂ : c = c
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ 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)ˣ)
have huv : Eq (α := ZMod n) (↑(((autToPow R hμ : (L ≃ₐ[R] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[R] L) → (ZMod n)ˣ) g) : ZMod n)
  (↑((modularCyclotomicCharacter L sorry : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ 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)
have 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 sorry : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)
Tactic: apply ZMod.val_injective
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
have 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 sorry : (a : L ≃+* L) → (ZMod n)ˣ) g.toRingEquiv) : ZMod n)
Tactic: apply hμ.pow_inj (ZMod.val_lt _) (ZMod.val_lt _)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)) (χ 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))
have rw : Eq (α := ZMod (p ^ n))
  ((PadicInt.toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (PadicInt.ofIntSeq (fun (x : ℕ) ↦ aux g (p ^ x)) sorry) :
    ZMod (p ^ n))
  ((↑(((modularCyclotomicCharacter L sorry : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
      ZMod (p ^ n)) :
    ZMod (p ^ n))
Tactic: rw [toFun_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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))
have refine : Eq (α := ZMod (p ^ n)) (↑(aux g (p ^ n)) : ZMod (p ^ n))
  (↑(((modularCyclotomicCharacter L sorry : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
    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 ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
⊢ (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))
have rw : (g : (a : L) → L) (↑(↑t : Lˣ) : L) =
  (↑(↑t : Lˣ) : L) ^
    ZMod.val (n := p ^ n)
      (↑(((modularCyclotomicCharacter L sorry : (L ≃+* L) →* (ZMod (p ^ n))ˣ) : (a : L ≃+* L) → (ZMod (p ^ n))ˣ) g) :
        ZMod (p ^ n))
Tactic: rw [toZModPow_toFun, ← modularCyclotomicCharacter.spec (ht := t.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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))
⊢ (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))
have rw₁ : Eq (α := L) ((g : (a : L) → L) (↑(↑t : Lˣ) : L) : L) ((g : (a : L) → L) (↑(↑t : Lˣ) : L) : L)
Tactic: rw [toZModPow_toFun, ← modularCyclotomicCharacter.spec (ht := t.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
p : ℕ
inst_3 : Fact (Nat.Prime p)
⊢ Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1
have pos : ∀ (H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)), Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1
Tactic: by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1
have neg : ∀ (H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)), Eq (α := ℤ_[p]) (cyclotomicCharacter.toFun.{u} (L := L) p 1) 1
Tactic: by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
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
have x : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
Tactic: haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
have 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))
Tactic: refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ cyclotomicCharacter.toFun p (f * g) =
    HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)
have pos : ∀ (H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
  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)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
⊢ cyclotomicCharacter.toFun p (f * g) =
    HMul.hMul (α := ℤ_[p]) (cyclotomicCharacter.toFun p f) (cyclotomicCharacter.toFun p g)
have neg : ∀ (H : ¬∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i)),
  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)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
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)
have x : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
Tactic: haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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)
have 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))
Tactic: refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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
⊢ 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]ˣ)
have 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]ˣ)
Tactic: by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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]ˣ)
⊢ 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]ˣ)
have 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]ˣ)
Tactic: by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (goal)
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]ˣ)
    (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
      (a : Gal(L/K)) → ℤ_[p]ˣ)
have neg : Continuous (X := Gal(L/K)) (Y := ℤ_[p]ˣ)
  (Function.comp (β := L ≃+* L)
    (⇑(MonoidHom.toHomUnits { toFun := fun (g : L ≃+* L) ↦ 1, map_one' := sorry, map_mul' := sorry }) : (a : L ≃+* L) → ℤ_[p]ˣ)
    (⇑(MulSemiringAction.toRingAut Gal(L/K) L) : (a : Gal(L/K)) → L ≃+* L))
Tactic: simp only [cyclotomicCharacter, cyclotomicCharacter.toFun, dif_neg H, MonoidHom.coe_comp]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (hypothesis)
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]ˣ)
    (⇑(MonoidHom.comp (N := L ≃+* L) (cyclotomicCharacter L p) (MulSemiringAction.toRingAut Gal(L/K) L)) :
      (a : Gal(L/K)) → ℤ_[p]ˣ)
have x : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
Tactic: haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩