Theorem: ModularCyclotomicCharacter.spec (AntLorentz/CyclotomicCharacter.lean)

State before:
L : Type u
inst✝ : Field L
n✝ : ℕ+
g : L ≃+* L
n : ℕ+
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ ZMod.val (χ n g))
Tactic:
rintro t
State after:
L : Type u
inst✝ : Field L
n✝ : ℕ+
g : L ≃+* L
n : ℕ+
t : { x // x ∈ rootsOfUnity n L }
⊢ ↑g ↑↑t = ↑↑(t ^ ZMod.val (χ n g))

State before:
L : Type u
inst✝ : Field L
n✝ : ℕ+
g : L ≃+* L
n : ℕ+
t : { x // x ∈ rootsOfUnity n L }
⊢ ↑g ↑↑t = ↑↑(t ^ ZMod.val (χ n g))
Tactic:
rw [ModularCyclotomicCharacter_aux_spec g n t, ← zpow_ofNat, ModularCyclotomicCharacter.toFun,
    ZMod.val_int_cast, ←Group.pow_eq_zpow_mod _ pow_card_eq_one]
State after:
no goals