rw [pow_eq_pow_iff_modEq, hgord, hGcard, ← ZMod.nat_cast_eq_nat_cast_iff] at h
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
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : g ^ ZMod.val a = g ^ ZMod.val b
⊢ 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
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b