-- 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 : ι
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} = (stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i}
⊢ MeasurableSet ((stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i})

Tactic:
exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)

Result:
no goals

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 : ι
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} = (stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i})

Tactic:
rw [this]

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 : ι
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} = (stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i}
⊢ MeasurableSet ((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 τ
⊢ Measurable (stoppedValue u τ)

Tactic:
have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>
  stronglyMeasurable_stoppedValue_of_le hf_prog (hτ.min_const i) fun _ => min_le_right _ _

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)
⊢ Measurable (stoppedValue u τ)

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 : ι
ω : Ω
⊢ ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} ↔ ω ∈ (stoppedValue u fun ω => τ ω ⊓ i) ⁻¹' t ∩ {ω | τ ω ≤ i}

Tactic:
simp only [stoppedValue, Set.mem_inter_iff, Set.mem_preimage, Set.mem_setOf_eq,
  and_congr_left_iff]

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 : ι
ω : Ω
⊢ τ ω ≤ i → (u (τ ω) ω ∈ t ↔ u (τ ω ⊓ i) ω ∈ t)

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)
⊢ Measurable (stoppedValue u τ)

Tactic:
intro t ht 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 : ι
⊢ MeasurableSet (stoppedValue u τ ⁻¹' 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 : ι
ω : Ω
⊢ τ ω ≤ i → (u (τ ω) ω ∈ t ↔ u (τ ω ⊓ i) ω ∈ t)

Tactic:
intro h

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 : ι
ω : Ω
h : τ ω ≤ i
⊢ u (τ ω) ω ∈ t ↔ u (τ ω ⊓ i) ω ∈ t