α : Type u_1
β : Type u_2
γ : Type ?u.69543
ι : Type ?u.69546
inst✝¹ : Countable ι
f g : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
f_approx : ℕ → α →ₛ β :=
  fun n =>
    { toFun := ↑(StronglyMeasurable.approx hf n),
      measurableSet_fiber' := (_ : ∀ (x : β), MeasurableSet (↑(StronglyMeasurable.approx hf n) ⁻¹' {x})),
      finite_range' := (_ : Set.Finite (range ↑(StronglyMeasurable.approx hf n))) }
⊢ StronglyMeasurable f
α : Type u_1
β : Type u_2
γ : Type ?u.69543
ι : Type ?u.69546
inst✝¹ : Countable ι
f g : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
⊢ StronglyMeasurable f
let f_approx : ℕ → @SimpleFunc α m β := fun n =>
  @SimpleFunc.mk α m β
    (hf.approx n)
    (fun x => h_mono _ (SimpleFunc.measurableSet_fiber' _ x))
    (SimpleFunc.finite_range (hf.approx n))
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.69543
ι : Type ?u.69546
inst✝¹ : Countable ι
f g : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
f_approx : ℕ → α →ₛ β :=
  fun n =>
    { toFun := ↑(StronglyMeasurable.approx hf n),
      measurableSet_fiber' := (_ : ∀ (x : β), MeasurableSet (↑(StronglyMeasurable.approx hf n) ⁻¹' {x})),
      finite_range' := (_ : Set.Finite (range ↑(StronglyMeasurable.approx hf n))) }
⊢ StronglyMeasurable f
exact ⟨f_approx, hf.tendsto_approx⟩