-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_toReal_of_lintegral_ne_top {f : α → ℝ≥0∞} (hf : ∫⁻ x, f x ∂μ ≠ ∞) :
    HasFiniteIntegral (fun x ↦ (f x).toReal) μ

Proof state:
case neg.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h✝ : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ ENNReal.ofReal (↑fx).toReal ≤ ↑fx

Tactic:
simp [← h, ← NNReal.coe_le_coe]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ HasFiniteIntegral (fun x => (f x).toReal) μ

Tactic:
have h x : ‖(f x).toReal‖ₑ = .ofReal (f x).toReal := by
  rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ HasFiniteIntegral (fun x => (f x).toReal) μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : f x = ⊤
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
simp [hfx]

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ⊤
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
lift f x to ℝ≥0 using hfx with fx h

Result:
case neg.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h✝ : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ ENNReal.ofReal (↑fx).toReal ≤ ↑fx

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
x : α
⊢ ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal

Tactic:
rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
by_cases hfx : f x = ∞

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : f x = ⊤
⊢ ENNReal.ofReal (f x).toReal ≤ f x

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ⊤
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a).toReal ∂μ < ⊤

Tactic:
refine lt_of_le_of_lt (lintegral_mono fun x => ?_) (lt_top_iff_ne_top.2 hf)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ HasFiniteIntegral (fun x => (f x).toReal) μ

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, h]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a).toReal ∂μ < ⊤