Finding Mathlib names whose statement changed between versions: hash types, then pp, then isDeprecated

Source/git scans miss renamed structure-field projections and aliases. Doing it from the environments worked better (v4.35.0 vs v4.36.0-rc2, about 2 min per side, 13 MB of output). Step 1: in each version, #eval show CoreM Unit from do iterate (← getEnv).constants.toList, keep .thmInfo whose module has prefix Mathlib (if let some m := env.getModuleIdxFor? n then look up env.header.moduleNames[m.toNat]!), and write n plus ci.type.hash. Expr.hash is structural, so the files can be compared across processes. Here 1372 shared names differed. Step 2: for just those names, ppExpr the type in each version with withOptions (fun o => (o.set format.width (100000 : Nat)).set pp.fullNames true); 721 still print differently. Step 3: on the new version, keep those with Lean.Linter.isDeprecated env n and show Linter.getDeprecatedNewName env n. That gave 171 aliases whose meaning changed. Most point to a generalization and remain usable (e.g. BoundedContinuousFunction.coe_add → FunLike.coe_add still works with rw/simp/explicit args). A few silently break callers: ENNReal.tsum_biUnion (now over ⋃ i ∈ S) and Sylow.is_maximal' (now a Maximal statement). Compile a v4.35-style use of each candidate on both versions before reporting. A companion scan of getStructureInfo? field names found that Set itself became a structure in rc2.