-- 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 ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this : IsProbabilityMeasure P
let let₁ let₂ : iIndepFun (β := E) X P
let₃ let₄ :
  let this := Fintype.ofFinite ι;
  ∀ (L : StrongDual ℝ ((x : ι) → E x)),
    charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
      ∏ i : ι,
        charFunDual.{u_3} (E := E i) (mE := inst_2 i) (Measure.map (fun (x : Ω) ↦ X i x) P)
          (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i))
let₅ :
  let this := Fintype.ofFinite ι;
  ∀ (L : StrongDual ℝ ((x : ι) → E x))
    (this_1 :
      ∀ (ω : Ω),
        Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
          (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)),
    charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
      ∏ i : ι,
        charFunDual.{u_3} (E := E i) (mE := inst_2 i) (Measure.map (fun (x : Ω) ↦ X i x) P)
          (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i))
let₆ :
  let this := Fintype.ofFinite ι;
  ∀ (L : StrongDual ℝ ((x : ι) → E x))
    (this_1 :
      ∀ (ω : Ω),
        Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
          (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)),
    cexp
        ((↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) * I -
          (↑Var[fun (ω : Ω) ↦ ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P] : ℂ) /
            2) =
      cexp
        ((∑ i : ι, (↑(∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)) * I -
          ∑ x : ι,
            (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2)
e_z :
  let this := Fintype.ofFinite ι;
  ∀ (L : StrongDual ℝ ((x : ι) → E x))
    (this_1 :
      ∀ (ω : Ω),
        Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
          (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)),
    (↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) =
      ∑ i : ι, (↑(∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)
⊢ iIndepFun (β := E) X P
have e_z₁ : let this := Fintype.ofFinite ι;
∀ (L : StrongDual ℝ ((x : ι) → E x))
  (this_1 :
    ∀ (ω : Ω),
      Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
        (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)),
  (↑Var[fun (ω : Ω) ↦ ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P] : ℂ) / 2 =
    ∑ x : ι, (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2
Tactic: classical
  let := Fintype.ofFinite ι
  rw [iIndepFun_iff_charFunDual_pi fun i ↦ hX.aemeasurable.eval i]
  intro L
  have this ω : L (X · ω) = ∑ i, (L ∘L (single ℝ E i)) (X i ω) := by
    simp [← map_sum, LinearMap.sum_single_apply]
  simp_rw [hX.charFunDual_map_eq_fun, fun i ↦ (hX.eval i).charFunDual_map_eq_fun, ← Complex.exp_sum,
    sum_sub_distrib, ← sum_mul, this]
  congr
  · simp_rw [← Complex.ofReal_sum]
    rw [integral_finsetSum _ fun i _ ↦ ((hX.eval i).map_fun _).integrable.ofReal]
  · rw [variance_fun_sum fun i ↦ ((hX.eval i).map_fun _).memLp_two]
    simp only [← sum_div, ← ofReal_sum, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      div_left_inj', ofReal_inj]
    congr with i
    rw [sum_eq_single_of_mem i (by grind) (fun j _ hij ↦ h i j hij.symm _ _),
      covariance_self ((hX.eval i).map_fun _).aemeasurable]