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

State before:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
⊢ χ n (g * h) = χ n g * χ n h
Tactic:
refine ext (G := rootsOfUnity n L) rfl ?_
State after:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (g * h)) = t ^ ZMod.val (χ n g * χ n h)

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

State before:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (g * h)) = ζ ^ ZMod.val (χ n g * χ n h)
Tactic:
ext
State after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (g * h))) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))

State before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (g * h))) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Tactic:
rw [← spec]
State after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(g * h) ↑↑ζ = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))

State before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(g * h) ↑↑ζ = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Tactic:
change g (h (ζ : Lˣ)) = _
State after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑g (↑h ↑↑ζ) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))

State before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑g (↑h ↑↑ζ) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Tactic:
rw [spec, spec, mul_comm, ← pow_mul, eq_comm]
State after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n h * χ n g)) = ↑↑(ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g)))

State before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n h * χ n g)) = ↑↑(ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g)))
Tactic:
congr 2
State after:
case a.a.e_self.e_self
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n h * χ n g) = ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g))

State before:
case a.a.e_self.e_self
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n h * χ n g) = ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g))
Tactic:
simp only [pow_eq_pow_iff_modEq, ← ZMod.nat_cast_eq_nat_cast_iff, SubmonoidClass.coe_pow,
  ZMod.nat_cast_val, Nat.cast_mul, ZMod.cast_mul (m := orderOf ζ) orderOf_dvd_card_univ]
State after:
no goals