case intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h : IsCyclic G
σ : G →* G
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
case intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
obtain ⟨m, hm⟩ := hG (σ h)
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
g : G
⊢ ↑σ g = g ^ m
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
refine' ⟨m, fun g => _⟩
case intro.intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
n : ℤ
⊢ ↑σ ((fun x x_1 => x ^ x_1) h n) = (fun x x_1 => x ^ x_1) h n ^ m
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
g : G
⊢ ↑σ g = g ^ m
obtain ⟨n, rfl⟩ := hG g
no goals
case intro.intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
n : ℤ
⊢ ↑σ ((fun x x_1 => x ^ x_1) h n) = (fun x x_1 => x ^ x_1) h n ^ m
rw [MonoidHom.map_zpow, ← hm, ← zpow_mul, ← zpow_mul']