mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
x✝ : Ω
⊢ x✝ ∈ (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ↔ x✝ ∈ (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
h_pos : 0 < logRatio c * a⁻¹ ^ 2
i : ℕ
⊢ 1 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
h_pos : 0 < logRatio c * a⁻¹ ^ 2
⊢ -2⁻¹ < 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
⊢ (∀ i ∈ s, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
hf

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
hf : ∀ i ∈ s, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: case fst
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : 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₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
x✝ : ↥I
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).1 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).1
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: case snd
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : 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₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
x✝ : ↥J
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).2 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).2
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: case fst
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : 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₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
x✝ : ↥I
⊢ (fun s ↦ (c • x) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (c • x) ⟨Sum.inr ↑t, ⋯⟩).1 x✝ =
    ((RingHom.id ℝ) c • (fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩)).1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: case snd
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : 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₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
x✝ : ↥J
⊢ (fun s ↦ (c • x) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (c • x) ⟨Sum.inr ↑t, ⋯⟩).2 x✝ =
    ((RingHom.id ℝ) c • (fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩)).2 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
x✝ : E
⊢ x✝ ∈ (fun x ↦ ‖x‖ ≤ b) ⁻¹' {True} ↔ x✝ ∈ {x | ‖x‖ ≤ b}

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: case hi
T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : Bot T
i : Fin #I
⊢ i.succ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: case inl
T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
j : Fin (#I + 1)
hij : 0 ≤ j
⊢ I.orderEmbOfFinWithBot 0 ≤ I.orderEmbOfFinWithBot j

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: case inl
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ 0
⊢ iIndepFun (fun i ω j ↦ X i j ω) κ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
i : S
⊢ ∀ (i_1 : T i), univ ∈ {s | MeasurableSet s}

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
x✝ : Ω
⊢ x✝ ∈ ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) ↔
    x✝ ∈ ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case neg.h₁
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot✝ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) ((μ Set.univ)⁻¹ • μ)
⊢ (μ Set.univ)⁻¹ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
⊢ t ∈ {t}

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
⊢ ∀ᵐ (ω : Ω) ∂P, B 0 ω = 0

Tactic:
have := hB.hasLaw_eval 0
  rw [gaussianReal_zero_var] at this
  exact this.ae_eq_of_dirac

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ s ∈ {s, t}

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ t ∈ {s, t}

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
x : ↥{s, t} → ℝ
⊢ t ∈ {s, t}

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case e'_2.e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
x✝ : Ω
⊢ B s x✝ = Function.eval ⟨s, ⋯⟩ ({s, t}.restrict fun x ↦ B x x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case e'_2.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
x✝ : Ω
⊢ B t x✝ = {s, t}.restrict (fun x ↦ B x x✝) ⟨t, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη✝ : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
this :
  ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
h' : ∀ i ∈ Finset.univ, MeasurableSet ((↑Finset.univ).pi fun j ↦ t ↑i ↑j)
ω : α
hω :
  (κ ω) (⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i, (κ ω) ((fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j)
hη : κ ω = η ω
x✝¹ : ↥I
x✝ : Ω
⊢ (x✝ ∈ (fun ω j ↦ X (↑x✝¹) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑x✝¹ ↑j) ↔
    x✝ ∈ (fun ω j ↦ X (↑x✝¹) j ω) ⁻¹' (↑(J ↑x✝¹)).pi (t ↑x✝¹)

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos
q : ℚ
h✝ : q < 0
⊢ 0 ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case neg
q : ℚ
h✝ : ¬q < 0
⊢ 1 ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
⊢ ∫ (x : WithLp 2 (↥I → ℝ)),
      id
        x ∂Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm)
        (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) =
    ∫ (x : WithLp 2 (↥I → ℝ)), id x ∂Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (projectiveFamily I)

Tactic:
rw [integral_map, integral_map, integral_map]
      · simp only [id_eq]
        rw [ContinuousLinearEquiv.integral_comp_id_comm,
          ContinuousLinearEquiv.integral_comp_comm]
        simp only [PiLp.continuousLinearEquiv_symm_apply, integral_id_projectiveFamily,
          WithLp.toLp_zero, WithLp.toLp_eq_zero]
        congr with i
        rw [eval_integral]
        · simpa using h2 _
        · exact fun _ ↦ (h1.hasGaussianLaw_eval _).integrable
      any_goals fun_prop
      exact aemeasurable_pi_lambda _ fun _ ↦ h1.aemeasurable _

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ∀ (x : { q' // ↑r < ↑q' }),
    f a ↑({ toFun := fun t ↦ ⟨↑t, ⋯⟩, invFun := fun t ↦ ⟨↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x) = f a ↑x

Tactic:
intro t
    simp only [Equiv.coe_fn_mk, Subtype.coe_mk]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
i : ι
⊢ cexp
      (↑((L ∘SL single ℝ E i) (∫ (x : E i), x ∂Measure.map (X i) P)) * I -
        ↑Var[⇑(L ∘SL single ℝ E i); Measure.map (X i) P] / 2) =
    cexp
      (↑(L (Pi.single i (∫ (x : E i), x ∂Measure.map (X i) P))) * I -
        ↑Var[⇑(L ∘SL single ℝ E i); Measure.map (X i) P] / 2)

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
h : i < j
h1 : i.succ ≤ j.succ
h2 : i.castSucc ≤ j.succ
h3 : i.castSucc ≤ j.castSucc
⊢ ↑(t i.succ) - ↑(t i.succ) - ↑(t i.castSucc) + ↑(t i.castSucc) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
⊢ X t = X t - X s + X s

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ 0 + ↑s = ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this : IsProbabilityMeasure P
x✝² : ι
x✝¹ : Ω
x✝ : κ x✝²
⊢ X x✝² x✝ x✝¹ = (ofLp ∘ toLp 2 ∘ fun ω j ↦ X x✝² j ω) x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
x✝¹ : Fin n
x✝ : Ω
⊢ (-B) (t x✝¹.succ) x✝ - (-B) (t x✝¹.castSucc) x✝ = ((fun x ↦ -x) ∘ fun ω ↦ B (t x✝¹.succ) ω - B (t x✝¹.castSucc) ω) x✝

Tactic:
simp

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
x✝¹ : Fin n
x✝ : Ω
⊢ -B (t x✝¹.succ) x✝ + B (t x✝¹.castSucc) x✝ = B (t x✝¹.castSucc) x✝ - B (t x✝¹.succ) x✝
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x✝ : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) x✝, 0 ≤ (preCDF ρ q (x✝, c).2).toReal

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
⊢ (ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ q + 1 ∈ Ioi q

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ⨅ r, f (a, t) ↑r ≤ 1

Tactic:
refine ciInf_le_of_le ?_ ?_ ?_
    · exact hbdd_below _
    · exact ⟨q + 1, by simp⟩
    · exact h_le_one _

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ ↑(t₀ + s) - ↑t₀ - (↑t₀ - ↑t₀) = ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ t₀ ≤ t₀ + t

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ t₀ ≤ t₀ + s

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

Tactic:
simp

Goal state after:
case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + t)) 2 P

Tactic:
simp

Goal state after:
case refine_2.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + t)) 2 P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

Tactic:
simp

Goal state after:
case refine_2.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + s)) 2 P

Tactic:
simp

Goal state after:
case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + s)) 2 P