Lean4
/-- Given a `s : Cycle α` such that `Nodup s`, retrieve the previous element before `x ∈ s`. -/
nonrec def prev : ∀ (s : Cycle α) (_hs : Nodup s) (x : α) (_hx : x ∈ s), α := fun s =>
Quot.hrecOn (motive := fun (s : Cycle α) => ∀ (_hs : Cycle.Nodup s) (x : α) (_hx : x ∈ s), α) s
(fun l _hn x hx => prev l x hx) fun l₁ l₂ h =>
Function.hfunext (propext h.nodup_iff) fun h₁ h₂ _he =>
Function.hfunext rfl fun x y hxy =>
Function.hfunext (propext (by rw [eq_of_heq hxy]; simpa [eq_of_heq hxy] using h.mem_iff)) fun hm hm' he' =>
heq_of_eq
(by rw [heq_iff_eq] at hxy; subst x; simpa using isRotated_prev_eq h h₁ _)
-- `simp` cannot infer the proofs: see `prev_reverse_eq_next'` for `@[simp]` lemma.
