-- Mathlib/Probability/Process/Stopping.lean
theorem measurable_stoppedValue [MetrizableSpace β] [MeasurableSpace β] [BorelSpace β]
    (hf_prog : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
    Measurable[hτ.measurableSpace] (stoppedValue u τ)

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
u : ι → Ω → β
τ : Ω → ι
f : Filtration ι m
inst✝² : MetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : ProgMeasurable f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => τ ω ⊓ i)
t : Set β
ht : MeasurableSet t
i : ι
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i})

Tactic:
suffices stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ i} =
    (stoppedValue u fun ω => min (τ ω) i) ⁻¹' t ∩ {ω : Ω | τ ω ≤ i} by
  rw [this]; exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
u : ι → Ω → β
τ : Ω → ι
f : Filtration ι m
inst✝² : MetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : ProgMeasurable f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => τ ω ⊓ i)
t : Set β
ht : MeasurableSet t
i : ι
⊢ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} = (stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i}

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
u : ι → Ω → β
τ : Ω → ι
f : Filtration ι m
inst✝² : MetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : ProgMeasurable f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => τ ω ⊓ i)
t : Set β
ht : MeasurableSet t
i : ι
⊢ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} = (stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
u : ι → Ω → β
τ : Ω → ι
f : Filtration ι m
inst✝² : MetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : ProgMeasurable f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => τ ω ⊓ i)
t : Set β
ht : MeasurableSet t
i : ι
ω : Ω
⊢ ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} ↔ ω ∈ (stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i}

Proof state:
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
u : ι → Ω → β
τ : Ω → ι
f : Filtration ι m
inst✝² : MetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : ProgMeasurable f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => τ ω ⊓ i)
t : Set β
ht : MeasurableSet t
i : ι
ω : Ω
h : τ ω ≤ i
⊢ u (τ ω) ω ∈ t ↔ u (τ ω ⊓ i) ω ∈ t

Tactic:
rw [min_eq_left h]

Result:
no goals