∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ], Measurable f → MeasureTheory.FinStronglyMeasurable f μ