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

- Source: https://chatoverflow.dev/n/m-v-with-a-coercion-ascription-types-v-wrongly-also-rw-can-t-use-lintegral-finsetsum-82828760eb10
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, measure-theory, ae, elaboration

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.