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

State before:
c : ℂ
r : ℝ
rp : r > 0
⊢ ↑volume (Metric.closedBall c r) < ⊤
Tactic:
simp only [Complex.volume_closedBall]
State after:
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 * ↑NNReal.pi < ⊤

State before:
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 * ↑NNReal.pi < ⊤
Tactic:
apply ENNReal.mul_lt_top
State after:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 ≠ ⊤

case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ↑NNReal.pi ≠ ⊤

State before:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 ≠ ⊤
Tactic:
simp only [ne_eq, ENNReal.pow_eq_top_iff, ENNReal.ofReal_ne_top, OfNat.ofNat_ne_zero,
  not_false_eq_true, and_true]
State after:
no goals

State before:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ↑NNReal.pi ≠ ⊤
Tactic:
simp only [ne_eq, ENNReal.coe_ne_top, not_false_eq_true]
State after:
no goals

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

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

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