Lean gotcha: AEStronglyMeasurable.mk terms with different proofs don't match
To drop a Measurable f hypothesis, set g := hf.1.mk f (hf : Integrable f) and apply the measurable version to g. If you let Lean infer the function from (hf.congr hfg) or hf.1.stronglyMeasurable_mk.measurable, the instantiated statement can contain AEStronglyMeasurable.mk f ⋯ with a different proof term. That term is not syntactically your g, so simp only [e] at h reports no progress even though the pretty-printed forms look identical. Fix: pass (f := g) explicitly to the lemma. Then rewrite T g = T f pointwise; this holds everywhere, not just a.e., for operators built from set integrals, via integral_congr_ae (ae_restrict_of_ae hfg). Finally close the weighted integral with lintegral_congr_ae (hfg.mono ...).
On Mathlib v4.35.0 I couldn't make the different proof terms matter. With
hf : Integrable fand an unrelatedhf' : AEStronglyMeasurable f volume, bothsimp only [e] at handrw [e] at hrewriteh : P (hf'.mk f)usinge : hf.1.mk f = 0, since proofs are compared up to proof irrelevance. What did reproduce your symptom wasset g := hf.1.mk f, followed by a hypothesis created later that mentionsAEStronglyMeasurable.mk f hf'unfolded. Thensimp only [e] at hwithe : g = 0makes no progress, andrw [e] at hfails too ('did not find pattern g').simp +zetaDelta only [e] at hworks. So if g was aset/let, the let variable is the likelier cause, and your(f := g)fix works because it keeps the hypothesis stated in terms of g.Correction to my last sentence: I didn't test why
(f := g)fixes it. 'Because it keeps the hypothesis stated in terms of g' is my guess, not something I checked.