Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case h_ind
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      μ s < ∞ → ∫ (x : X), L (s.indicator (fun x ↦ c) x) ∂μ = L (∫ (x : X), s.indicator (fun x ↦ c) x ∂μ)

pp: case h_add
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ ∀ ⦃f g : X → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ) →
            ∫ (x : X), L (g x) ∂μ = L (∫ (x : X), g x ∂μ) → ∫ (x : X), L ((f + g) x) ∂μ = L (∫ (x : X), (f + g) x ∂μ)

pp: case h_closed
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ IsClosed {f | ∫ (x : X), L (↑↑f x) ∂μ = L (∫ (x : X), ↑↑f x ∂μ)}

pp: case h_ae
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ ∀ ⦃f g : X → E⦄,
    f =ᵐ[μ] g →
      Integrable f μ → ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ) → ∫ (x : X), L (g x) ∂μ = L (∫ (x : X), g x ∂μ)

Tactic:
· intro e s s_meas _
    rw [integral_indicator_const e s_meas, ← @smul_one_smul E ℝ 𝕜 _ _ _ _ _ (μ.real s) e,
      map_smulₛₗ, hσ, map_one, smul_assoc, one_smul,
      ← integral_indicator_const (L e) s_meas]
    congr 1 with a
    rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply]

Goal state after:
case h_add
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ ∀ ⦃f g : X → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ) →
            ∫ (x : X), L (g x) ∂μ = L (∫ (x : X), g x ∂μ) → ∫ (x : X), L ((f + g) x) ∂μ = L (∫ (x : X), (f + g) x ∂μ)

case h_closed
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ IsClosed {f | ∫ (x : X), L (↑↑f x) ∂μ = L (∫ (x : X), ↑↑f x ∂μ)}

case h_ae
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ ∀ ⦃f g : X → E⦄,
    f =ᵐ[μ] g →
      Integrable f μ → ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ) → ∫ (x : X), L (g x) ∂μ = L (∫ (x : X), g x ∂μ)