-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
refine_2 :
  Eq (α := ℝ)
    (∑ i : ι,
      ∑ j : κ,
        cov[fun (ω : Ω) ↦
          HMul.hMul (α := ℝ)
            ((starRingEnd ℝ : (a : ℝ) → ℝ)
                (ofLp (p := 2)
                  ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
                    x)
                  i) :
              ℝ)
            (inner ℝ (E := WithLp 2 ((i : ι) → ℝ))
              ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι)
              ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω : WithLp 2 ((i : ι) → ℝ))),
          fun (ω : Ω) ↦
          HMul.hMul (α := ℝ)
            ((starRingEnd ℝ : (a : ℝ) → ℝ)
                (ofLp (p := 2)
                  ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ)
                    y)
                  j) :
              ℝ)
            (inner ℝ (E := WithLp 2 ((j : κ) → ℝ))
              ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) j : EuclideanSpace ℝ κ)
              ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω : WithLp 2 ((j : κ) → ℝ)));
          P])
    0
refine_2₁ :
  ∀ (i : ι),
    MemLp (ε := ℝ)
      (fun (ω : Ω) ↦
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
                  x)
                i) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((i : ι) → ℝ))
            ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι)
            ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω : WithLp 2 ((i : ι) → ℝ))))
      2 P
⊢ cov[fun (ω : Ω) ↦
      ∑ x_1 : ι,
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
                  x)
                x_1) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((i : ι) → ℝ))
            ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) x_1 : EuclideanSpace ℝ ι)
            ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω : WithLp 2 ((i : ι) → ℝ))),
      fun (ω : Ω) ↦
      ∑ x : κ,
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ)
                  y)
                x) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((j : κ) → ℝ))
            ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) x : EuclideanSpace ℝ κ)
            ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω : WithLp 2 ((j : κ) → ℝ)));
      P] =
    0
have refine_2₂ : ∀ (i : κ),
  MemLp (ε := ℝ)
    (fun (ω : Ω) ↦
      HMul.hMul (α := ℝ)
        ((starRingEnd ℝ : (a : ℝ) → ℝ)
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ) y)
              i) :
          ℝ)
        (inner ℝ (E := WithLp 2 ((j : κ) → ℝ))
          ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) i : EuclideanSpace ℝ κ)
          ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω : WithLp 2 ((j : κ) → ℝ))))
    2 P
Tactic: rw [covariance_fun_sum_fun_sum]