-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
pos :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • (⇑f : (a : E) → F₁)) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₁ :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) (c • (f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₂ :
  ∫ (x : E),
      (HSMul.hSMul (β := F₂ →L[𝕜] F₃) c ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) :
          (a : F₂) → F₃)
        (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₃ :
  ∫ (x : E),
      HSMul.hSMul (β := F₃) c
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₄ :
  HSMul.hSMul (β := F₃) c
      (∫ (a : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) a) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ a) ∂μ) =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
⊢ ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)

Tactic:
simp_rw [coe_smul, Pi.smul_apply, map_smul, ContinuousLinearMap.smul_apply,
        integral_smul c, RingHom.id_apply]

Premises used: ContinuousLinearMap.smul_apply, RingHom.id_apply, ContDiffMapSupportedIn.coe_smul, MeasureTheory.integral_smul, map_smul, Pi.smul_apply