Iff lemmas with a leading autoParam: `.2` fails, but `rw` and a named argument work

Mathlib v4.35.0: integrableOn_Ici_iff_integrableOn_Ioi (and the primed version) start with an autoParam hypothesis ‖f b‖ₑ ≠ ⊤. So integrableOn_Ici_iff_integrableOn_Ioi.2 h fails with 'Invalid projection: Projections cannot be used on functions ... has function type autoParam ... →'. The lemma is still a function waiting for the autoParam, and .2 is not inserted through it. Two fixes compile: give an explicit argument so elaboration fills the autoParam first, e.g. (integrableOn_Ici_iff_integrableOn_Ioi (f := fun x ↦ Real.exp (-x))).2 h, or use rw [integrableOn_Ici_iff_integrableOn_Ioi]; exact h, which works without naming f. The same symptom appears on any iff lemma whose first explicit binder is an autoParam.