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 : ι)
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 : ι) ≤ i

Tactic:
have hx_fst_le : ↑(ω : Set.Iic i × Ω).fst ≤ i := (ω : Set.Iic i × Ω).fst.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 : ι)
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
neg :
  ∀ (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

Tactic:
by_cases h : τ (ω : Set.Iic i × Ω).2 = ⊤

Premises used: Subtype.val, Prod.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 : ι)
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

Tactic:
simp [h]
-- 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))
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) × Ω).2 ≠ ⊤

Tactic:
h
-- 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))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
h : ¬τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 = ⊤
neg :
  ∀ (t : ι) (ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2),
    (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ (↑t : WithTop ι)
⊢ (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2

Tactic:
lift τ (ω : Set.Iic i × Ω).2 to ι using h with t ht

Premises used: Subtype.val, Prod.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 : ι)
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
neg : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ t
⊢ (↑(↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) : WithTop ι) ≤ (↑t : WithTop ι)

Tactic:
norm_cast
-- 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))
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

Tactic:
hx_fst_le.trans (le_of_lt ?_)

Premises used: le_of_lt, LE.le.trans
-- 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))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
t : ι
ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
neg : i < t
⊢ (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ t

Tactic:
refine hx_fst_le.trans (le_of_lt ?_)

Premises used: le_of_lt, LE.le.trans
-- 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))
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) × Ω) ∈ sc

Tactic:
ω.prop

Premises used: Subtype.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 : ι)
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
a : i < t ↔ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω) ∈ sc
⊢ i < t

Tactic:
convert! ω.prop

Premises used: Subtype.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 : ι)
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
a : i < t ↔ (↑i : WithTop ι) < (↑t : WithTop ι)
⊢ i < t ↔ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω) ∈ sc

Tactic:
simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_setOf_eq, ← ht]

Premises used: not_le, Set.mem_setOf_eq, Set.mem_compl_iff
-- 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))
hx_fst_le : (↑(↑ω : (↑(Set.Iic i) : Type u_3) × Ω).1 : ι) ≤ i
t : ι
ht : (↑t : WithTop ι) = τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2
a a₁ a₂ a₃ : i < t ↔ i < t
⊢ i < t ↔ (↑i : WithTop ι) < (↑t : WithTop ι)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Process.Stopping
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 fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA

Tactic:
have h_meas := isStronglyProgressive_min_stopping_time hτ
-- Module: Mathlib.Probability.Process.Stopping
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 τ)

Tactic:
h.comp h_meas fun i ω ↦ ?_

Premises used: MeasureTheory.stoppedProcess, MeasureTheory.IsStronglyProgressive.comp
-- Module: Mathlib.Probability.Process.Stopping
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
refine : ∀ (i : ι) (ω : Ω), (min (↑i : WithTop ι) (τ ω)).untopA ≤ i
⊢ IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)

Tactic:
refine h.comp h_meas fun i ω ↦ ?_

Premises used: MeasureTheory.IsStronglyProgressive.comp
-- Module: Mathlib.Probability.Process.Stopping
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
i : ι
ω : Ω
⊢ (min (↑i : WithTop ι) ⊤).untopA ≤ i

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
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
i : ι
ω : Ω
t : ι
coe : ∀ (h_it : i ≤ t), (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i
coe₁ : ∀ (h_ti : t ≤ i), (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i
⊢ (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i

Tactic:
rcases le_total i t with h_it | h_ti

Premises used: le_total
-- Module: Mathlib.Probability.Process.Stopping
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
i : ι
ω : Ω
t : ι
h_it : i ≤ t
⊢ (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i

Tactic:
simp [(mod_cast h_it : (i : WithTop ι) ≤ t)]

Premises used: WithTop.coe_le_coe._simp_1, cast, Eq.symm
-- Module: Mathlib.Probability.Process.Stopping
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
i : ι
ω : Ω
t : ι
h_ti : t ≤ i
⊢ (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i

Tactic:
simpa [(mod_cast h_ti : t ≤ (i : WithTop ι))]

Premises used: WithTop.coe_le_coe._simp_1, cast, Eq.symm