!4#3472, GroupTheory.Perm.Cycle.Concrete

Stream: mathlib4

[Jeremy Tan]

!4#3472 how do I fix Quot.hrecOn here (L139)?

def formPerm : ∀ (s : Cycle α) (h : Nodup s), Equiv.Perm α :=
  fun s => Quot.hrecOn s (fun l h => List.formPerm l) fun l₁ l₂ (h : l₁ ~r l₂) => by
    ext
    · exact h.nodup_iff
    · intro h₁ h₂ _
      exact heq_of_eq (formPerm_eq_of_isRotated h₁ h)

And what do I do with all the deprecated functions?