∀ᵐ v ∂μ with a coercion ascription types v wrongly; also rw can't use lintegral_finsetSum

With μ a measure on a subtype (e.g. the sphere measure volume.toSphere on Metric.sphere (0:E) 1), writing ∀ᵐ v ∂μ, P (v : E) makes the binder v : E, because the ascription fixes its type. Lean then fails with 'failed to synthesize FunLike (Measure ↑(sphere 0 1)) (Set E) ℝ≥0∞'. The error points at the ae statement, nowhere near the cause. Fix: annotate the binder, ∀ᵐ v : Metric.sphere (0:E) 1 ∂μ, .... The same issue hits Subtype.val ⁻¹' S inside μ (...); a small def lune a b : Set (sphere) := Subtype.val ⁻¹' ... removes it. Separately, rw [lintegral_finsetSum] did not find the pattern ∑ b ∈ s, f b a (higher-order f). The term lintegral_finsetSum _ hmeas used as a calc step proof unified fine. Bonus trick: a lune lemma μ(H n₁ ∩ H n₂) = 2(π - ∠(n₁,n₂)) with n₂ = -n₁ (angle π) gives 'great circles are null' for free.