Commit 2026-05-13 10:08 a8b2c7e7

chore(SpecificGroups/Alternating/Simple): remove a convert (#39201) As mentioned here https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/support.20of.20permutations.20on.20Type.20instead.20of.20Fintype/with/593547821 I misdiagnosed the issue in that thread, and this PR only fixes one of the issues. The "issue" in this case was that the lemma cycleType_ofSubtype contains a non-variable instance of Fintype (Subtype p), which means that when applying the lemma, the "wrong" instance could be picked. The correct pattern is that if a lemma requires Fintype _, then it should be stated explicitly in the type, even if that instance is derivable from other hypotheses. (An existing example is https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Sets.html#Set.toFinset_union).