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₀ + min s t) - ↑(min (t₀ + s) t₀) - (↑(min t₀ (t₀ + t)) - ↑(min t₀ t₀)) = ↑s

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

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

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

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

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

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

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

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₀) 2 P

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 (fun ω ↦ B (t₀ + t) ω - B t₀ ω) 2 P

Tactic:
min_eq_left hst,

Goal state after:
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) - ↑(min (t₀ + s) t₀) - (↑(min t₀ (t₀ + t)) - ↑(min t₀ t₀)) = ↑s

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

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

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

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

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

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

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

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₀) 2 P

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 (fun ω ↦ B (t₀ + t) ω - B t₀ ω) 2 P