case pos
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : r = 0
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ

case neg
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
by_cases h : r = 0
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
case neg
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
apply le_antisymm _ (lintegral_const_mul_le r f)
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
have rinv : r * r⁻¹ = 1 := ENNReal.mul_inv_cancel h hr
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
have rinv' : r⁻¹ * r = 1 := by
  rw [mul_comm]
  exact rinv
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : (r⁻¹ * ∫⁻ (a : α), r * f a ∂μ) ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
have := lintegral_const_mul_le (μ := μ) r⁻¹ fun x => r * f x
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : (r⁻¹ * ∫⁻ (a : α), r * f a ∂μ) ≤ ∫⁻ (a : α), f a ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : (r⁻¹ * ∫⁻ (a : α), r * f a ∂μ) ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
simp [(mul_assoc _ _ _).symm, rinv'] at this
no goals
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : (r⁻¹ * ∫⁻ (a : α), r * f a ∂μ) ≤ ∫⁻ (a : α), f a ∂μ
⊢ (∫⁻ (a : α), r * f a ∂μ) ≤ r * ∫⁻ (a : α), f a ∂μ
simpa [(mul_assoc _ _ _).symm, rinv] using mul_le_mul_left' this r
no goals
case pos
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : r = 0
⊢ (∫⁻ (a : α), r * f a ∂μ) = r * ∫⁻ (a : α), f a ∂μ
simp [h]
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ r * r⁻¹ = 1
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ r⁻¹ * r = 1
rw [mul_comm]
no goals
α : Type u_1
β : Type ?u.937326
γ : Type ?u.937329
δ : Type ?u.937332
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ r * r⁻¹ = 1
exact rinv