no goals
α : Type u_3
β : Type ?u.668179
m : MeasurableSpace α
L : Type ?u.668185
M : Type u_4
N : Type u_2
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DistribMulAction R N
inst✝ : ContinuousConstSMul R N
r : R
h : v ⟂ᵥ w
s : Set α
hmeas : MeasurableSet s
hs₁ : ∀ (t : Set α), t ⊆ s → ↑v t = 0
hs₂ : ∀ (t : Set α), t ⊆ sᶜ → ↑w t = 0
t : Set α
ht : t ⊆ sᶜ
⊢ ↑(r • w) t = 0
simp only [coe_smul, Pi.smul_apply, hs₂ t ht, smul_zero]