-- 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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
refine_1 :
  ∀ (I : Finset T) (J : (i : ↥I) → Finset (S (↑i : T))),
    HasGaussianLaw (E := (i : ↥I) → (j : ↥(J i)) → E)
      (fun (ω : Ω) (i : ↥I) (j : ↥(J i)) ↦ X (↑i : T) (↑j : S (↑i : T)) ω) P
refine_2 refine_2₁ :
  ∀ (I : Finset T) (J : (i : ↥I) → Finset (S (↑i : T))) (i j : ↥I) (hij : i ≠ j) (L₁ : StrongDual ℝ ((j : ↥(J i)) → E))
    (L₂ : StrongDual ℝ ((j : ↥(J j)) → E)),
    cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
          X (↑i : T) (↑j : S (↑i : T)) ω,
        Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
          X (↑j : T) (↑j_1 : S (↑j : T)) ω;
        P] =
      0
⊢ iIndepFun (β := fun (t : T) ↦ (s : S t) → E) (fun (t : T) (ω : Ω) (s : S t) ↦ X t s ω) P
have refine_2₂ : ∀ (I : Finset T) (J : (i : ↥I) → Finset (S (↑i : T))) (i j : ↥I) (hij : i ≠ j) (L₁ : StrongDual ℝ ((j : ↥(J i)) → E))
  (L₂ : StrongDual ℝ ((j : ↥(J j)) → E))
  (h1 :
    Eq.{u_2 + 1} (α := Ω → ℝ)
      (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
        X (↑i : T) (↑k : S (↑i : T)) ω)
      (∑ k : ↥(J i),
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
            (a : E) → ℝ) ∘
          X (↑i : T) (↑k : S (↑i : T)))),
  cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
        X (↑i : T) (↑j : S (↑i : T)) ω,
      Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
        X (↑j : T) (↑j_1 : S (↑j : T)) ω;
      P] =
    0
Tactic: classical
  refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij L₁ L₂ ↦ ?_
  · let L : (I.sigma (fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E) →L[ℝ] (i : I) → J i → E :=
      { toFun x i j := x ⟨⟨i, j⟩, by simp⟩
        map_add' x y := by ext; simp
        map_smul' c x := by ext; simp }
    exact (hX.hasGaussianLaw _).map L
  have h1 : L₁ ∘ (fun ω k ↦ X i k ω) = ∑ k : J i, (L₁ ∘L .single ℝ _ k) ∘ X i k := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω k ↦ X j k ω) = ∑ k : J j, (L₂ ∘L .single ℝ _ k) ∘ X j k := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun _ _ ↦ sum_eq_zero fun _ _ ↦ h i j (by simpa) ..
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨j, k⟩).map _).memLp_two