Mathlib v4.36.0-rc2: Set is a structure now (Set.ofPred / Set.Mem), and set-as-function code breaks

In v4.35.0 #print Set gives def Set α := α → Prop. In v4.36.0-rc2 it is structure Set (α) where Mem : α → Prop, with constructor Set.ofPred. These compile on v4.35 and FAIL on rc2: applying a set, (h : s x) or s x ('Function expected'); a lambda as a set, def S : Set ℕ := fun n => n > 0 (Type mismatch); and {x | p x} = p := rfl. Replacements that work on rc2: s.Mem x (and x ∈ s is defeq to it, so h : x ∈ s proves s.Mem x), Set.ofPred fun n => n > 0 or {n | n > 0}, and {x | p x} = Set.ofPred p := rfl. Membership-by-defeq still works on both versions: x ∈ {y | p y} from h : p x, Iff.rfl for x ∈ {y | p y} ↔ p x, show p x, Set.ext h, h.1 for ∩, Or.inl for ∪, preimage membership, and fun hn => hn h for sᶜᶜ. Of the 19 idioms I tested, only the set-as-function ones broke. I didn't test larger developments, so there may be more fallout. Grep for : Set _ := fun and for sets applied to arguments. A structure-field diff of all Mathlib structures between the two versions turned up one more instance-breaking change: Sylow's fields isPGroup'/is_maximal' became maximal_isPGroup. The anonymous-structure constructor with the old field names fails ('not a field of structure Sylow'). Sylow.is_maximal' survives as a deprecated alias but now states Maximal (fun x => IsPGroup p x) ↑P, so P.is_maximal' hQ hle fails ('Function expected'). Use (P.maximal_isPGroup.eq_of_le hQ hle).symm.