awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
ω : Ω
cases : ∀ (x : WithTop ι), (min (↑i : WithTop ι) x).untopA ≤ i
⊢ (min (↑i : WithTop ι) (τ ω)).untopA ≤ i

Tactic:
cases τ ω with
  | top => simp
  | coe t =>
    rcases le_total i t with h_it | h_ti
    · simp [(mod_cast h_it : (i : WithTop ι) ≤ t)]
    · simpa [(mod_cast h_ti : t ≤ (i : WithTop ι))]

Premises used: WithTop.top, WithTop.coe
-- 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 τ
⊢ StronglyAdapted (β := fun (a : ι) ↦ β) f (MeasureTheory.stoppedProcess u τ)

Tactic:
(h.stoppedProcess hτ).stronglyAdapted

Premises used: MeasureTheory.IsStronglyProgressive.stronglyAdapted, MeasureTheory.IsStronglyProgressive.stoppedProcess
-- 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 ι
hu : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
i : ι
⊢ StronglyMeasurable (MeasureTheory.stoppedProcess u τ i)

Tactic:
(hu.stronglyAdapted_stoppedProcess hτ i).mono (f.le _)

Premises used: MeasureTheory.IsStronglyProgressive.stronglyAdapted_stoppedProcess, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.le
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ ∀ (ω : Ω), (τ ω).untopA ≤ n

Tactic:
have hτ_le' ω : (τ ω).untopA ≤ n := untopA_le (hτ_le ω)
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
h₁ :
  ∀ (ω : Ω),
    stoppedValue u τ ω =
      ((fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω))
        ω
⊢ stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)

Tactic:
ext1 ω
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
ω : Ω
⊢ stoppedValue u τ ω =
    ((fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω))
      ω

Tactic:
simp only [stoppedValue, Function.comp_apply]

Premises used: MeasureTheory.stoppedValue, Function.comp_apply
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
⊢ stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)

Tactic:
have : stoppedValue u τ =
      (fun p : Set.Iic n × Ω => u (↑p.fst) p.snd) ∘ fun ω => (⟨(τ ω).untopA, hτ_le' ω⟩, ω) := by
    ext1 ω; simp only [stoppedValue, Function.comp_apply]
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this :
  stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
rw :
  StronglyMeasurable.{u_1, u_2} (α := Ω) (β := β)
    ((fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω))
⊢ StronglyMeasurable (stoppedValue u τ)

Tactic:
rw [this]
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this :
  stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
⊢ StronglyMeasurable.{u_1, u_2} (α := Ω) (β := β)
    ((fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω))

Tactic:
StronglyMeasurable.comp_measurable (h n) ?_

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this :
  stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
refine :
  Measurable (β := Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) fun (ω : Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
⊢ StronglyMeasurable.{u_1, u_2} (α := Ω) (β := β)
    ((fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω))

Tactic:
refine StronglyMeasurable.comp_measurable (h n) ?_

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this :
  stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
⊢ Measurable (β := Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) fun (ω : Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)

Tactic:
(Measurable.subtype_mk ?_).prodMk measurable_id

Premises used: Measurable.subtype_mk, measurable_id, Measurable.prodMk
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this :
  stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
refine : Measurable.{u_1, u_3} (β := ι) fun (ω : Ω) ↦ (τ ω).untopA
⊢ Measurable (β := Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) fun (ω : Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)

Tactic:
refine (Measurable.subtype_mk ?_).prodMk measurable_id

Premises used: Measurable.subtype_mk, measurable_id, Measurable.prodMk
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this :
  stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
⊢ Measurable.{u_1, u_3} (β := ι) fun (ω : Ω) ↦ (τ ω).untopA

Tactic:
(hτ.measurable_of_le hτ_le).untopA

Premises used: MeasureTheory.IsStoppingTime.measurable_of_le, Measurable.untopA
-- 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this :
  stoppedValue u τ =
    (fun (p : Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (ω : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA ⋯, ω)
⊢ Measurable.{u_1, u_3} (β := ι) fun (ω : Ω) ↦ (τ ω).untopA

Tactic:
exact (hτ.measurable_of_le hτ_le).untopA

Premises used: MeasureTheory.IsStoppingTime.measurable_of_le, Measurable.untopA
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
⊢ ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))

Tactic:
have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>
    stronglyMeasurable_stoppedValue_of_le hf_prog (hτ.min_const i) fun _ => min_le_right _ _
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
this :
  stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
rw : MeasurableSet ((stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
rw [this]
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
this :
  stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet ((stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.IsStoppingTime.measurableSet_le, MeasurableSet.inter
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
this :
  stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet ((stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.IsStoppingTime.measurableSet_le, MeasurableSet.inter
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
suffices :
  stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
suffices stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ i} =
      (stoppedValue u fun ω => min (τ ω) i) ⁻¹' t ∩ {ω : Ω | τ ω ≤ i} by
    rw [this]; exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
h :
  ∀ (ω : Ω),
    ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ↔
      ω ∈ (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
⊢ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
ext1 ω
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
ω : Ω
h : τ ω ≤ (↑i : WithTop ι) → (u (τ ω).untopA ω ∈ t ↔ u (min (τ ω) (↑i : WithTop ι)).untopA ω ∈ t)
⊢ ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ↔
    ω ∈ (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
simp only [stoppedValue, Set.mem_inter_iff, Set.mem_preimage, Set.mem_setOf_eq,
    and_congr_left_iff]

Premises used: MeasureTheory.stoppedValue, Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_left_iff, Set.mem_preimage
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
ω : Ω
h : τ ω ≤ (↑i : WithTop ι)
h₁ h₂ : u (τ ω).untopA ω ∈ t ↔ u (τ ω).untopA ω ∈ t
⊢ u (τ ω).untopA ω ∈ t ↔ u (min (τ ω) (↑i : WithTop ι)).untopA ω ∈ t

Tactic:
rw [min_eq_left h]

Premises used: min_eq_left
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
⊢ ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))

Tactic:
have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>
    stronglyMeasurable_stoppedValue_of_le hf_prog (hτ.min_const i) fun _ => min_le_right _ _
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)

Tactic:
⟨?_, fun i ↦ measurableSet_preimage_stoppedValue_inter hf_prog hτ ht i⟩

Premises used: MeasurableSet, MeasureTheory.measurableSet_preimage_stoppedValue_inter, And.intro
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
refine : MeasurableSet (stoppedValue u τ ⁻¹' t)
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)

Tactic:
refine ⟨?_, fun i ↦ measurableSet_preimage_stoppedValue_inter hf_prog hτ ht i⟩
-- 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 β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
obtain : ∀ (seq : ℕ → ι) (h_seq_tendsto : Tendsto seq atTop atTop), MeasurableSet (stoppedValue u τ ⁻¹' t)
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)

Tactic:
obtain ⟨seq : ℕ → ι, h_seq_tendsto⟩ := (atTop : Filter ι).exists_seq_tendsto

Premises used: Filter.seq, Filter.atTop, Filter.exists_seq_tendsto