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 β
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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
h :
  ∀ (ω : Ω),
    ω ∈ stoppedValue u τ ⁻¹' t ↔
      ω ∈
        (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
          stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}

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 τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h :
  stoppedValue u τ ω ∈ t ↔
    (stoppedValue u τ ω ∈ t ∧ ∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ stoppedValue u τ ω ∈ t ∧ τ ω = ⊤
⊢ ω ∈ stoppedValue u τ ⁻¹' t ↔
    ω ∈
      (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
        stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}

Tactic:
simp only [Set.mem_preimage, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq,
      exists_and_left]

Premises used: Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, exists_and_left, Set.mem_setOf_eq, 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 τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h : stoppedValue u τ ω ∈ t → (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤
⊢ stoppedValue u τ ω ∈ t ↔
    (stoppedValue u τ ω ∈ t ∧ ∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ stoppedValue u τ ω ∈ t ∧ τ ω = ⊤

Tactic:
rw [← and_or_left, iff_self_and]

Premises used: and_or_left, iff_self_and
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h : stoppedValue u τ ω ∈ t
pos : ∀ (h : τ ω = ⊤), (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤
neg : ∀ (h : ¬τ ω = ⊤), (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤
⊢ (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤

Tactic:
by_cases 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 β
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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h_1 : stoppedValue u τ ω ∈ t
h : τ ω = ⊤
⊢ (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤

Tactic:
.inr h

Premises used: Or.inr
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h_1 : stoppedValue u τ ω ∈ t
h : τ ω = ⊤
⊢ (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤

Tactic:
exact .inr 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 β
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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h_1 : stoppedValue u τ ω ∈ t
h : ¬τ ω = ⊤
⊢ τ ω ≠ ⊤

Tactic:
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 β
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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h_1 : stoppedValue u τ ω ∈ t
h : ¬τ ω = ⊤
neg : ∀ (t : ι), (∃ (x : ℕ), (↑t : WithTop ι) ≤ (↑(seq x) : WithTop ι)) ∨ (↑t : WithTop ι) = ⊤
⊢ (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤

Tactic:
lift τ ω to ι using h with t
-- 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_1 : Set β
ht : MeasurableSet t_1
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h : stoppedValue u τ ω ∈ t_1
t : ι
neg : ∃ (x : ℕ), t ≤ seq x
⊢ (∃ (x : ℕ), (↑t : WithTop ι) ≤ (↑(seq x) : WithTop ι)) ∨ (↑t : WithTop ι) = ⊤

Tactic:
simp only [coe_le_coe, coe_ne_top, or_false]

Premises used: WithTop.coe_ne_top, or_false, WithTop.coe_le_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 β
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_1 : Set β
ht : MeasurableSet t_1
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h : stoppedValue u τ ω ∈ t_1
t : ι
neg :
  ∀ (h_seq_tendsto : ∀ (b : ι), ∀ᶠ (a : ℕ) in atTop, b ≤ seq a) (ω : Ω),
    stoppedValue u τ ω ∈ t_1 → ∀ (t : ι), ∃ (x : ℕ), t ≤ seq x
⊢ ∃ (x : ℕ), t ≤ seq x

Tactic:
rw [tendsto_atTop] at h_seq_tendsto

Premises used: Filter.tendsto_atTop
-- 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_1 : Set β
ht : MeasurableSet t_1
seq : ℕ → ι
h_seq_tendsto : ∀ (b : ι), ∀ᶠ (a : ℕ) in atTop, b ≤ seq a
ω : Ω
h : stoppedValue u τ ω ∈ t_1
t : ι
⊢ ∃ (x : ℕ), t ≤ seq x

Tactic:
(h_seq_tendsto t).exists

Premises used: Filter.Eventually.exists
-- 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_1 : Set β
ht : MeasurableSet t_1
seq : ℕ → ι
h_seq_tendsto : ∀ (b : ι), ∀ᶠ (a : ℕ) in atTop, b ≤ seq a
ω : Ω
h : stoppedValue u τ ω ∈ t_1
t : ι
⊢ ∃ (x : ℕ), t ≤ seq x

Tactic:
exact (h_seq_tendsto t).exists

Premises used: Filter.Eventually.exists
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
⊢ stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}

Tactic:
have : stoppedValue u τ ⁻¹' t
      = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ seq n})
        ∪ (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}) := by
    ext1 ω
    simp only [Set.mem_preimage, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq,
      exists_and_left]
    rw [← and_or_left, iff_self_and]
    intro _
    by_cases h : τ ω = ⊤
    · exact .inr h
    · lift τ ω to ι using h with t
      simp only [coe_le_coe, coe_ne_top, or_false]
      rw [tendsto_atTop] at h_seq_tendsto
      exact (h_seq_tendsto t).exists
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
rw :
  MeasurableSet
    ((⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)

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 τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet
    ((⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})

Tactic:
MeasurableSet.union ?_ ?_

Premises used: MeasurableSet.union
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
refine_1 : MeasurableSet.{u_1} (α := Ω) (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)})
refine_2 : MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
⊢ MeasurableSet
    ((⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})

Tactic:
refine MeasurableSet.union ?_ ?_

Premises used: MeasurableSet.union
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)})

Tactic:
MeasurableSet.iUnion fun i ↦ f.le (seq i) _
      (measurableSet_preimage_stoppedValue_inter hf_prog hτ ht (seq i))

Premises used: MeasureTheory.stoppedValue, setOf, LE.le, MeasureTheory.measurableSet_preimage_stoppedValue_inter, WithTop.some, Inter.inter, Set.preimage, MeasureTheory.Filtration.le, MeasurableSet.iUnion
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)})

Tactic:
exact MeasurableSet.iUnion fun i ↦ f.le (seq i) _
      (measurableSet_preimage_stoppedValue_inter hf_prog hτ ht (seq i))

Premises used: MeasureTheory.stoppedValue, setOf, LE.le, MeasureTheory.measurableSet_preimage_stoppedValue_inter, WithTop.some, Inter.inter, Set.preimage, MeasureTheory.Filtration.le, MeasurableSet.iUnion
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
h :
  ∀ (ω : Ω),
    ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} ↔
      Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}) ω
⊢ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} = (fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}

Tactic:
ext ω
-- 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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
ω : Ω
h : τ ω = ⊤ → (u (untopD (Classical.arbitrary ι) (τ ω)) ω ∈ t ↔ u (Classical.arbitrary ι) ω ∈ t)
⊢ ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} ↔
    Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}) ω

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

Premises used: MeasureTheory.stoppedValue, Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_left_iff, WithTop.untopA, 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 τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
ω : Ω
h : τ ω = ⊤
⊢ u (untopD (Classical.arbitrary ι) (τ ω)) ω ∈ t ↔ u (Classical.arbitrary ι) ω ∈ t

Tactic:
simp [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 β
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
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} = (fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}

Tactic:
have : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
       = (fun ω ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω | τ ω = ⊤} := by
      ext ω
      simp only [Set.mem_inter_iff, Set.mem_preimage, stoppedValue, untopA,
        Set.mem_setOf_eq, and_congr_left_iff]
      intro h
      simp [h]