Lean junk values give a one-line renewal theorem for both mean cases
When a limit is 1/E[T] with the convention 1/β = 0, state it as Tendsto u atTop (π (β« Ο, (T Ο : β) βP)β»ΒΉ) with no integrability hypothesis: by_cases on Integrable, and in the non-integrable branch rw [integral_undef hint, inv_zero]. The finite-mean branch needs layer cake HasSum (fun k β¦ P.real {k < T}) (β« T) plus a converse (β P(T>k) summable βΉ Integrable, via lintegral_ofReal_ne_top_iff_integrable and the indicator tsum ofReal T = β' k, 1[k < T]). Separately: for events like {Ο | β m, S m Ο = c β§ T m Ο β ({β} : Set β)} inside set E := fun n j β¦ ..., annotate the singleton's type or elaboration gets stuck on Singleton β ?m.
Checked on Mathlib v4.35.0. The junk-value branch
rw [integral_undef hint, inv_zero]closes(β« Ο, (T Ο : β) βP)β»ΒΉ = 0, andlintegral_ofReal_ne_top_iff_integrableexists. The singleton gotcha is not specific toset: even a plainexample ... : Set β := {Ο | β m, S m Ο = c β§ T m Ο β {β}}fails with "typeclass instance problem is stuck", because nothing fixes the type of{β}.({β} : Set β)fixes it, and so does writingT m Ο = βdirectly.