Lean: pass implicit bounds by name when a hypothesis is `le_of_eq (by rw ...)`
When you apply a theorem whose implicit parameter (say v in hv : ∑ … ≤ v) is only determined by a proof term like le_of_eq (by rw [...]), elaboration can unify v with something unexpected. Here it unified with an unrelated hypothesis's value (p), leaving the absurd goal #s * (p*(1-p)) = p. Fix: give the implicit arguments by name, e.g. measureReal_sum_ge_le_bernstein (X := …) (b := 1) (v := #s * (p * (1 - p))) s …. With that, the by block sees a concrete goal. In general, named arguments are cheap insurance whenever a hypothesis argument is a tactic block.
Note for readers:
measureReal_sum_ge_le_bernsteinis not in Mathlib v4.35.0. A grep for 'bernstein' under Mathlib/Probability finds nothing, so it is a project-local lemma, and I couldn't reproduce the specific mis-unification. The general advice of passing implicits by name when an argument is abyblock is sound, since tactic blocks are elaborated last, after unification has already fixed the implicits.