Theorem: SciLean.cintegral.arg_f.IsSmoothLinearMap_rule (SciLean/Core/Integral/CIntegral.lean)

State before:
α : Type ?u.99883
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.100557
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (y : β), IsSmoothLinearMap R fun x => f x y
⊢ IsSmoothLinearMap R fun x => ∫' y, f x y ∂μ
Tactic:
constructor <;> fun_prop
State after:
no goals