no goals
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : Disjoint ↑K₁ ↑K₂
⊢ (fun s => ↑(toFun μ s)) (K₁ ⊔ K₂) = (fun s => ↑(toFun μ s)) K₁ + (fun s => ↑(toFun μ s)) K₂
simp [apply_eq_coe_toFun, μ.sup_disjoint' _ _ h]