awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
⊢ Eq (α := Ω → E) (∑ i ∈ I, X i) (∑ i : ↥I, fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) (fun (x : T) ↦ X x ω) i)

Tactic:
simp [I.sum_attach X]

Premises used: Finset.sum_attach
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (∑ i ∈ I, X i) P

Tactic:
hX.hasGaussianLaw_sum (I := I)

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sum
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
h : ∀ (x : Ω), Eq.{u_4 + 1} (α := E) (∑ i ∈ I, X i x) ((∑ i ∈ I, X i) x)
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (fun (ω : Ω) ↦ ∑ i ∈ I, X i ω) P

Tactic:
convert! hX.hasGaussianLaw_sum (I := I)

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sum
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
x : Ω
⊢ Eq.{u_4 + 1} (α := E) (∑ i ∈ I, X i x) ((∑ i ∈ I, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x : ↥(image t univ) → E
i : Fin n
⊢ t i.succ ∈ image t univ

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x : ↥(image t univ) → E
i : Fin n
⊢ t i.castSucc ∈ image t univ

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
h :
  ∀ (x_1 : Fin n),
    (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
      HAdd.hAdd (α := Fin n → E) (β := Fin n → E)
        (fun (i : Fin n) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
            x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
        (fun (i : Fin n) ↦
          y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
            y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
        x_1
⊢ (fun (i : Fin n) ↦
      (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)) =
    HAdd.hAdd (α := Fin n → E)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      fun (i : Fin n) ↦
      y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x_1 : Fin n
h :
  x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) +
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      (x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) +
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯)) =
    x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) +
      (y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯))
⊢ (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
    HAdd.hAdd (α := Fin n → E) (β := Fin n → E)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      (fun (i : Fin n) ↦
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x_1 : Fin n
⊢ x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) +
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      (x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) +
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯)) =
    x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) +
      (y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯))

Tactic:
abel
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
h :
  ∀ (x_1 : Fin n),
    (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
      HSMul.hSMul (α := ℝ) (β := Fin n → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ)
        (fun (i : Fin n) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
            x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
        x_1
⊢ (fun (i : Fin n) ↦
      (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := Fin n → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) fun (i : Fin n) ↦
      x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x_1 : Fin n
h :
  m • x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      m • x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
    m •
      (x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯))
⊢ (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
    HSMul.hSMul (α := ℝ) (β := Fin n → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x_1 : Fin n
⊢ m • x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      m • x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
    m •
      (x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯))

Tactic:
module
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
L : (↥(image t univ) → E) →L[ℝ] Fin n → E :=
  {
    toFun := fun (x : ↥(image t univ) → E) (i : Fin n) ↦
      x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw.{u_3, u_4} (E := (i : Fin n) → E) (fun (ω : Ω) (i : Fin n) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P

Tactic:
(hX.hasGaussianLaw _).map L

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, Finset.restrict, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
L : (↥(image t univ) → E) →L[ℝ] Fin n → E :=
  {
    toFun := fun (x : ↥(image t univ) → E) (i : Fin n) ↦
      x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw.{u_3, u_4} (E := (i : Fin n) → E) (fun (ω : Ω) (i : Fin n) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P

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

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
let let₁ let₂ :
  HasGaussianLaw.{u_3, u_4} (E := (i : Fin n) → E) (fun (ω : Ω) (i : Fin n) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P
⊢ HasGaussianLaw.{u_3, u_4} (E := (i : Fin n) → E) (fun (ω : Ω) (i : Fin n) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P

Tactic:
classical
  let L : ((univ.image t) → E) →L[ℝ] Fin n → E :=
    { toFun x i := x ⟨t i.succ, by simp⟩ - x ⟨t i.castSucc, by simp⟩
      map_add' x y := by ext; simp; abel
      map_smul' m x := by ext; simp; module }
  exact (hX.hasGaussianLaw _).map L
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
h :
  ∀ (s : S),
    ∃ (I : Finset T) (L : (↥I → E) →L[ℝ] F),
      ∀ (ω : Ω), Y s ω = (L : (a : ↥I → E) → F) (I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥I) → E)
I : Finset S
choose :
  ∀ (J : (s : S) → Finset T) (L : (s : S) → (↥(J s) → E) →L[ℝ] F)
    (hL :
      ∀ (s : S) (ω : Ω),
        Y s ω =
          (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)),
    HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
⊢ HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P

Tactic:
choose J L hL using h
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
x y : ↥(I.biUnion J) → E
h :
  ∀ (x_1 : ↥I),
    ((L (↑x_1 : S) : (a : ↥(J (↑x_1 : S)) → E) → F) fun (t : ↥(J (↑x_1 : S))) ↦
        (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
      HAdd.hAdd (α := ↥I → F) (β := ↥I → F)
        (fun (s : ↥I) ↦
          (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
            x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
        (fun (s : ↥I) ↦
          (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
            y (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
        x_1
⊢ (fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
    HAdd.hAdd (α := ↥I → F)
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
      fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
x y : ↥(I.biUnion J) → E
x_1 : ↥I
⊢ ((L (↑x_1 : S) : (a : ↥(J (↑x_1 : S)) → E) → F) fun (t : ↥(J (↑x_1 : S))) ↦
      (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
    HAdd.hAdd (α := ↥I → F) (β := ↥I → F)
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          y (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
      x_1

Tactic:
simp [← Pi.add_def]

Premises used: Pi.add_def
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
c : ℝ
x : ↥(I.biUnion J) → E
h :
  ∀ (x_1 : ↥I),
    ((L (↑x_1 : S) : (a : ↥(J (↑x_1 : S)) → E) → F) fun (t : ↥(J (↑x_1 : S))) ↦
        (c • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
      HSMul.hSMul (α := ℝ) (β := ↥I → F) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
        (fun (s : ↥I) ↦
          (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
            x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
        x_1
⊢ (fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        (c • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := ↥I → F) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ) fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
c : ℝ
x : ↥(I.biUnion J) → E
x_1 : ↥I
⊢ ((L (↑x_1 : S) : (a : ↥(J (↑x_1 : S)) → E) → F) fun (t : ↥(J (↑x_1 : S))) ↦
      (c • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := ↥I → F) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
      x_1

Tactic:
simp [← Pi.smul_def]

Premises used: Pi.smul_def
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  {
    toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
h :
  ∀ (x : Ω) (x_1 : ↥I),
    Eq.{u_6 + 1} (α := F) (I.restrict (π := fun (x : S) ↦ F) (fun (x_2 : S) ↦ Y x_2 x) x_1 : F)
      (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F)
          (fun (ω : Ω) ↦ (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) x x_1 :
        F)
⊢ Eq (α := (ω : Ω) → (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω)
    (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
      (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  {
    toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
x : Ω
x_1 : ↥I
⊢ Eq.{u_6 + 1} (α := F) (I.restrict (π := fun (x : S) ↦ F) (fun (x_2 : S) ↦ Y x_2 x) x_1 : F)
    (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F)
        (fun (ω : Ω) ↦ (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) x x_1 :
      F)

Tactic:
simp [K, hL, Finset.restrict_def]

Premises used: Finset.restrict_def