The Lean 4 theorem `gen_stoneGroup_eq` in the `ChapterStoneTheorem` chapter of the timepiece formalization

-- Generated from ChapterStoneTheorem.lean — theorem BookProof.ChapterStoneResolvent.UnboundedSelfAdjoint.gen_stoneGroup_eq
import Mathlib
import Definitions.Def_ChapterStoneTheorem
import Definitions.Def_ChapterStoneConverse
import Definitions.Def_ChapterStoneResolvent
import Definitions.Def_ChapterSirkTrotterKato
open BookProof.ChapterStoneMeasurable
open BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup
open BookProof.ChapterStoneResolvent.UnboundedSelfAdjoint

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable [TopologicalSpace.SeparableSpace H]


open scoped InnerProductSpace

theorem BookProof.ChapterStoneResolvent.UnboundedSelfAdjoint.gen_stoneGroup_eq (T : UnboundedSelfAdjoint H) : T.stoneGroup.gen = T := by sorry