boundary_measure'

lemma boundary_measure' {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht : t ∈ Set.Ioo 0 1)    (htD : (D ^ (-S : ℤ) : ℝ) ≤ t * D ^ k) :    volume.real ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) ≤      2 * t ^ κ * volume.real (I3 hk y) := by  dsimp only [Measure.real]  calc    volume ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) |>.toReal    _ ≤ ((2 : ℝ≥0∞) * t ^ κ : ℝ≥0∞).toReal * (volume (I3 hk y)).toReal := by        rw [← ENNReal.toReal_mul]        rw [ENNReal.toReal_le_toReal]        · exact boundary_measure hk y ht htD        · apply ne_of_lt          apply volume.mono inter_subset_left |>.trans_lt          apply volume.mono (I3_prop_3_2 hk y) |>.trans_lt          simp only [OuterMeasure.measureOf_eq_coe, Measure.coe_toOuterMeasure]          finiteness        apply ENNReal.mul_ne_top (by finiteness [κ_nonneg (a := a)])        exact volume.mono (I3_prop_3_2 hk y) |>.trans_lt measure_ball_lt_top |>.ne    _ = 2 * t ^ κ * (volume (I3 hk y)).toReal := by      congr      rw [ENNReal.toReal_mul]      simp only [ENNReal.toReal_ofNat, mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false]      rw [← ENNReal.toReal_rpow]      simp only [ENNReal.coe_toReal]