Heat Tail change Of Variables

lemma heatTail_changeOfVariables    {α x δ t : ℝ} (hα : 0 < α) (ht : 0 < t) :  (∫ y, Set.indicator {y : ℝ | δ ≤ |y - x|}            (fun y => heatKernel α (x - y) t) y)  = (1 / Real.sqrt Real.pi) *    ∫ z, Set.indicator           {z : ℝ | (δ / Real.sqrt (4 * α * t)) ≤ |z|}           (fun z => Real.exp (-z^2)) z := by    unfold heatKernel     let s : ℝ := Real.sqrt (4 * α * t)    have s_pos: 0 < s := by positivity     calc       ∫ (y : ℝ), {y | δ ≤ |y - x|}.indicator (fun y ↦ 1 / √(4 * Real.pi * α * t) * Real.exp (-(x - y) ^ 2 / (4 * α * t))) y        = ∫ z, Set.indicator {z : ℝ | δ ≤ |z|}               (fun z => 1 / √(4 * Real.pi * α * t) * Real.exp (-z^2 / (4 * α * t))) z := by          simp only [abs_sub_comm]          exact integral_sub_left_eq_self (fun z =>                 Set.indicator {z : ℝ | δ ≤ |z|} (fun z => 1 / √(4 * Real.pi * α * t) * Real.exp (-z^2 / (4 * α * t))) z)                 (μ := volume) (x : ℝ)      _ = ∫ z, Set.indicator {z : ℝ | δ / s ≤ |s⁻¹  * z|}               (fun z => 1 / √(4 * Real.pi * α * t) * Real.exp (-(s⁻¹ * z)^2)) z := by            congr 1; ext z;            simp only [Set.indicator]            congr 1            · simp only [Set.mem_setOf_eq]              rw [div_le_iff₀' s_pos, abs_mul, abs_inv, abs_of_pos s_pos]              field_simp [s_pos.ne.symm]            · congr 2              field_simp [s_pos.ne.symm]; rw [Real.sq_sqrt (by positivity)]; ring      _ = 1 / √(4 * Real.pi * α * t) * ∫ z, Set.indicator {z : ℝ | δ / s ≤ |s⁻¹  * z|}               (fun z => Real.exp (-(s⁻¹ * z)^2)) z := by          simp [Set.indicator_const_mul]          rw [integral_const_mul]      _ =  1 / √(4 * Real.pi * α * t) * (s * ∫ z, Set.indicator {z : ℝ | δ / s ≤ |z|}               (fun z => Real.exp (-z^2)) z) := by          congr 1          set f : ℝ → ℝ := fun u ↦ {u | δ / s ≤ |u|}.indicator (fun u => Real.exp (-u ^ 2)) u          have hf : (fun z ↦ {z | δ / s ≤ |s⁻¹ * z|}.indicator (fun z => Real.exp (-(s⁻¹ * z) ^ 2)) z) =            (fun z ↦ f (s⁻¹ * z)) := by            ext z; dsimp [f]; rfl          rw [hf, integral_comp_mul_left f s⁻¹, inv_inv, abs_of_pos]; rfl; exact s_pos      _ = (1 / Real.sqrt Real.pi) * ∫ z, Set.indicator           {z : ℝ | δ / s ≤ |z|}           (fun z => Real.exp (-z^2)) z := by             unfold s; rw [← mul_assoc]; field_simp             rw [ mul_right_comm, mul_comm ];             rw [ mul_comm, ← Real.sqrt_mul <| by positivity ]             ac_rfl