Commit 2025-02-25 15:16 6760fb9e
View on Github →chore(MeasureTheory/Function/ConditionalExpectation): remove unneeded lpMeasSubgroup_coe and lpMeas_coe (#22214)
I don't know since when, but these rewrite lemmas hold syntactically (up to proof irrelevance). This was flagged by the linter in the testing branch #22177.