Integral split near far

lemma integral_split_near_far {α x t : ℝ} (g : ℝ → ℝ) (far : Set ℝ)    (hα : 0 < α) (ht : 0 < t)    (hg : Integrable g) (h_meas_far : MeasurableSet far):    ∫ y, heatKernel α (x - y) t * (g y - g x) ∂volume =      (∫ y in farᶜ, heatKernel α (x - y) t * (g y - g x) ∂volume) +      ∫ y in far,  heatKernel α (x - y) t * (g y - g x) ∂volume := by   have h_int : Integrable (fun y => heatKernel α (x - y) t * (g y - g x)) := by    have h1 : Integrable (fun y => heatKernel α (x - y) t * g y) :=      integrable_heatKernel_mul_of_L1 g hα ht hg    have h2 : Integrable (fun y => heatKernel α (x - y) t * g x) :=      (integrable_heatKernel_slice hα ht (x:= x)).mul_const (g x)    have h_eq : (fun y => heatKernel α (x - y) t * (g y - g x)) =                (fun y => heatKernel α (x - y) t * g y) - (fun y => heatKernel α (x - y) t * g x) := by      ext y      simp [mul_sub]    rw [h_eq]    exact Integrable.sub h1 h2   exact (integral_add_compl (s := far) h_meas_far h_int).symm.trans (by rw [add_comm])