Theorem: SchwartzMap.Distribution.one_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
φ : 𝓢(E, F)
⊢ 1 φ = ∫ (x : E), φ x
Tactic:
change (One.one : 𝓢(E, F) →L[ℝ] F) φ = _
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
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ One.one φ = ∫ (x : E), φ 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
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ One.one φ = ∫ (x : E), φ x
Tactic:
simp [One.one]
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
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ integralCLM φ = ∫ (x : E), φ 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
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ integralCLM φ = ∫ (x : E), φ x
Tactic:
rw [integralCLM_apply]
State after:
no goals