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

State before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∫ (x : ℝ) in s, DiracSeq b x ≠ 0
Tactic:
refine ne_of_gt ?_
State after:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ∫ (x : ℝ) in s, DiracSeq b x

State before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ∫ (x : ℝ) in s, DiracSeq b x
Tactic:
rw [set_integral_pos_iff_support_of_nonneg_ae]
State after:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume ((Function.support fun x => DiracSeq b x) ∩ s)

case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s

State before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume ((Function.support fun x => DiracSeq b x) ∩ s)

case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
. simp [DiracSeq.support hb.ne']
  exact hs
State after:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s

State before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
. refine Filter.eventually_of_forall ?_
  simp
  exact DiracSeq.nonneg hb.le
State after:
case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s

State before:
case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
. exact Integrable.integrableOn (DiracSeq.integrable hb)
State after:
no goals

State before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume ((Function.support fun x => DiracSeq b x) ∩ s)
Tactic:
simp [DiracSeq.support hb.ne']
State after:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume s

State before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume s
Tactic:
exact hs
State after:
no goals

State before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x
Tactic:
refine Filter.eventually_of_forall ?_
State after:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 x ≤ (fun x => DiracSeq b x) x

State before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 x ≤ (fun x => DiracSeq b x) x
Tactic:
simp
State after:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 ≤ DiracSeq b x

State before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 ≤ DiracSeq b x
Tactic:
exact DiracSeq.nonneg hb.le
State after:
no goals

State before:
case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
exact Integrable.integrableOn (DiracSeq.integrable hb)
State after:
no goals