Theorem: rootsOfUnity.integer_power_of_ringEquiv (AntLorentz/CyclotomicCharacter.lean)

State before:
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
⊢ ∃ m, ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
Tactic:
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (g.restrictRootsOfUnity n).toMonoidHom
State after:
case intro
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : { x // x ∈ rootsOfUnity n L }), ↑(MulEquiv.toMonoidHom (RingEquiv.restrictRootsOfUnity g n)) g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)

State before:
case intro
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : { x // x ∈ rootsOfUnity n L }), ↑(MulEquiv.toMonoidHom (RingEquiv.restrictRootsOfUnity g n)) g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
Tactic:
exact ⟨m, by simp [← hm]⟩
State after:
no goals

State before:
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : { x // x ∈ rootsOfUnity n L }), ↑(MulEquiv.toMonoidHom (RingEquiv.restrictRootsOfUnity g n)) g_1 = g_1 ^ m
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
Tactic:
simp [← hm]
State after:
no goals