. conv => arg 1; intro b; arg 1; intro x; rw [DiracSeq.eq_comp_mul]
  simp
  simp [intervalIntegral.integral_comp_mul_left]
  rw [inv_eq_one_div, ← DiracSeq.integral_Ioi zero_lt_one]
  apply intervalIntegral_tendsto_integral_Ioi
  . apply Integrable.integrableOn
    exact DiracSeq.integrable zero_lt_one
  . exact Tendsto.atTop_mul_const ha tendsto_coe_coe_pnat_atTop
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
no goals