α : Type u_1
β : Type u_2
γ : Type ?u.729415
δ : Type ?u.729418
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
eq : (fun a => ↑‖‖f a‖‖₊) = fun a => ↑‖f a‖₊
⊢ HasFiniteIntegral fun a => ‖f a‖
α : Type u_1
β : Type u_2
γ : Type ?u.729415
δ : Type ?u.729418
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
⊢ HasFiniteIntegral fun a => ‖f a‖
have eq : (fun a => (nnnorm ‖f a‖ : ℝ≥0∞)) = fun a => (‖f a‖₊ : ℝ≥0∞) := by
  funext
  rw [nnnorm_norm]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.729415
δ : Type ?u.729418
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
eq : (fun a => ↑‖‖f a‖‖₊) = fun a => ↑‖f a‖₊
⊢ HasFiniteIntegral fun a => ‖f a‖
rwa [HasFiniteIntegral, eq]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.729415
δ : Type ?u.729418
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
x✝ : α
⊢ ↑‖‖f x✝‖‖₊ = ↑‖f x✝‖₊
α : Type u_1
β : Type u_2
γ : Type ?u.729415
δ : Type ?u.729418
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
⊢ (fun a => ↑‖‖f a‖‖₊) = fun a => ↑‖f a‖₊
funext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.729415
δ : Type ?u.729418
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
x✝ : α
⊢ ↑‖‖f x✝‖‖₊ = ↑‖f x✝‖₊
rw [nnnorm_norm]