-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
rw :
  (compLpL 2 μ (HAdd.hAdd (α := ℝ →L[ℝ] G) (toSpanSingleton ℝ x) (toSpanSingleton ℝ y)) :
        (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
rw₁ :
  (HAdd.hAdd (α := ↥(Lp ℝ 2 μ) →L[ℝ] ↥(Lp G 2 μ)) (compLpL 2 μ (toSpanSingleton ℝ x))
          (compLpL 2 μ (toSpanSingleton ℝ y)) :
        (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
rw₂ rw₃ :
  HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ))) =
    HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
⊢ (compLpL 2 μ (toSpanSingleton ℝ (x + y)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))

Tactic:
rw [toSpanSingleton_add, add_compLpL, add_apply]

Premises used: ContinuousLinearMap.add_apply, ContinuousLinearMap.toSpanSingleton_add, ContinuousLinearMap.add_compLpL