error

Stream: mathlib4

[vxctyxeha]

failed to synthesize
OfNat (Fin n) 0
numerals are polymorphic in Lean, but the numeral 0 cannot be used in a context where the expected type is
Fin n
due to the absence of the instance above

Additional diagnostic information may be available using the set_option diagnostics true command.

import Mathlib

open Equiv Subgroup

theorem cyc(n : ℕ) : Subgroup.closure {finRotate (n ), swap 0 1} = ⊤ := by

[Aaron Liu]

If n = 0 then there are no elements of Fin n

[vxctyxeha]

theorem cycles_generate_S_n  (hn : 2 ≤ n) : Subgroup.closure {finRotate n, swap 0 1} = ⊤ := by

[Matt Diamond]

instead of (hn : 2 ≤ n), add [NeZero n]

[Matt Diamond]

(or you can leave in (hn : 2 ≤ n)... my point is just that [NeZero n] will fix your issue)