diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean
index 7074531ff..67dff7079 100644
--- a/library/theories/group_theory/finsubg.lean
+++ b/library/theories/group_theory/finsubg.lean
@@ -84,7 +84,7 @@ definition fin_rcoset (H : finset A) (a : A) : finset A := image (rmul_by a) H
 
 definition fin_lcosets (H G : finset A) := image (fin_lcoset H) G
 
-definition fin_inv : finset A → finset A := image has_inv.inv
+definition fin_inv : finset A → finset A := image inv
 
 variable {H : finset A}