awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})

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
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
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 ι)})
⊢ 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:
rw [h_set_eq]
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
refine_1 : Measurable (β := Ω) fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ 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:
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)))
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
⊢ Measurable (β := Ω) fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2

Tactic:
measurable_snd.comp (@measurable_subtype_coe _ m_prod _)

Premises used: measurable_subtype_coe, Measurable.comp, measurable_snd
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
⊢ Measurable (β := Ω) fun (x : (↑s : Type (max u_1 u_3))) ↦ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2

Tactic:
exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)

Premises used: measurable_subtype_coe, Measurable.comp, measurable_snd
-- Module: Mathlib.Probability.Process.Stopping
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 ⊤))
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 ι))
⊢ 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:
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 _)

Premises used: measurable_subtype_coe, Measurable.comp, WithTop.top, measurable_snd, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
h_min_eq_left :
  Eq (α := (x : (↑sc : Type (max u_1 u_3))) → WithTop ι)
    (fun (x : (↑sc : Type (max u_1 u_3))) ↦
      min (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) (τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2))
    fun (x : (↑sc : Type (max u_1 u_3))) ↦ (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)
simp :
  Measurable (β := WithTop ι) fun (x : (↑sᶜ : Type (max u_1 u_3))) ↦
    (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)
⊢ 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:
simp +unfoldPartialApp only [sc, Set.restrict, h_min_eq_left]

Premises used: Set.restrict
-- Module: Mathlib.Probability.Process.Stopping
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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
h_min_eq_left :
  Eq (α := (x : (↑sc : Type (max u_1 u_3))) → WithTop ι)
    (fun (x : (↑sc : Type (max u_1 u_3))) ↦
      min (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) (τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2))
    fun (x : (↑sc : Type (max u_1 u_3))) ↦ (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)
⊢ Measurable (β := WithTop ι) fun (x : (↑sᶜ : Type (max u_1 u_3))) ↦
    (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)

Tactic:
(h_meas_fst _).withTop_coe

Premises used: Set.Mem, setOf, Measurable.withTop_coe
-- Module: Mathlib.Probability.Process.Stopping
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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
h_min_eq_left :
  Eq (α := (x : (↑sc : Type (max u_1 u_3))) → WithTop ι)
    (fun (x : (↑sc : Type (max u_1 u_3))) ↦
      min (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) (τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2))
    fun (x : (↑sc : Type (max u_1 u_3))) ↦ (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)
⊢ Measurable (β := WithTop ι) fun (x : (↑sᶜ : Type (max u_1 u_3))) ↦
    (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)

Tactic:
exact (h_meas_fst _).withTop_coe

Premises used: Measurable.withTop_coe
-- Module: Mathlib.Probability.Process.Stopping
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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
refine_2 :
  Eq (α := (x : (↑sc : Type (max u_1 u_3))) → WithTop ι)
    (fun (x : (↑sc : Type (max u_1 u_3))) ↦
      min (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) (τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2))
    fun (x : (↑sc : Type (max u_1 u_3))) ↦ (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)
⊢ 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:
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 _).withTop_coe
-- Module: Mathlib.Probability.Process.Stopping
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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
refine_2 :
  ∀ (ω : (↑sc : Type (max u_1 u_3))),
    min (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) (τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2) =
      (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)
⊢ Eq (α := (x : (↑sc : Type (max u_1 u_3))) → WithTop ι)
    (fun (x : (↑sc : Type (max u_1 u_3))) ↦
      min (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) (τ (↑x : (↑(Set.Iic i) : Type u_3) × Ω).2))
    fun (x : (↑sc : Type (max u_1 u_3))) ↦ (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
refine_2 : (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ min (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) (τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2) =
    (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)

Tactic:
rw [min_eq_left]

Premises used: min_eq_left