Theorem: SchwartzMap.Distribution.const_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
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
c : 𝕜'
φ : 𝓢(E, F)
⊢ (const E F c) φ = c • ∫ (x : E), φ x
Tactic:
simp [const, one_apply]
State after:
no goals