-- Mathlib/Probability/Process/Stopping.lean
theorem progMeasurable_min_stopping_time [MetrizableSpace ι] (hτ : IsStoppingTime f τ) :
    ProgMeasurable f fun i ω => min i (τ ω)

Proof state:
case hf.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
⊢ Measurable fun a => τ (↑a).2

Tactic:
refine @measurable_of_Iic ι s _ _ _ (m_set s) _ _ _ _ fun j => ?_

Result:
case hf.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
j : ι
⊢ MeasurableSet ((fun a => τ (↑a).2) ⁻¹' Set.Iic j)

Proof state:
case hf.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
⊢ Measurable (sᶜ.restrict fun p => (fun i ω => i ⊓ τ ω) (↑p.1) p.2)

Tactic:
suffices h_min_eq_left :
  (fun x : sc => min (↑(x : Set.Iic i × Ω).fst) (τ (x : Set.Iic i × Ω).snd)) = fun x : sc =>
    ↑(x : Set.Iic i × Ω).fst by
  simp +unfoldPartialApp only [sc, Set.restrict, h_min_eq_left]
  exact h_meas_fst _

Result:
case hf.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
⊢ (fun x => ↑(↑x).1 ⊓ τ (↑x).2) = fun x => ↑(↑x).1

Proof state:
case hf.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
j : ι
h_set_eq : (fun x => τ (↑x).2) ⁻¹' Set.Iic j = (fun x => (↑x).2) ⁻¹' {ω | τ ω ≤ i ⊓ j}
⊢ MeasurableSet ((fun a => τ (↑a).2) ⁻¹' Set.Iic j)

Tactic:
rw [h_set_eq]

Result:
case hf.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
j : ι
h_set_eq : (fun x => τ (↑x).2) ⁻¹' Set.Iic j = (fun x => (↑x).2) ⁻¹' {ω | τ ω ≤ i ⊓ j}
⊢ MeasurableSet ((fun x => (↑x).2) ⁻¹' {ω | τ ω ≤ i ⊓ j})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
⊢ StronglyMeasurable fun p => (fun i ω => i ⊓ τ ω) (↑p.1) p.2

Tactic:
let m_set : ∀ t : Set (Set.Iic i × Ω), MeasurableSpace t := fun _ =>
  @Subtype.instMeasurableSpace (Set.Iic i × Ω) _ m_prod

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
⊢ StronglyMeasurable fun p => (fun i ω => i ⊓ τ ω) (↑p.1) p.2

Proof state:
case hf.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
⊢ Measurable (sᶜ.restrict fun p => (fun i ω => i ⊓ τ ω) (↑p.1) p.2)

Tactic:
letI sc := sᶜ

Result:
case hf.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
⊢ Measurable (sᶜ.restrict fun p => (fun i ω => i ⊓ τ ω) (↑p.1) p.2)