awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ min (↑i : WithTop ι) (σ ω) ≠ ⊤

Tactic:
exact (lt_of_le_of_lt (min_le_right _ _) <| lt_top_iff_ne_top.2 hσ).ne

Premises used: Iff.mpr, lt_of_le_of_lt, lt_top_iff_ne_top, min_le_right, LT.lt.ne
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
rw : stoppedProcess u (σ ⊓ τ) = stoppedProcess u fun (ω : Ω) ↦ min (σ ω) (τ ω)
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u fun (ω : Ω) ↦ min (σ ω) (τ ω)

Tactic:
rw [stoppedProcess_stoppedProcess]

Premises used: MeasureTheory.stoppedProcess_stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
⊢ stoppedProcess u (σ ⊓ τ) = stoppedProcess u fun (ω : Ω) ↦ min (σ ω) (τ ω)

Tactic:
rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
h : σ ≤ τ
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u σ

Tactic:
simp [h]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
h : τ ≤ σ
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u τ

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 τ
⊢ IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA

Tactic:
fun i ↦ (Measurable.untopA ?_).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, MeasureTheory.IsStronglyProgressive, Measurable.untopA
-- 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 τ
refine :
  ∀ (i : ι),
    Measurable (β := WithTop ι) fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦
      min (↑(↑p.1 : ι) : WithTop ι) (τ p.2)
⊢ IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA

Tactic:
refine fun i ↦ (Measurable.untopA ?_).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, Measurable.untopA
-- 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 ι)}
⊢ MeasurableSet s

Tactic:
have hs : MeasurableSet[m_prod] s := @measurable_snd (Set.Iic i) Ω _ (f i) _ (hτ i)
-- 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
⊢ ∀ (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
-- 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 : ι)
⊢ Measurable (β := WithTop ι) fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦
    min (↑(↑p.1 : ι) : WithTop ι) (τ p.2)

Tactic:
measurable_of_restrict_of_restrict_compl hs ?_ ?_

Premises used: measurable_of_restrict_of_restrict_compl
-- 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 : ι)
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))
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))
⊢ Measurable (β := 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 ?_ ?_

Premises used: measurable_of_restrict_of_restrict_compl
-- 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 : ι)
⊢ 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:
Measurable.min (h_meas_fst s).withTop_coe ?_

Premises used: Measurable.withTop_coe, Set.restrict, Measurable.min
-- 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 : ι)
refine_1 : Measurable (β := WithTop ι) fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).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.min (h_meas_fst s).withTop_coe ?_

Premises used: Measurable.withTop_coe, Measurable.min
-- 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 : ι)
⊢ Measurable (β := WithTop ι) fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2

Tactic:
measurable_of_Iic fun j ↦ ?_

Premises used: measurable_of_Iic
-- 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 : ι)
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)
⊢ Measurable (β := WithTop ι) fun (a : (↑s : Type (max u_1 u_3))) ↦ τ (↑a : { x : ι // x ∈ Set.Iic i } × Ω).2

Tactic:
refine measurable_of_Iic fun j ↦ ?_

Premises used: measurable_of_Iic
-- 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 : ι)
⊢ 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:
simp
-- 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 :
  ∀ (ω : (↑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 ι)})
        ω
⊢ 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:
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 : ι)
j : ι
ω : (↑s : Type (max u_1 u_3))
h :
  τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑j : WithTop ι) →
    τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑i : WithTop ι)
⊢ 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:
simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_setOf_eq, Set.mem_setOf_eq, iff_and_self]

Premises used: Set.mem_setOf_eq, le_inf_iff, Set.preimage_setOf_eq, Set.mem_Iic, WithTop.coe_min, iff_and_self, Set.mem_preimage
-- 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 : ι
ω : (↑s : Type (max u_1 u_3))
⊢ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑j : WithTop ι) →
    τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑i : WithTop ι)

Tactic:
fun _ => ω.prop

Premises used: Set.Mem, setOf, 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 : ι)
j : ι
ω : (↑s : Type (max u_1 u_3))
⊢ τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑j : WithTop ι) →
    τ (↑ω : (↑(Set.Iic i) : Type u_3) × Ω).2 ≤ (↑i : WithTop ι)

Tactic:
exact fun _ => ω.prop

Premises used: Subtype.prop