mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case e'_3.e'_2
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ v * (NNReal.mk (c ^ 2) ⋯)⁻¹ = NNReal.mk (c⁻¹ ^ 2) ⋯ * v

Tactic:
rw [mul_comm]

Goal state after:
case e'_3.e'_2
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ (NNReal.mk (c ^ 2) ⋯)⁻¹ * v = NNReal.mk (c⁻¹ ^ 2) ⋯ * v
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ |X ω| ^ p * rexp (v * X ω)) μ

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv
  obtain ⟨l, u, hvlu, h_subset⟩ := hv
  have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
  refine integrable_rpow_abs_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
  · positivity
  · exact h_subset (add_half_inf_sub_mem_Ioo hvlu)
  · exact h_subset (sub_half_inf_sub_mem_Ioo hvlu)

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ ((covarianceBilin (Measure.map (fun x ↦ c + x) μ)) x✝¹) x✝ = ((covarianceBilin μ) x✝¹) x✝

Tactic:
covarianceBilin_of_not_memLp,

Goal state after:
case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ (0 x✝¹) x✝ = ((covarianceBilin μ) x✝¹) x✝

case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ ¬MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
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✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ MeasurableSet {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}

Tactic:
refine MeasurableSet.inter ?_ ?_
      · change MeasurableSet {p : E × E | ‖p.1‖ ≤ a}
        exact measurableSet_le (by fun_prop) (by fun_prop)
      · change MeasurableSet {p : E × E | b < ‖p.2‖}
        exact measurableSet_lt (by fun_prop) (by fun_prop)

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

Goal state before:
pp: case e_6.e'_1
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖(√2 / 2) • (p.1 - p.2)‖ = ‖p.1 - p.2‖ / √2

Tactic:
norm_smul,

Goal state after:
case e_6.e'_1
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖√2 / 2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case e_6.e'_2
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖(√2 / 2) • (p.1 + p.2)‖ = ‖p.1 + p.2‖ / √2

Tactic:
norm_smul,

Goal state after:
case e_6.e'_2
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖√2 / 2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

Tactic:
by_cases h : MemLp id 2 μ
  swap; · simp only [uncenteredCovarianceBilinDual_of_not_memLp h, norm_zero]; positivity
  calc ‖uncenteredCovarianceBilinDual μ L₁ L₂‖
  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
  _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
  _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
    refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
    · simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm
    · simp_rw [mul_assoc]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
      refine Integrable.const_mul ?_ _
      exact h.integrable_norm_pow (by simp)
    · simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x
  _ = ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
    rw [← integral_const_mul]
    congr with x
    ring

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ charFun (Measure.map (⇑L) μ) t = charFun (gaussianReal (L m) ((f L) L).toNNReal) t

Tactic:
charFun_map_eq_charFunDual_smul,

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ charFunDual μ (t • L) = charFun (gaussianReal (L m) ((f L) L).toNNReal) t
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ
⊢ Set.Ioo (-C) C ⊆ integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ

Tactic:
exact fun x hx ↦ integrable_exp_mul_of_le_of_le hC_neg hC hx.1.le hx.2.le

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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ ENNReal.ofReal (rexp (C * a ^ 2)) * μ (closedBall 0 a) = μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
rw [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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ μ (closedBall 0 a) * ENNReal.ofReal (rexp (C * a ^ 2)) = μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ ∫ (x : ↥I → ℝ), x s ∂projectiveFamily I = 0

Tactic:
by
  conv => enter [1, 2]; change fun x ↦ ContinuousLinearMap.proj (R := ℝ) s x
  rw [ContinuousLinearMap.integral_comp_id_comm, integral_id_projectiveFamily, map_zero]
  exact IsGaussian.integrable_id

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

Goal state before:
pp: case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑t + ↑s - 2 * min ↑s ↑t = ↑t + ↑s - 2 * min ↑t ↑s

Tactic:
min_comm

Goal state after:
case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑t + ↑s - 2 * min ↑t ↑s = ↑t + ↑s - 2 * min ↑t ↑s
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha✝ : 0 ≤ a
ha : a = 0
⊢ 1 ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-(2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n)))

Tactic:
refine le_add_right ?_

Goal state after:
case inl
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha✝ : 0 ≤ a
ha : a = 0
⊢ 1 ≤ ENNReal.ofReal (rexp (logRatio c))
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: case h1.refine_1
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), AEMeasurable (X i) (⇑κ ∘ₘ P)
hY : AEMeasurable Y (⇑κ ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
I : Finset S
⊢ IndepFun (fun ω i ↦ X (↑i) ω) (AEMeasurable.mk Y hY) κ P

Tactic:
exact (h I).congr' (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk)

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

Goal state before:
pp: α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Monotone (if p a then f a else g a)

Tactic:
split_ifs with h; exacts [(hf h).mono, (hg h).mono]

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

Goal state before:
pp: case hv.inr
Ω : 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 → ℝ)
i j : ↥I
this :
  ∀ (i j : ↥I),
    ↑i ≤ ↑j →
      cov[(fun ω ↦ ω i) ∘ fun ω ↦ I.restrict fun x ↦ X x ω, (fun ω ↦ ω j) ∘ fun ω ↦ I.restrict fun x ↦ X x ω; P] =
        ↑(min ↑i ↑j)
hij : ¬↑i ≤ ↑j
⊢ ↑(min ↑j ↑i) = ↑(min ↑i ↑j)

Tactic:
min_comm

Goal state after:
case hv.inr
Ω : 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 → ℝ)
i j : ↥I
this :
  ∀ (i j : ↥I),
    ↑i ≤ ↑j →
      cov[(fun ω ↦ ω i) ∘ fun ω ↦ I.restrict fun x ↦ X x ω, (fun ω ↦ ω j) ∘ fun ω ↦ I.restrict fun x ↦ X x ω; P] =
        ↑(min ↑i ↑j)
hij : ¬↑i ≤ ↑j
⊢ ↑(min ↑i ↑j) = ↑(min ↑i ↑j)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case inr
Ω : 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
this :
  ∀ (i j : Fin n),
    i ≠ j →
      i < j →
        ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
            ↑(min (t i.castSucc) (t j.castSucc)) =
          0
h : ¬i < j
⊢ ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc)) =
    ↑(min (t j.succ) (t i.succ)) - ↑(min (t j.succ) (t i.castSucc)) - ↑(min (t j.castSucc) (t i.succ)) +
      ↑(min (t j.castSucc) (t i.castSucc))

Tactic:
min_comm

Goal state after:
case inr
Ω : 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
this :
  ∀ (i j : Fin n),
    i ≠ j →
      i < j →
        ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
            ↑(min (t i.castSucc) (t j.castSucc)) =
          0
h : ¬i < j
⊢ ↑(min (t i.succ) (t j.succ)) - ↑(min (t j.castSucc) (t i.succ)) - ↑(min (t i.castSucc) (t j.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc)) =
    ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.castSucc) (t j.succ)) - ↑(min (t j.castSucc) (t i.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc))
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ ∫ (x : Ω), B (t₀ + t) x - B t₀ x ∂P = 0

Tactic:
rw [integral_sub, hB.integral_eval, hB.integral_eval, sub_zero]
    all_goals exact (hB.isGaussianProcess.hasGaussianLaw_eval _).integrable

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

Goal state before:
pp: case hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0 ⊕ ↑(Set.Iic t₀)),
    ∃ I L, ∀ (ω : Ω), Sum.elim (fun s ω ↦ B (t₀ + s) ω - B t₀ ω) (fun t ↦ B ↑t) s ω = L (I.restrict fun x ↦ B x ω)

Tactic:
rintro (t | ⟨t, ht⟩)

Goal state after:
case hXY.inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
⊢ ∃ I L,
    ∀ (ω : Ω), Sum.elim (fun s ω ↦ B (t₀ + s) ω - B t₀ ω) (fun t ↦ B ↑t) (Sum.inl t) ω = L (I.restrict fun x ↦ B x ω)

case hXY.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
ht : t ∈ Set.Iic t₀
⊢ ∃ I L,
    ∀ (ω : Ω),
      Sum.elim (fun s ω ↦ B (t₀ + s) ω - B t₀ ω) (fun t ↦ B ↑t) (Sum.inr ⟨t, ht⟩) ω = L (I.restrict fun x ↦ B x ω)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
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 t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑⟨t, ht⟩; P] = 0

Tactic:
rw [covariance_fun_sub_left, hB.covariance_eval, hB.covariance_eval, min_eq_right, min_eq_right,
      sub_self]

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 t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ ↑⟨t, ht⟩ ≤ t₀

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 t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ ↑⟨t, ht⟩ ≤ t₀ + s

case h.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + s)) 2 P

case h.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

case h.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B ↑⟨t, ht⟩) 2 P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
⊢ ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun x ↦ B x ω) (𝓝 0) (𝓝 0)

Tactic:
filter_upwards [hB.cont, hB.eval_zero_ae_eq_zero] with ω h1 h2

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
ω : Ω
h1 : Continuous fun x ↦ B x ω
h2 : B 0 ω = 0
⊢ Filter.Tendsto (fun x ↦ B x ω) (𝓝 0) (𝓝 0)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), (η (b, f ω).2) (Prod.mk b_1 ⁻¹' s) ∂ξ (b, f ω) =
    ∫⁻ (c : δ), ((η.comap f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (b, f ω)

Tactic:
comap_apply

Goal state after:
case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), (η (b, f ω).2) (Prod.mk b_1 ⁻¹' s) ∂ξ (b, f ω) = ∫⁻ (c : δ), (η (f ω)) (Prod.mk c ⁻¹' s) ∂ξ (b, f ω)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), (η (f ω, b).1) (Prod.mk b_1 ⁻¹' s) ∂ξ (f ω, b) =
    ∫⁻ (c : δ), ((η.comap f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (f ω, b)

Tactic:
comap_apply

Goal state after:
case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), (η (f ω, b).1) (Prod.mk b_1 ⁻¹' s) ∂ξ (f ω, b) = ∫⁻ (c : δ), (η (f ω)) (Prod.mk c ⁻¹' s) ∂ξ (f ω, b)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y ↦ x ⊆ y) fun q ↦ Iic ↑q
h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q ↦ s ×ˢ Iic ↑q
q : ℚ
⊢ Measurable fun b ↦ ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic ↑q)

Tactic:
exact (Kernel.measurable_coe _ measurableSet_Iic).comp measurable_prodMk_left

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 : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a = (κ a) (f' i)
h_eq : ∀ (a : β), Prod.mk a ⁻¹' ⋃ i, f' i = ⋃ i, Prod.mk a ⁻¹' f' i
h_disj : ∀ (a : β), Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i)
⊢ ∑' (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a = ∑' (i : ℕ), (κ a) (f' i)

Tactic:
by simp_rw [hf_eq]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : ¬(ν a) (countablePartitionSet n x) = 0
h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
⊢ κ a ≤ κ' a

Tactic:
· apply hκκ'

Goal state after:
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ ((Measure.map (fun a ↦ (X a, Y a)) μ).fst {x})⁻¹ * (Measure.map (fun a ↦ (X a, Y a)) μ) ({x} ×ˢ s) =
    ((Measure.map X μ) {x})⁻¹ * (Measure.map (fun a ↦ (X a, Y a)) μ) ({x} ×ˢ s)

Tactic:
rw [Measure.fst_map_prodMk hY]

Goal state after:
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ).fst {x} ≠ 0

Tactic:
rwa [Measure.fst_map_prodMk hY]

Goal state after: