measurable space instances on p-adics and completions

Stream: mathlib4

[Kevin Buzzard]

import Mathlib

#synth MeasurableSpace ℝ -- works and is `borel _`
#synth MeasurableSpace ℂ -- works and is `borel _`

-- even the abstraction works
variable (K : Type*) [RCLike K] in
#synth MeasurableSpace K -- works and is `borel _`

-- but everything below fails

-- completion of ℚ at ∞ is not a measurable space (it's canonically ℝ)
variable (v : NumberField.InfinitePlace ℚ) in
#synth MeasurableSpace v.Completion -- fails

-- more generally completion of a number field at an infinite place is not a measurable space
-- it's RCLike, modulo a choice of √-1 in the ℂ case
variable (K : Type*) [Field K] [NumberField K] (v : NumberField.InfinitePlace K) in
#synth MeasurableSpace (v.Completion) -- fails

-- 2-adic numbers are not a measurable space
#synth MeasurableSpace ℚ_[2] -- fails

-- p-adic numbers are not a measurable space
variable (p : ℕ) [Fact p.Prime] in
#synth MeasurableSpace ℚ_[p] -- fails

open NumberField in
-- completion of a number field at a finite place isn't a measurable space either
variable (K : Type*) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) in
#synth MeasurableSpace (v.adicCompletion K) -- fails

It seems that the analysts cannot conceive of any sensible measurable space structure on $\mathbb{R}$ or $\mathbb{C}$ (or even on their RCLike abstraction) other than the Borel measurable space. Analogously, I cannot conceive of any sensible measurable space structure on the $p$-adics or on completions of number fields at finite or infinite places other than borel _. Would these be acceptable instances in mathlib?