-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
have :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
refine_2 :
  ∀
    (h1 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
        (∑ i : ↥I,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S))),
    cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
        Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
      0
have₁ :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
refine_2₁ refine_2₂ :
  ∀
    (h1 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
        (∑ i : ↥I,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S))),
    cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
        Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
      0
refine_2₃ :
  ∀
    (h1 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
        (∑ i : ↥I,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S)))
    (h2 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
        (∑ j : ↥J,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T))),
    cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
        Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
      0
refine_2₄ :
  ∀
    (h1 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
        (∑ i : ↥I,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S)))
    (h2 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
        (∑ j : ↥J,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T))),
    Eq (α := ℝ)
      (∑ i : ↥I,
        ∑ j : ↥J,
          cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                    (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
                (a : E) → ℝ) ∘
              X (↑i : S),
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                    (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
                (a : E) → ℝ) ∘
              Y (↑j : T);
            P])
      0
refine_2₅ :
  ∀
    (h1 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
        (∑ i : ↥I,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S)))
    (h2 :
      Eq.{u_2 + 1} (α := Ω → ℝ)
        (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
        (∑ j : ↥J,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T)))
    (i : ↥I),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
      2 P
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have refine_2₆ : ∀
  (h1 :
    Eq.{u_2 + 1} (α := Ω → ℝ)
      (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (∑ i : ↥I,
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
            (a : E) → ℝ) ∘
          X (↑i : S)))
  (h2 :
    Eq.{u_2 + 1} (α := Ω → ℝ)
      (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
      (∑ j : ↥J,
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
            (a : E) → ℝ) ∘
          Y (↑j : T)))
  (i : ↥J),
  MemLp (ε := ℝ)
    ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
            (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) i)) :
        (a : E) → ℝ) ∘
      Y (↑i : T))
    2 P
Tactic: classical
  have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..
  · exact fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two
  · exact fun t ↦ ((hXY.hasGaussianLaw_eval (.inr t)).map _).memLp_two