awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι)
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 (α := (↑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 simp : Measurable (β := WithTop ι) fun (x : (↑sᶜ : Type (max u_1 u_3))) ↦
  (↑(↑(↑x : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι)
Tactic: simp +unfoldPartialApp only [sc, Set.restrict, h_min_eq_left]
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
⊢ 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_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 ι)
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
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
⊢ 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 ι)
have 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 ι)
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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑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 ι)
have refine_2 : (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
Tactic: rw [min_eq_left]
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
⊢ (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
have hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
Tactic: have hx_fst_le : ↑(ω : Set.Iic i × Ω).fst ≤ i := (ω : Set.Iic i × Ω).fst.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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
⊢ (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
have pos : ∀ (h : τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 = ⊤),
  (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
Tactic: by_cases h : τ (ω : Set.Iic i × Ω).2 = ⊤
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
pos :
  ∀ (h : τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 = ⊤),
    (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
have neg : ∀ (h : ¬τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 = ⊤),
  (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
Tactic: by_cases h : τ (ω : Set.Iic i × Ω).2 = ⊤
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
h : ¬τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 = ⊤
⊢ (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
have neg : ∀ (t : ι) (ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2),
  (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ (↑t : WithTop ι)
Tactic: lift τ (ω : Set.Iic i × Ω).2 to ι using h with t ht
Cleared hypotheses: h
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
t : ι
ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ (↑t : WithTop ι)
have neg : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ t
Tactic: norm_cast
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
t : ι
ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ t
have neg : i < t
Tactic: refine hx_fst_le.trans (le_of_lt ?_)
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
t : ι
ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ i < t
have a : i < t ↔ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω) ∈ sc
Tactic: convert! ω.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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
t : ι
ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ i < t ↔ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω) ∈ sc
have a : i < t ↔ (↑i : WithTop ι) < (↑t : WithTop ι)
Tactic: simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_setOf_eq, ← ht]
-- 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 : ι)
sc : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) := sᶜ
ω : (↑sc : Type (max u_1 u_3))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
t : ι
ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
⊢ i < t ↔ (↑i : WithTop ι) < (↑t : WithTop ι)
have a : i < t ↔ i < t
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
⊢ IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)
have h_meas : IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA
Tactic: have h_meas := isStronglyProgressive_min_stopping_time hτ
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA
⊢ IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)
have refine : ∀ (i : ι) (ω : Ω), (min (↑i : WithTop ι) (τ ω)).untopA ≤ i
Tactic: refine h.comp h_meas fun i ω ↦ ?_