case h
α : Type u_1
β : Type ?u.1005086
γ : Type ?u.1005089
δ : Type ?u.1005092
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ENNReal.ofReal (ENNReal.toReal (f a)) = f a
α : Type u_1
β : Type ?u.1005086
γ : Type ?u.1005089
δ : Type ?u.1005092
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ (fun x => ENNReal.ofReal (ENNReal.toReal (f x))) =ᵐ[μ] f
filter_upwards [hf]
case h
α : Type u_1
β : Type ?u.1005086
γ : Type ?u.1005089
δ : Type ?u.1005092
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ENNReal.ofReal (ENNReal.toReal (f x)) = f x
case h
α : Type u_1
β : Type ?u.1005086
γ : Type ?u.1005089
δ : Type ?u.1005092
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ENNReal.ofReal (ENNReal.toReal (f a)) = f a
intro x hx
no goals
case h
α : Type u_1
β : Type ?u.1005086
γ : Type ?u.1005089
δ : Type ?u.1005092
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ENNReal.ofReal (ENNReal.toReal (f x)) = f x
simp only [hx.ne, ofReal_toReal, Ne.def, not_false_iff]