case intro
M : Type ?u.1286508
N : Type ?u.1286511
G : Type ?u.1286514
R : Type u_2
S : Type ?u.1286520
F : Type u_1
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ+
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : RingHomClass F R R
σ : F
ζ : { x // x ∈ rootsOfUnity k R }
m : ℤ
hm : ∀ (g : { x // x ∈ rootsOfUnity k R }), ↑(restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m, ↑σ ↑↑ζ = ↑↑ζ ^ m
M : Type ?u.1286508
N : Type ?u.1286511
G : Type ?u.1286514
R : Type u_2
S : Type ?u.1286520
F : Type u_1
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ+
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : RingHomClass F R R
σ : F
ζ : { x // x ∈ rootsOfUnity k R }
⊢ ∃ m, ↑σ ↑↑ζ = ↑↑ζ ^ m
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k)
case intro
M : Type ?u.1286508
N : Type ?u.1286511
G : Type ?u.1286514
R : Type u_2
S : Type ?u.1286520
F : Type u_1
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ+
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : RingHomClass F R R
σ : F
ζ : { x // x ∈ rootsOfUnity k R }
m : ℤ
hm : ∀ (g : { x // x ∈ rootsOfUnity k R }), ↑(restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑ζ ^ Int.toNat (m % ↑(orderOf ζ)) = ↑↑ζ ^ m_1
case intro
M : Type ?u.1286508
N : Type ?u.1286511
G : Type ?u.1286514
R : Type u_2
S : Type ?u.1286520
F : Type u_1
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ+
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : RingHomClass F R R
σ : F
ζ : { x // x ∈ rootsOfUnity k R }
m : ℤ
hm : ∀ (g : { x // x ∈ rootsOfUnity k R }), ↑(restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m, ↑σ ↑↑ζ = ↑↑ζ ^ m
rw [← restrictRootsOfUnity_coe_apply, hm, zpow_eq_mod_orderOf, ← Int.toNat_of_nonneg
    (m.emod_nonneg (Int.coe_nat_ne_zero.mpr (pos_iff_ne_zero.mp (orderOf_pos ζ)))),
  zpow_ofNat, rootsOfUnity.coe_pow]
no goals
case intro
M : Type ?u.1286508
N : Type ?u.1286511
G : Type ?u.1286514
R : Type u_2
S : Type ?u.1286520
F : Type u_1
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ+
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : RingHomClass F R R
σ : F
ζ : { x // x ∈ rootsOfUnity k R }
m : ℤ
hm : ∀ (g : { x // x ∈ rootsOfUnity k R }), ↑(restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑ζ ^ Int.toNat (m % ↑(orderOf ζ)) = ↑↑ζ ^ m_1
exact ⟨(m % orderOf ζ).toNat, rfl⟩