-- Mathlib/Probability/Process/Stopping.lean
theorem condExp_min_stopping_time_ae_eq_restrict_le [MeasurableSpace ι] [SecondCountableTopology ι]
    [BorelSpace ι] (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ)
    [SigmaFinite (μ.trim (hτ.min hσ).measurableSpace_le)] :
    μ[f|(hτ.min hσ).measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[f|hτ.measurableSpace]

Proof state:
case hπ
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ IsStoppingTime ℱ σ

Tactic:
simp_all only

Result:
no goals

Proof state:
case hπ
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ IsStoppingTime ℱ σ

Tactic:
simp_all only

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ μ[f|⋯.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x ≤ σ x})] μ[f|hτ.measurableSpace]

Tactic:
refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
  (hτ.min hσ).measurableSpace_le (hτ.measurableSet_le_stopping_time hσ) fun t => ?_).symm

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)

Tactic:
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_le_iff]

Result:
case hπ
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ IsStoppingTime ℱ σ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ IsStoppingTime.measurableSpace ?hτ ⊓ IsStoppingTime.measurableSpace ?hπ ≤ hτ.measurableSpace

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace

Tactic:
rw [IsStoppingTime.measurableSpace_min]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ IsStoppingTime.measurableSpace ?hτ ⊓ IsStoppingTime.measurableSpace ?hπ ≤ hτ.measurableSpace

case hτ
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ IsStoppingTime ℱ τ

case hπ
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → ι
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
f : Ω → E
inst✝⁶ : atTop.IsCountablyGenerated
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : MeasurableSpace ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ IsStoppingTime ℱ σ