Theorem: LocalVolume.closedBall (Ray/Hartogs/FubiniBall.lean)

State before:
c : ℂ
r : ℝ
rp : r > 0
⊢ LocalVolumeSet (Metric.closedBall c r)
Tactic:
apply LocalVolume.closure_interior
State after:
case bp
c : ℂ
r : ℝ
rp : r > 0
⊢ ∀ (x : ℂ), ∀ r > 0, ↑volume (ball x r) > 0

case ci
c : ℂ
r : ℝ
rp : r > 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))

State before:
case bp
c : ℂ
r : ℝ
rp : r > 0
⊢ ∀ (x : ℂ), ∀ r > 0, ↑volume (ball x r) > 0
Tactic:
intro x r rp
State after:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ ↑volume (ball x r) > 0

State before:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ ↑volume (ball x r) > 0
Tactic:
simp only [Complex.volume_ball, gt_iff_lt, CanonicallyOrderedCommSemiring.mul_pos,
  ENNReal.coe_pos, NNReal.pi_pos, and_true]
State after:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r ^ 2

State before:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r ^ 2
Tactic:
apply ENNReal.pow_pos
State after:
case bp.a
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r

State before:
case bp.a
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r
Tactic:
bound
State after:
no goals

State before:
case ci
c : ℂ
r : ℝ
rp : r > 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))
Tactic:
have rz := rp.ne'
State after:
case ci
c : ℂ
r : ℝ
rp : r > 0
rz : r ≠ 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))

State before:
case ci
c : ℂ
r : ℝ
rp : r > 0
rz : r ≠ 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))
Tactic:
simp only [interior_closedBall c rz, closure_ball c rz, subset_refl]
State after:
no goals