awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
⊢ Measurable (β := WithTop ι) fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦
    min (↑(↑p.1 : ι) : WithTop ι) (τ p.2)
have h_meas_fst : ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
  Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
Tactic: have h_meas_fst : ∀ t : Set (Set.Iic i × Ω),
      Measurable[m_set t] fun x : t => ((x : Set.Iic i × Ω).fst : ι) :=
    fun t => (@measurable_subtype_coe (Set.Iic i × Ω) m_prod _).fst.subtype_val
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
⊢ Measurable (β := WithTop ι) fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦
    min (↑(↑p.1 : ι) : WithTop ι) (τ p.2)
have refine_1 : Measurable (α := (↑s : Type (max u_1 u_3))) (β := WithTop ι)
  (s.restrict (π := fun (a : Prod.{u_3, u_1} { x : ι // x ∈ Set.Iic i } Ω) ↦ WithTop ι)
    fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ min (↑(↑p.1 : ι) : WithTop ι) (τ p.2))
Tactic: refine measurable_of_restrict_of_restrict_compl hs ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
refine_1 :
  Measurable (α := (↑s : Type (max u_1 u_3))) (β := WithTop ι)
    (s.restrict (π := fun (a : Prod.{u_3, u_1} { x : ι // x ∈ Set.Iic i } Ω) ↦ WithTop ι)
      fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ min (↑(↑p.1 : ι) : WithTop ι) (τ p.2))
⊢ Measurable (β := WithTop ι) fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦
    min (↑(↑p.1 : ι) : WithTop ι) (τ p.2)
have refine_2 : Measurable (α := (↑sᶜ : Type (max u_1 u_3))) (β := WithTop ι)
  (sᶜ.restrict (π := fun (a : Prod.{u_3, u_1} { x : ι // x ∈ Set.Iic i } Ω) ↦ WithTop ι)
    fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ min (↑(↑p.1 : ι) : WithTop ι) (τ p.2))
Tactic: refine measurable_of_restrict_of_restrict_compl hs ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
⊢ Measurable (α := (↑s : Type (max u_1 u_3))) (β := WithTop ι)
    (s.restrict (π := fun (a : Prod.{u_3, u_1} { x : ι // x ∈ Set.Iic i } Ω) ↦ WithTop ι)
      fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ min (↑(↑p.1 : ι) : WithTop ι) (τ p.2))
have refine_1 : Measurable (β := WithTop ι) fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2
Tactic: refine Measurable.min (h_meas_fst s).withTop_coe ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
⊢ Measurable (β := WithTop ι) fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2
have refine_1 : ∀ (j : WithTop ι),
  MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    ((fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2) ⁻¹' Set.Iic j)
Tactic: refine measurable_of_Iic fun j ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
j : ι
⊢ Eq (α := Set (↑s : Type (max u_1 u_3)))
    ((fun (x : (↑s : Type (max u_1 u_3))) ↦ τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
    (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
      {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
have h : ∀ (ω : (↑s : Type (max u_1 u_3))),
  Membership.mem (γ := Set (↑s : Type (max u_1 u_3)))
      ((fun (x : (↑s : Type (max u_1 u_3))) ↦ τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
      ω ↔
    Membership.mem (γ := Set (↑s : Type (max u_1 u_3)))
      (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
        {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
      ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
j : ι
ω : (↑s : Type (max u_1 u_3))
⊢ Membership.mem (γ := Set (↑s : Type (max u_1 u_3)))
      ((fun (x : (↑s : Type (max u_1 u_3))) ↦ τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
      ω ↔
    Membership.mem (γ := Set (↑s : Type (max u_1 u_3)))
      (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
        {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
      ω
have h : τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑j : WithTop ι) →
  τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑i : WithTop ι)
Tactic: simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_setOf_eq, Set.mem_setOf_eq, iff_and_self]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
j : ι
⊢ MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    ((fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
have h_set_eq : Eq (α := Set (↑s : Type (max u_1 u_3)))
  ((fun (x : (↑s : Type (max u_1 u_3))) ↦ τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
  (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
    {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
Tactic: have h_set_eq : (fun x : s => τ (x : Set.Iic i × Ω).snd) ⁻¹' Set.Iic j =
          (fun x : s => (x : Set.Iic i × Ω).snd) ⁻¹' {ω | τ ω ≤ min i j} := by
        ext1 ω
        simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_setOf_eq, Set.mem_setOf_eq, iff_and_self]
        exact fun _ => ω.prop
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
j : ι
h_set_eq :
  Eq (α := Set (↑s : Type (max u_1 u_3)))
    ((fun (x : (↑s : Type (max u_1 u_3))) ↦ τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
    (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
      {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
⊢ MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    ((fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
have refine_1 : MeasurableSet (α := (↑s : Type (max u_1 u_3)))
  (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
    {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
Tactic: rw [h_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
j : ι
h_set_eq :
  Eq (α := Set (↑s : Type (max u_1 u_3)))
    ((fun (x : (↑s : Type (max u_1 u_3))) ↦ τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
    (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
      {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
⊢ MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    (Set.preimage (β := Ω) (fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2)
      {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)})
have refine_1 : Measurable (β := Ω) fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2
Tactic: suffices h_meas : @Measurable _ _ (m_set s) (f i) fun x : s ↦ (x : Set.Iic i × Ω).snd from
        h_meas (f.mono (min_le_left _ _) _ (hτ.measurableSet_le (min i j)))
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
j : WithTop ι
⊢ MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    ((fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2) ⁻¹' Set.Iic j)
have refine_1 : MeasurableSet (α := (↑s : Type (max u_1 u_3)))
  (Set.preimage (β := WithTop ι) (fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2)
    (Set.Iic ⊤))
Tactic: cases j with
    | top => simp
    | coe j =>
      have h_set_eq : (fun x : s => τ (x : Set.Iic i × Ω).snd) ⁻¹' Set.Iic j =
          (fun x : s => (x : Set.Iic i × Ω).snd) ⁻¹' {ω | τ ω ≤ min i j} := by
        ext1 ω
        simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_setOf_eq, Set.mem_setOf_eq, iff_and_self]
        exact fun _ => ω.prop
      rw [h_set_eq]
      suffices h_meas : @Measurable _ _ (m_set s) (f i) fun x : s ↦ (x : Set.Iic i × Ω).snd from
        h_meas (f.mono (min_le_left _ _) _ (hτ.measurableSet_le (min i j)))
      exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
hs : MeasurableSet s
h_meas_fst :
  ∀ (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)),
    Measurable (β := ι) fun (x : (↑t : Type (max u_1 u_3))) ↦ (↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι)
j : WithTop ι
refine_1 :
  MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    (Set.preimage (β := WithTop ι) (fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2)
      (Set.Iic ⊤))
⊢ MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    ((fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2) ⁻¹' Set.Iic j)
have refine_1₁ : ∀ (j : ι),
  MeasurableSet (α := (↑s : Type (max u_1 u_3)))
    ((fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2) ⁻¹' Set.Iic (↑j : WithTop ι))
Tactic: cases j with
    | top => simp
    | coe j =>
      have h_set_eq : (fun x : s => τ (x : Set.Iic i × Ω).snd) ⁻¹' Set.Iic j =
          (fun x : s => (x : Set.Iic i × Ω).snd) ⁻¹' {ω | τ ω ≤ min i j} := by
        ext1 ω
        simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_setOf_eq, Set.mem_setOf_eq, iff_and_self]
        exact fun _ => ω.prop
      rw [h_set_eq]
      suffices h_meas : @Measurable _ _ (m_set s) (f i) fun x : s ↦ (x : Set.Iic i × Ω).snd from
        h_meas (f.mono (min_le_left _ _) _ (hτ.measurableSet_le (min i j)))
      exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)
Cleared hypotheses: j