Quotient by an involutive function

Stream: Is there code for X?

[Eric Wieser]

Do we have a more general version of the Setoid relation used for docs#Sym2, that takes any involutive function f (not just Prod.swap), and generates the quotient by the relation r x y := x = y ∨ x = f y?

[Eric Wieser]

That is,

abbrev Setoid.ofInvolutive {α} (f : α → α) (hf : Function.Involutive f) : Setoid α where
  r x y := x = y ∨ x = f y
  iseqv := by
    refine ⟨fun x => .inl rfl, fun {x y} => Or.imp Eq.symm fun h => hf.eq_iff.mp h.symm, fun {x y z} => ?_⟩
    rintro (rfl | hxy) (rfl | hyz)
    · exact .inl rfl
    · exact .inr hyz
    · exact .inr hxy
    · exact .inl <| hxy.trans <| hf.eq_iff.mpr hyz