have hgord := orderOf_eq_card_of_forall_mem_zpowers hg
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ a = b
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
⊢ a = b