α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : { x // x ∈ zpowers a }
i : ℤ
hi : (fun x x_1 => x ^ x_1) a i = ↑b
⊢ ↑b ^ orderOf a = 1
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : { x // x ∈ zpowers a }
⊢ ↑b ^ orderOf a = 1
let ⟨i, hi⟩ := b.2
no goals
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : { x // x ∈ zpowers a }
i : ℤ
hi : (fun x x_1 => x ^ x_1) a i = ↑b
⊢ ↑b ^ orderOf a = 1
rw [← hi, ← zpow_ofNat, ← zpow_mul, mul_comm, zpow_mul, zpow_ofNat,
  pow_orderOf_eq_one, one_zpow]