-- 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) → ℝ)
⊢ cov[fun (ω : Ω) ↦
      inner.{0, u_4} ℝ (E := WithLp 2 ((j : κ i) → ℝ))
        (∑ i_1 : κ i,
          HSMul.hSMul (α := (fun (x : κ i) ↦ ℝ) i_1) (β := EuclideanSpace ℝ (κ i))
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun (κ i) ℝ) :
                  (a : EuclideanSpace ℝ (κ i)) → EuclideanSpace ℝ (κ i))
                x)
              i_1)
            ((EuclideanSpace.basisFun (κ i) ℝ : (a : κ i) → EuclideanSpace ℝ (κ i)) i_1 : EuclideanSpace ℝ (κ i)))
        ((toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω),
      fun (ω : Ω) ↦
      inner.{0, u_4} ℝ (E := WithLp 2 ((j : κ j) → ℝ))
        (∑ i : κ j,
          HSMul.hSMul (α := (fun (x : κ j) ↦ ℝ) i) (β := EuclideanSpace ℝ (κ j))
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun (κ j) ℝ) :
                  (a : EuclideanSpace ℝ (κ j)) → EuclideanSpace ℝ (κ j))
                y)
              i)
            ((EuclideanSpace.basisFun (κ j) ℝ : (a : κ j) → EuclideanSpace ℝ (κ j)) i : EuclideanSpace ℝ (κ j)))
        ((toLp 2 ∘ fun (ω : Ω) (j_1 : κ j) ↦ X j j_1 ω) ω);
      P] =
    0
have refine_2 : 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
Tactic: simp_rw [sum_inner, inner_smul_left]