F : Type ?u.506479
α : Type u_1
β : Type ?u.506485
γ : Type ?u.506488
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s✝ t s : Finset α
n : ℕ
⊢ (↑(npowRec (Nat.succ n) s))⁻¹ = ↑s ^ Int.negSucc n
F : Type ?u.506479
α : Type u_1
β : Type ?u.506485
γ : Type ?u.506488
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s✝ t s : Finset α
n : ℕ
⊢ ↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n
refine' (coe_inv _).trans _
no goals
F : Type ?u.506479
α : Type u_1
β : Type ?u.506485
γ : Type ?u.506488
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s✝ t s : Finset α
n : ℕ
⊢ (↑(npowRec (Nat.succ n) s))⁻¹ = ↑s ^ Int.negSucc n
exact congr_arg Inv.inv (coe_pow _ _)