no goals
α : Type u_1
E : Type ?u.12375
F : Type ?u.12378
F' : Type ?u.12381
G : Type ?u.12384
𝕜 : Type ?u.12387
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_2
inst✝ : AddCommMonoid β
T T' : Set α → β
s t : Set α
x✝⁴ : MeasurableSet s
x✝³ : MeasurableSet t
x✝² : ↑↑μ s ≠ ⊤
x✝¹ : ↑↑μ t ≠ ⊤
x✝ : s ∩ t = ∅
⊢ OfNat.ofNat 0 (s ∪ t) = OfNat.ofNat 0 s + OfNat.ofNat 0 t
simp