Theorem: Complex.volume_closedBall' (Ray/Hartogs/FubiniBall.lean)

State before:
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Tactic:
have c : ContinuousOn (fun _ : ℂ ↦ (1 : ℝ)) (closedBall c r) := continuousOn_const
State after:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2

State before:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2
Tactic:
have f := fubini_ball c
State after:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
f : ∫ (z : ℂ) in closedBall c✝ r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2

State before:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
f : ∫ (z : ℂ) in closedBall c✝ r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2
Tactic:
clear c
State after:
c : ℂ
r : ℝ
rp : r ≥ 0
f : ∫ (z : ℂ) in closedBall c r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2

State before:
c : ℂ
r : ℝ
rp : r ≥ 0
f : ∫ (z : ℂ) in closedBall c r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Tactic:
simp only [ENNReal.toReal_ofReal Real.two_pi_pos.le, ←
  intervalIntegral.integral_of_le rp, integral_const, Measure.restrict_apply, MeasurableSet.univ,
  univ_inter, Algebra.id.smul_eq_mul, mul_one, Real.volume_Ioc, tsub_zero,
  intervalIntegral.integral_mul_const, integral_id, zero_pow, Ne, bit0_eq_zero,
  Nat.one_ne_zero, not_false_iff] at f
State after:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 / 2 * (2 * π)
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2

State before:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 / 2 * (2 * π)
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Tactic:
ring_nf at f ⊢
State after:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 * π
⊢ (↑volume (closedBall c r)).toReal = r ^ 2 * π

State before:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 * π
⊢ (↑volume (closedBall c r)).toReal = r ^ 2 * π
Tactic:
exact f
State after:
no goals