awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
fst :
  ∀ (x_1 : ↥I),
    (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).1
        x_1 =
      (HAdd.hAdd (α := (↥I → E) × (↥J → E))
            (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
            (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).1
        x_1
snd :
  ∀ (x_1 : ↥J),
    (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).2
        x_1 =
      (HAdd.hAdd (α := (↥I → E) × (↥J → E))
            (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
            (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).2
        x_1
⊢ (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
      (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)) =
    HAdd.hAdd (α := (↥I → E) × (↥J → E))
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
      (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
x_1 : ↥I
⊢ (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
          (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).1
      x_1 =
    (HAdd.hAdd (α := (↥I → E) × (↥J → E))
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
          (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).1
      x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
x_1 : ↥J
⊢ (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
          (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).2
      x_1 =
    (HAdd.hAdd (α := (↥I → E) × (↥J → E))
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
          (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).2
      x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
fst :
  ∀ (x_1 : ↥I),
    (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).1
        x_1 =
      (HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
            (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).1
        x_1
snd :
  ∀ (x_1 : ↥J),
    (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).2
        x_1 =
      (HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
            (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).2
        x_1
⊢ (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
      (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
x_1 : ↥I
⊢ (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
          (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).1
      x_1 =
    (HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).1
      x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
x_1 : ↥J
⊢ (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
          (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).2
      x_1 =
    (HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).2
      x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L : (↥(I.disjSum J) → E) →L[ℝ] (↥I → E) × (↥J → E) :=
  {
    toFun := fun (x : ↥(I.disjSum J) → E) ↦
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw (E := ((i : ↥I) → E) × ((j : ↥J) → E))
    (fun (ω : Ω) ↦ (fun (i : ↥I) ↦ X (↑i : S) ω, fun (j : ↥J) ↦ Y (↑j : T) ω)) P

Tactic:
(hXY.hasGaussianLaw _).map L

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, setOf, Finset.restrict, ProbabilityTheory.HasGaussianLaw.map, Sum.elim
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L : (↥(I.disjSum J) → E) →L[ℝ] (↥I → E) × (↥J → E) :=
  {
    toFun := fun (x : ↥(I.disjSum J) → E) ↦
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw (E := ((i : ↥I) → E) × ((j : ↥J) → E))
    (fun (ω : Ω) ↦ (fun (i : ↥I) ↦ X (↑i : S) ω, fun (j : ↥J) ↦ Y (↑j : T) ω)) P

Tactic:
exact (hXY.hasGaussianLaw _).map L

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h₁ :
  ∀ (x : Ω),
    Eq (α := ℝ)
      (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) x)
      ((∑ i : ↥I,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S))
        x)
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
x : Ω
⊢ Eq (α := ℝ) (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) x)
    ((∑ i : ↥I,
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
            (a : E) → ℝ) ∘
          X (↑i : S))
      x)

Tactic:
simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]

Premises used: ContinuousLinearMap.sum_comp_single, ContinuousLinearMap.coe_comp'
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))

Tactic:
have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h₁ :
  ∀ (x : Ω),
    Eq (α := ℝ)
      (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) x)
      ((∑ j : ↥J,
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T))
        x)
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
x : Ω
⊢ Eq (α := ℝ) (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) x)
    ((∑ j : ↥J,
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
            (a : E) → ℝ) ∘
          Y (↑j : T))
      x)

Tactic:
simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]

Premises used: ContinuousLinearMap.sum_comp_single, ContinuousLinearMap.coe_comp'
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))

Tactic:
have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]