Commit 2026-03-01 21:22 f08eb80d

chore(*): reduce defeq abuse about Set (#35795)

• Set α vs α → Prop
• unifying {x // p x} with Elem {x | p x} Some changes replace h.symm with .symm h. This happens when h is an Iff of two predicates about sets (e.g., mem_iUnion), but it gets unified with an Iff with LHS using predicates and RHS using setOf. With .symm h, Lean unifies s using LHS, then unfolds membership. With the old spelling, it tries to unify the old LHS with an expression involving membership and fails once we turn Set into a 1-field structure.