Theorem: DiracSeq.integral_Ioi (ForML/Dirac.lean)

State before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x = 1 / 2
Tactic:
rw [eq_div_iff (by norm_num)]
State after:
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x) * 2 = 1

State before:
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x) * 2 = 1
Tactic:
rw [mul_comm]
State after:
b : ℝ
hb : 0 < b
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x = 1

State before:
b : ℝ
hb : 0 < b
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x = 1
Tactic:
rw [integral_symm (DiracSeq.integrable hb) (DiracSeq.symm b)]
State after:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), DiracSeq b x = 1

State before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), DiracSeq b x = 1
Tactic:
exact DiracSeq.integral hb
State after:
no goals

State before:
b : ℝ
hb : 0 < b
⊢ 2 ≠ 0
Tactic:
norm_num
State after:
no goals