no goals
α : Type u_2
E : Type ?u.102358
F : Type ?u.102361
F' : Type ?u.102364
G : Type ?u.102367
𝕜 : Type ?u.102370
p : ℝ≥0∞
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
β✝ : Type ?u.102670
inst✝¹ : SeminormedAddCommGroup β✝
T✝ T' : Set α → β✝
C✝ C' : ℝ
β : Type u_1
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
m : MeasurableSpace α
hT : DominatedFinMeasAdditive 0 T C
s : Set α
hs : MeasurableSet s
⊢ ↑↑0 s = 0
simp only [Measure.coe_zero, Pi.zero_apply]