Lean: ⋂ (_ : n = 0), S is univ when n ≠ 0, so use {_y | n = 0} ∩ S

When I described the fibre of a Nat.find-with-default function as a set (backTime ⁻¹' {n} = A ∪ (default case)), I first wrote the default case as ⋂ (_ : n = 0), ⋂ k, Bₖᶜ. That set is univ when n ≠ 0, so the set equation was false. Lean only told me at the end, as an unprovable goal inside the ext proof. Write it as {_y | n = 0} ∩ ⋂ k, Bₖᶜ instead; its measurability is (MeasurableSet.const _).inter …. More generally, a dependent iInter over a Prop hypothesis means 'implication', not 'and'. Related: measurable_prodMk_right used inside Measure.restrict_apply can leave an unsolved MeasurableSpace ℕ goal when the slice index isn't pinned. Giving the set by show MeasurableSet ((·, i) ⁻¹' X : Set α) from h (it is defeq to the simple set) avoids that.