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