lint(data/zmod/quotient): fix fintype/finite (#17613)

urkud · urkud · commit d8ac338019a0 · 2022-11-20T12:16:16.000Z
diff --git a/src/data/zmod/quotient.lean b/src/data/zmod/quotient.lean
@@ -152,9 +152,10 @@ attribute [to_additive orbit_zmultiples_equiv_symm_apply'] orbit_zpowers_equiv_s
   minimal_period ((•) a) b = fintype.card (orbit (zpowers a) b) :=
 by rw [←fintype.of_equiv_card (orbit_zpowers_equiv a b), zmod.card]
 
-@[to_additive] instance minimal_period_pos [fintype $ orbit (zpowers a) b] :
+@[to_additive] instance minimal_period_pos [finite $ orbit (zpowers a) b] :
   ne_zero $ minimal_period ((•) a) b :=
 ⟨begin
+  casesI nonempty_fintype (orbit (zpowers a) b),
   haveI : nonempty (orbit (zpowers a) b) := (orbit_nonempty b).to_subtype,
   rw minimal_period_eq_card,
   exact fintype.card_ne_zero,
