rwa [pow_eq_pow_iff_modEq, Nat.ModEq, Nat.mod_eq_of_lt, Nat.mod_eq_of_lt] at hxy
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x = y % orderOf g
⊢ y < orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ x < orderOf g