-- 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₂
f g : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
pos :
  ∫ (x : E),
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) (((⇑f : (a : E) → F₁) + (⇑g : (a : E) → F₁)) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃)
        (φ x) ∂μ =
    HAdd.hAdd (α := F₃)
      (∫ (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₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₁ :
  ∫ (x : E),
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x + (g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃)
        (φ x) ∂μ =
    HAdd.hAdd (α := F₃)
      (∫ (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₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₂ :
  ∫ (x : E),
      (HAdd.hAdd (α := F₂ →L[𝕜] F₃) (β := F₂ →L[𝕜] F₃)
            ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃)
            ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) :
          (a : F₂) → F₃)
        (φ x) ∂μ =
    HAdd.hAdd (α := F₃)
      (∫ (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₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₃ :
  ∫ (x : E),
      HAdd.hAdd (α := F₃) (β := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ∂μ =
    HAdd.hAdd (α := F₃)
      (∫ (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₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
⊢ ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f + g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HAdd.hAdd (α := F₃)
      (∫ (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₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)

Tactic:
simp_rw [coe_add, Pi.add_apply, map_add, ContinuousLinearMap.add_apply,
        integral_add (f.integrable_bilin B hφ) (g.integrable_bilin B hφ)]

Premises used: ContDiffMapSupportedIn.coe_add, ContDiffMapSupportedIn.integrable_bilin, map_add, ContinuousLinearMap.add_apply, Pi.add_apply, MeasureTheory.integral_add