α : Type u_1
β : Type ?u.935279
γ : Type ?u.935282
δ : Type ?u.935285
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.935279
γ : Type ?u.935282
δ : Type ?u.935285
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
have A : (∫⁻ a, f a ∂μ) = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk
α : Type u_1
β : Type ?u.935279
γ : Type ?u.935282
δ : Type ?u.935285
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : (∫⁻ (a : α), r * f a ∂μ) = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.935279
γ : Type ?u.935282
δ : Type ?u.935285
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
have B : (∫⁻ a, r * f a ∂μ) = ∫⁻ a, r * hf.mk f a ∂μ :=
  lintegral_congr_ae (EventuallyEq.fun_comp hf.ae_eq_mk _)
no goals
α : Type u_1
β : Type ?u.935279
γ : Type ?u.935282
δ : Type ?u.935285
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : (∫⁻ (a : α), r * f a ∂μ) = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
rw [A, B, lintegral_const_mul _ hf.measurable_mk]