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

State before:
α : Type ?u.96092
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.96766
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 : β), IsLinearMap R fun x => f x y
⊢ IsLinearMap R fun x => ∫' y, f x y ∂μ
Tactic:
have := hf
State after:
α : Type ?u.96092
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.96766
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 this : ∀ (y : β), IsLinearMap R fun x => f x y
⊢ IsLinearMap R fun x => ∫' y, f x y ∂μ

State before:
α : Type ?u.96092
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.96766
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 this : ∀ (y : β), IsLinearMap R fun x => f x y
⊢ IsLinearMap R fun x => ∫' y, f x y ∂μ
Tactic:
sorry_proof
State after:
no goals