mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I✝ J I : Finset ℝ≥0
⊢ IsGaussian (Measure.map (⇑(EuclideanSpace.equiv ↥I ℝ)) (multivariateGaussian 0 (covMatrix I)))

Tactic:
infer_instance

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁶ : Preorder T
inst✝⁵ : MeasurableSpace E
F : Type u_4
G : Type u_5
inst✝⁴ : MeasurableSpace G
inst✝³ : FunLike F E G
inst✝² : AddGroup E
inst✝¹ : SubtractionMonoid G
inst✝ : AddMonoidHomClass F E G
f : F
hf : Measurable ⇑f
hX : HasIndepIncrements X P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
⊢ iIndepFun (fun i ω ↦ f (X (t i.succ) ω - X (t i.castSucc) ω)) P

Tactic:
exact (hX n t ht).comp (fun _ ↦ f) (fun _ ↦ hf)

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ charFun (Measure.map Prod.fst (μ.prod ν)) * charFun (Measure.map Prod.snd (μ.prod ν)) = charFun μ * charFun ν

pp: case mX
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

pp: case mY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

pp: case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
measurePreserving_fst.map_eq,

Goal state after:
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ charFun μ * charFun (Measure.map Prod.snd (μ.prod ν)) = charFun μ * charFun ν

case mX
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

case mY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case mX
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

pp: case mY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

pp: case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
any_goals fun_prop

Goal state after:
case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ charFunDual (Measure.map Prod.fst (μ.prod ν)) * charFunDual (Measure.map Prod.snd (μ.prod ν)) =
    charFunDual μ * charFunDual ν

pp: case mX
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

pp: case mY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

pp: case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
measurePreserving_fst.map_eq,

Goal state after:
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ charFunDual μ * charFunDual (Measure.map Prod.snd (μ.prod ν)) = charFunDual μ * charFunDual ν

case mX
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

case mY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case mX
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

pp: case mY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

pp: case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
any_goals fun_prop

Goal state after:
case hXY
E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
⊢ (fun i ↦ (m • x) ⟨t i.succ, ⋯⟩ - (m • x) ⟨t i.castSucc, ⋯⟩) =
    (RingHom.id ℝ) m • fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩

Tactic:
by ext; simp; module

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ charFun (Measure.map (fun p ↦ ∑ i, p i) (Measure.pi μ)) = ∏ i, charFun (μ i)

Tactic:
ext
  simp [charFun_eq_charFunDual_toDualMap, charFunDual_map_sum_pi_eq_prod]

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 : 1 < μ {x | ‖x‖ ≤ a} * 2
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 < ∞
⊢ 1 < 2 * c

Tactic:
mul_comm

Goal state after:
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 : 1 < 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 < ∞
⊢ 1 < 2 * c
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
⊢ MeasurableSet {x | ‖x‖ ≤ b}

Tactic:
exact measurableSet_le (by fun_prop) (by fun_prop)

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

Goal state before:
pp: case refine_2
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
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
h2 : (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) = ∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j
⊢ ∑ i,
      ∑ j,
        cov[⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i,
          ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j; P] =
    0

Tactic:
exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..

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

Goal state before:
pp: case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atTop (𝓝 1)

pp: case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atTop (𝓝 1)

Tactic:
exacts [(hf h).tendsto_atTop_one, (hg h).tendsto_atTop_one]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
x y z : StrongDual ℝ (E × F)
⊢ (L₁ ((x + y) ∘SL inl ℝ E F)) (z ∘SL inl ℝ E F) + (L₂ ((x + y) ∘SL inr ℝ E F)) (z ∘SL inr ℝ E F) =
    (L₁ (x ∘SL inl ℝ E F)) (z ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (z ∘SL inr ℝ E F) +
      ((L₁ (y ∘SL inl ℝ E F)) (z ∘SL inl ℝ E F) + (L₂ (y ∘SL inr ℝ E F)) (z ∘SL inr ℝ E F))

Tactic:
simp [add_add_add_comm]

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

Goal state before:
pp: case hm.hφ
Ω : 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)
⊢ AEMeasurable (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (projectiveFamily I)

pp: case hm.hfm
Ω : 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)
⊢ AEStronglyMeasurable id (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (projectiveFamily I))

pp: case hm.hφ
Ω : 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)
⊢ AEMeasurable (fun ω ↦ I.restrict fun x ↦ X x ω) P

pp: case hm.hfm
Ω : 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)
⊢ AEStronglyMeasurable (fun x ↦ id ((PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm x))
    (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)

pp: case hm.hφ
Ω : 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)
⊢ AEMeasurable (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)

pp: case hm.hfm
Ω : 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)
⊢ AEStronglyMeasurable id
    (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P))

Tactic:
any_goals fun_prop

Goal state after:
case hm.hφ
Ω : 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)
⊢ AEMeasurable (fun ω ↦ I.restrict fun x ↦ X x ω) P
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
x y z : StrongDual ℝ (E × F)
⊢ (L₁ (x ∘SL inl ℝ E F)) ((y + z) ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) ((y + z) ∘SL inr ℝ E F) =
    (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F) +
      ((L₁ (x ∘SL inl ℝ E F)) (z ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (z ∘SL inr ℝ E F))

Tactic:
simp [add_add_add_comm]

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

Goal state before:
pp: case neg.hfin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ ∃ i, (κ a) (s ×ˢ Iic ↑↑i) ≠ ∞

Tactic:
exact ⟨h_nonempty.some, measure_ne_top _ _⟩

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1

Tactic:
refine fun r ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF fun s hs _ ↦ ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ∞
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a ↦ ENNReal.ofReal (↑(condCDF ρ a) ↑r)) =ᵐ[ρ.fst] preCDF ρ r

Tactic:
filter_upwards [condCDF_ae_eq ρ r, preCDF_le_one ρ] with a ha ha_le_one

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
a : α
ha : ↑(condCDF ρ a) ↑r = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ ENNReal.ofReal (↑(condCDF ρ a) ↑r) = preCDF ρ r a
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 : α
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (fun n ↦ f (a, t) (-↑n)) atTop (𝓝 0)

Tactic:
exact hf.tendsto_zero_of_antitone _ _ Nat.mono_cast.neg
    (tendsto_neg_atBot_iff.mpr tendsto_natCast_atTop_atTop)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ (condCDF ρ a).measure (Iic x) = ENNReal.ofReal (↑(condCDF ρ a) x)

Tactic:
rw [← sub_zero (condCDF ρ a x)]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ (condCDF ρ a).measure (Iic x) = ENNReal.ofReal (↑(condCDF ρ a) x - 0)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case mX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0), AEMeasurable (fun ω ↦ B (t₀ + s) ω - B t₀ ω) P

pp: case mY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (t : ↑(Set.Iic t₀)), AEMeasurable (B ↑t) P

pp: case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0) (t : ↑(Set.Iic t₀)), cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑t; P] = 0

Tactic:
any_goals fun_prop

Goal state after:
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0) (t : ↑(Set.Iic t₀)), cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑t; P] = 0
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
IsCondKernelCDF.toKernel_Iic

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)