-- Mathlib/Probability/Process/Stopping.lean
theorem stronglyMeasurable_stoppedValue_of_le (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ)
    {n : ι} (hτ_le : ∀ ω, τ ω ≤ n) : StronglyMeasurable[f n] (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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)
⊢ StronglyMeasurable (stoppedValue u τ)

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)
⊢ StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω))

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)
⊢ StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω))

Tactic:
refine StronglyMeasurable.comp_measurable (h n) ?_

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)
⊢ Measurable fun ω => (⟨τ ω, ⋯⟩, ω)

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)
⊢ Measurable fun ω => (⟨τ ω, ⋯⟩, ω)

Tactic:
exact (hτ.measurable_of_le hτ_le).subtype_mk.prod_mk measurable_id

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
⊢ stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
ω : Ω
⊢ stoppedValue u τ ω = ((fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)) ω

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
ω : Ω
⊢ stoppedValue u τ ω = ((fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)) ω

Tactic:
simp only [stoppedValue, Function.comp_apply, Subtype.coe_mk]

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
⊢ StronglyMeasurable (stoppedValue u τ)

Tactic:
have : stoppedValue u τ =
    (fun p : Set.Iic n × Ω => u (↑p.fst) p.snd) ∘ fun ω => (⟨τ ω, hτ_le ω⟩, ω) := by
  ext1 ω; simp only [stoppedValue, Function.comp_apply, Subtype.coe_mk]

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
h : ProgMeasurable f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ n
this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)
⊢ StronglyMeasurable (stoppedValue u τ)