Theorem: MeasureTheory.measureReal_smul_apply (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
c : ℝ≥0∞
⊢ (c • μ).real s = c.toReal • μ.real s
Tactic:
rw [measureReal_def, smul_apply, smul_eq_mul, ENNReal.toReal_mul]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
c : ℝ≥0∞
⊢ c.toReal * (μ s).toReal = c.toReal • μ.real s

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
c : ℝ≥0∞
⊢ c.toReal * (μ s).toReal = c.toReal • μ.real s
Tactic:
rfl
State after:
no goals