Theorem: SchwartzMap.integralCLM_apply (ForML/SchwartzLp.lean)

State before:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ integralCLM f = ∫ (x : E), f x
Tactic:
rw [integralCLM]
State after:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' ℝ) f = ∫ (x : E), f x

State before:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' ℝ) f = ∫ (x : E), f x
Tactic:
exact integralCLM'_apply
State after:
no goals