no goals
E✝ : Type ?u.1969525
inst✝¹² : NormedAddCommGroup E✝
inst✝¹¹ : NormedSpace ℝ E✝
inst✝¹⁰ : MeasurableSpace E✝
inst✝⁹ : BorelSpace E✝
inst✝⁸ : FiniteDimensional ℝ E✝
μ✝ : Measure E✝
inst✝⁷ : IsAddHaarMeasure μ✝
F : Type ?u.1970194
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : CompleteSpace F
s : Set E✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
x : E
r : ℝ
this : closedBall 0 r = (fun x x_1 => x + x_1) x ⁻¹' closedBall x r
⊢ ↑↑μ (closedBall x r) = ↑↑μ (closedBall 0 r)
rw [this, measure_preimage_add]
no goals
E✝ : Type ?u.1969525
inst✝¹² : NormedAddCommGroup E✝
inst✝¹¹ : NormedSpace ℝ E✝
inst✝¹⁰ : MeasurableSpace E✝
inst✝⁹ : BorelSpace E✝
inst✝⁸ : FiniteDimensional ℝ E✝
μ✝ : Measure E✝
inst✝⁷ : IsAddHaarMeasure μ✝
F : Type ?u.1970194
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : CompleteSpace F
s : Set E✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
x : E
r : ℝ
⊢ closedBall 0 r = (fun x x_1 => x + x_1) x ⁻¹' closedBall x r
simp [preimage_add_closedBall]