-- Mathlib/MeasureTheory/Group/AddCircle.lean
theorem closedBall_ae_eq_ball {x : AddCircle T} {ε : ℝ} : closedBall x ε =ᵐ[volume] ball x ε

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ closedBall x ε =ᶠ[ae volume] ball x ε

Tactic:
rcases le_or_lt ε 0 with hε | hε

Result:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᶠ[ae volume] ball x ε

case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ closedBall x ε =ᶠ[ae volume] ball x ε

Proof state:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᶠ[ae volume] ball x ε

Tactic:
rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall,
  min_eq_right (by linarith [hT.out] : 2 * ε ≤ T), ENNReal.ofReal_eq_zero]

Result:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0

Proof state:
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))
⊢ volume (closedBall x ε) ≤ volume (ball x ε)

Tactic:
refine le_of_tendsto this <| mem_of_superset (Ioo_mem_nhdsLT hε) fun r hr ↦ ?_

Result:
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))
r : ℝ
hr : r ∈ Ioo 0 ε
⊢ r ∈ {x_1 | (fun c => volume (closedBall x c) ≤ volume (ball x ε)) x_1}

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun k => k) (𝓝[<] ε) (𝓝 ε)

Tactic:
exact nhdsWithin_le_nhds

Result:
no goals

Proof state:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos zero_le_two hε

Result:
no goals

Proof state:
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ volume (closedBall x ε) ≤ volume (ball x ε)

Tactic:
have : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 <| volume (closedBall x ε)) := by
  simp_rw [volume_closedBall]
  refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)
  exact nhdsWithin_le_nhds

Result:
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))
⊢ volume (closedBall x ε) ≤ volume (ball x ε)

Proof state:
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))
r : ℝ
hr : r ∈ Ioo 0 ε
⊢ r ∈ {x_1 | (fun c => volume (closedBall x c) ≤ volume (ball x ε)) x_1}

Tactic:
exact measure_mono (closedBall_subset_ball hr.2)

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))

Tactic:
simp_rw [volume_closedBall]

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ => ENNReal.ofReal (T ⊓ 2 * δ)) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (T ⊓ 2 * ε)))

Proof state:
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ closedBall x ε =ᶠ[ae volume] ball x ε

Tactic:
suffices volume (closedBall x ε) ≤ volume (ball x ε) from
  (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this
    measurableSet_ball.nullMeasurableSet (measure_ne_top _ _)).symm

Result:
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ volume (closedBall x ε) ≤ volume (ball x ε)

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ T

Tactic:
linarith [hT.out]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ => ENNReal.ofReal (T ⊓ 2 * δ)) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (T ⊓ 2 * ε)))

Tactic:
refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun k => k) (𝓝[<] ε) (𝓝 ε)