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

-- Generated from ChapterStoneTheorem.lean — theorem BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.ext'
import Mathlib
import Definitions.Def_ChapterStoneTheorem
import Definitions.Def_ChapterStoneMeasurable
import Definitions.Def_ChapterStoneConverse
open BookProof.ChapterStoneMeasurable
open BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]


open scoped InnerProductSpace

theorem BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.ext_prime :
    ∀ {G G' : WeakMeasurableUnitaryGroup H}, (∀ t, G.U t = G'.U t) → G = G' := by sorry