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

Goal state before:
pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ μ.real s • ∫ (a : Ω), u a ∂μ = ∫ (x : Ω) in s, v x ∂μ

Tactic:
←
      (setIntegral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)

Goal state after:
case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ μ.real s • ∫ (a : Ω), u a ∂μ = ∫ (x : Ω) in s, u x ∂μ

Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t✝ : Set β
ht : MeasurableSet t✝
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
a✝ : stoppedValue u τ ω ∈ t✝
t : ι
⊢ (∃ x, ↑t ≤ ↑(seq x)) ∨ ↑t = ⊤

Tactic:
simp only [coe_le_coe, coe_ne_top, or_false]

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t✝ : Set β
ht : MeasurableSet t✝
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
a✝ : stoppedValue u τ ω ∈ t✝
t : ι
⊢ ∃ x, t ≤ seq x
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
⊢ stoppedValue u τ y = (∑ i ∈ s, {ω | τ ω = ↑i}.indicator (u i)) y

Tactic:
rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
⊢ u (τ y).untopA y = ∑ i ∈ s with y ∈ {ω | τ ω = ↑i}, u i y
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ f n ω) atTop atBot

Tactic:
filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
    not_bddBelow_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n ≤ τ a}.indicator (u n) x = ({a | τ a = ↑n} ∪ {a | ↑n + 1 ≤ τ a}).indicator (u n) x

Tactic:
simp_rw [@eq_comm _ _ (n : WithTop ℕ), @le_iff_eq_or_lt _ _ (n : WithTop ℕ)]

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n = τ a ∨ ↑n < τ a}.indicator (u n) x = ({a | ↑n = τ a} ∪ {a | ↑n + 1 ≤ τ a}).indicator (u n) x
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
ω : Ω
hl : a ≤ X ω
hr : X ω ≤ b
ht : ¬0 ≤ t
⊢ (a * t ≤ t * X ω ∨ b * t ≤ t * X ω) ∧ (t * X ω ≤ a * t ∨ t * X ω ≤ b * t)

Tactic:
exact ⟨Or.inr (by nlinarith), Or.inl (by nlinarith)⟩

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ x ∉ {a | τ a = ↑n} ∩ {a | ↑n + 1 ≤ τ a}

Tactic:
rintro ⟨h₁, h₂⟩
      rw [Set.mem_ofPred] at h₁ h₂
      rw [h₁] at h₂
      norm_cast at h₂
      grind

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (fun t ↦ ∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
have h_re_of_mem n t (ht' : t ∈ interior (integrableExpSet X μ)) :
      (∫ ω, X ω ^ n * Complex.exp (t * X ω) ∂μ).re = ∫ ω, X ω ^ n * exp (t * X ω) ∂μ := by
    rw [← RCLike.re_eq_complex_re, ← integral_re]
    · norm_cast
    · refine integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet ?_ n
      simpa using ht'
  have h_re n : ∀ᶠ t' : ℝ in 𝓝 t, (∫ ω, X ω ^ n * Complex.exp (t' * X ω) ∂μ).re
      = ∫ ω, X ω ^ n * exp (t' * X ω) ∂μ := by
    filter_upwards [isOpen_interior.eventually_mem ht] with t ht' using h_re_of_mem n t ht'
  rw [← EventuallyEq.hasDerivAt_iff (h_re _), ← h_re_of_mem _ t ht]
  exact (hasDerivAt_integral_pow_mul_exp (by simp [ht]) n).real_of_complex

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ NullSingletonClass (gaussianReal μ v)

Tactic:
rw [gaussianReal_of_var_ne_zero _ h]
  infer_instance

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

Tactic:
exact gaussianReal_map_const_mul c

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

Goal state before:
pp: μ : Measure ℝ
h : IsGaussian μ
⊢ Measure.map (⇑(ContinuousLinearMap.id ℝ ℝ)) μ = gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal

Tactic:
rw [h.map_eq_gaussianReal]; simp

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

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ ∑ i, ∑ j, cov[fun ω ↦ x.ofLp i * X i ω, fun ω ↦ y.ofLp j * X j ω; μ] =
    ∑ x_1, ∑ x_2, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]

Tactic:
refine Finset.sum_congr rfl fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_
      rw [covariance_const_mul_left, covariance_const_mul_right]
      ring

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
r : ℝ
hxr : ∀ x ∈ s, ‖x‖ ≤ r
L : StrongDual 𝕜 E
hLs : L ∈ s
⊢ ‖(toLpₗ μ p) L‖ ≤ r * (eLpNorm id p μ).toReal

Tactic:
specialize hxr L hLs

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
r : ℝ
L : StrongDual 𝕜 E
hxr : ‖L‖ ≤ r
hLs : L ∈ s
⊢ ‖(toLpₗ μ p) L‖ ≤ r * (eLpNorm id p μ).toReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2 ≤ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n

Tactic:
simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero,
      Nat.ofNat_pos, pow_pos, mul_nonneg_iff_of_pos_right, inv_pos, mul_nonneg_iff_of_pos_left]

Goal state after:
case pos
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 0 ≤ Real.log (c.toReal / (1 - c).toReal)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (x : ↥I → ℝ), x s - x t ∂projectiveFamily I) Var[fun x ↦ x s - x t; projectiveFamily I].toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
variance_fun_sub,

Goal state after:
I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (x : ↥I → ℝ), x s - x t ∂projectiveFamily I)
      (Var[fun x ↦ x s; projectiveFamily I] - 2 * cov[fun x ↦ x s, fun x ↦ x t; projectiveFamily I] +
          Var[fun x ↦ x t; projectiveFamily I]).toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)

case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
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
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᵐ[μ] closedBall 0 a

Tactic:
← ae_iff_prob_eq_one ?_

Goal state after:
case pos
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
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᵐ[μ] closedBall 0 a

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
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Measurable fun x ↦ ‖x‖ ≤ a
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
· exact (IsGaussian.hasGaussianLaw_id.eval t).integrable

Goal state after:
case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: case e'_6.e'_5.e'_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
i : Fin n
ω : Ω
⊢ ↑i.succ = min n (↑i + 1)

pp: case e'_6.e'_6.e'_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
i : Fin n
ω : Ω
⊢ ↑i.castSucc = min n ↑i

pp: case convert_1
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ Monotone t'

pp: case convert_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ EventuallyConst t' atTop

Tactic:
· grind

Goal state after:
case e'_6.e'_6.e'_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
i : Fin n
ω : Ω
⊢ ↑i.castSucc = min n ↑i

case convert_1
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ Monotone t'

case convert_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ EventuallyConst t' atTop
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: case e'_6.e'_6.e'_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
i : Fin n
ω : Ω
⊢ ↑i.castSucc = min n ↑i

pp: case convert_1
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ Monotone t'

pp: case convert_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ EventuallyConst t' atTop

Tactic:
· grind

Goal state after:
case convert_1
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ Monotone t'

case convert_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ EventuallyConst t' atTop
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case convert_11
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s✝ : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
e : ↥(insert i s) → ι := Subtype.val
⊢ ∀ i_1 ∈ {x | ↑x ∈ s}, X ↑i_1 = X ↑i_1

Tactic:
· grind

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
⊢ cov[(fun ω ↦ ω i) ∘ fun ω ↦ I.restrict fun x ↦ X x ω, (fun ω ↦ ω j) ∘ fun ω ↦ I.restrict fun x ↦ X x ω; P] =
    ↑(min ↑i ↑j)

Tactic:
covariance_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
⊢ cov[(fun ω ↦ ω j) ∘ fun ω ↦ I.restrict fun x ↦ X x ω, (fun ω ↦ ω i) ∘ fun ω ↦ I.restrict fun x ↦ X x ω; P] =
    ↑(min ↑i ↑j)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x)

Tactic:
← sub_zero (hf.stieltjesFunction a x)

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x - 0)
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
⊢ ↑⟨t, ht⟩ ≤ t₀

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
⊢ ↑⟨t, ht⟩ ≤ t₀ + s

pp: 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

pp: 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

pp: 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

Tactic:
· grind

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₀ + 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.Kernel.Disintegration.Basic

Goal state before:
pp: case inl
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hx : ρ.fst {a} ≠ 0
⊢ (ρCond a) (Prod.mk a ⁻¹' {a} ×ˢ s) = {a}.indicator (fun x ↦ (ρCond x) s) a

pp: case inr
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hax : a ≠ x
⊢ (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a

Tactic:
· simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]
      congr with y
      simp

Goal state after:
case inr
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hax : a ≠ x
⊢ (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a