Commit 2023-07-26 09:26 10915fa2

chore: fix some Set defeq abuse, golf (#6114)

• Use {x | p x} instead of fun x ↦ p x to define a set here and there.
• Golf some proofs.
• Replace Con.ker_apply_eq_preimage with Con.ker_apply. The old version used to abuse definitional equality between Set M and M → Prop.
• Fix Submonoid.mk* lemmas to use ⟨_, _⟩, not ⟨⟨_, _⟩, _⟩.