awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA
i : ι
ω : Ω
t : ι
⊢ (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i
have coe : ∀ (h_it : i ≤ t), (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i
Tactic: rcases le_total i t with h_it | h_ti
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA
i : ι
ω : Ω
t : ι
coe : ∀ (h_it : i ≤ t), (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i
⊢ (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i
have coe₁ : ∀ (h_ti : t ≤ i), (min (↑i : WithTop ι) (↑t : WithTop ι)).untopA ≤ i
Tactic: rcases le_total i t with h_it | h_ti
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA
i : ι
ω : Ω
⊢ (min (↑i : WithTop ι) (τ ω)).untopA ≤ i
have cases : ∀ (x : WithTop ι), (min (↑i : WithTop ι) x).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 ι))]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ StronglyMeasurable (stoppedValue u τ)
have hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
Tactic: have hτ_le' ω : (τ ω).untopA ≤ n := untopA_le (hτ_le ω)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
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 ⋯, ω)
have 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 sorry, ω))
      ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
⊢ StronglyMeasurable (stoppedValue u τ)
have 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 sorry, ω)
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]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
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 (stoppedValue u τ)
have 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 sorry, ω))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
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 ⋯, ω))
have refine : Measurable (β := Prod.{u_3, u_1} (↑(Set.Iic n) : Type u_3) Ω) fun (ω : Ω) ↦
  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic n) (τ ω).untopA sorry, ω)
Tactic: refine StronglyMeasurable.comp_measurable (h n) ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
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 ⋯, ω)
have refine : Measurable.{u_1, u_3} (β := ι) fun (ω : Ω) ↦ (τ ω).untopA
Tactic: refine (Measurable.subtype_mk ?_).prodMk measurable_id
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have h_str_meas : ∀ (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 _ _
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have rw : MeasurableSet ((stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ι))
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have suffices : stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
  (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' 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)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ι))
⊢ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
have h : ∀ (ω : Ω),
  ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ↔
    ω ∈ (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ι))
ω : Ω
⊢ ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ↔
    ω ∈ (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)) ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
have h : τ ω ≤ (↑i : WithTop ι) → (u (τ ω).untopA ω ∈ t ↔ u (min (τ ω) (↑i : WithTop ι)).untopA ω ∈ t)
Tactic: simp only [stoppedValue, Set.mem_inter_iff, Set.mem_preimage, Set.mem_setOf_eq,
    and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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
have h₁ : u (τ ω).untopA ω ∈ t ↔ u (τ ω).untopA ω ∈ t
Tactic: rw [min_eq_left h]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
⊢ Measurable (stoppedValue u τ)
have h_str_meas : ∀ (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 _ _
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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)
have refine : MeasurableSet (stoppedValue u τ ⁻¹' t)
Tactic: refine ⟨?_, fun i ↦ measurableSet_preimage_stoppedValue_inter hf_prog hτ ht i⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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)
have obtain : ∀ (seq : ℕ → ι) (h_seq_tendsto : Tendsto seq atTop atTop), MeasurableSet (stoppedValue u τ ⁻¹' t)
Tactic: obtain ⟨seq : ℕ → ι, h_seq_tendsto⟩ := (atTop : Filter ι).exists_seq_tendsto
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ∩ {ω : Ω | τ ω = ⊤}
have h : ∀ (ω : Ω),
  ω ∈ stoppedValue u τ ⁻¹' t ↔
    ω ∈
      (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
        stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ∩ {ω : Ω | τ ω = ⊤}
have h : stoppedValue u τ ω ∈ t ↔
  (stoppedValue u τ ω ∈ t ∧ ∃ (x : ℕ), τ ω ≤ (↑(seq x) : 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]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ↔
    (stoppedValue u τ ω ∈ t ∧ ∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ stoppedValue u τ ω ∈ t ∧ τ ω = ⊤
have h : stoppedValue u τ ω ∈ t → (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤
Tactic: rw [← and_or_left, iff_self_and]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ι)) ∨ τ ω = ⊤
have pos : ∀ (h : τ ω = ⊤), (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤
Tactic: by_cases h : τ ω = ⊤
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ι)) ∨ τ ω = ⊤
⊢ (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤
have neg : ∀ (h : ¬τ ω = ⊤), (∃ (x : ℕ), τ ω ≤ (↑(seq x) : WithTop ι)) ∨ τ ω = ⊤
Tactic: by_cases h : τ ω = ⊤
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 ι)) ∨ τ ω = ⊤
have neg : ∀ (t : ι), (∃ (x : ℕ), (↑t : WithTop ι) ≤ (↑(seq x) : WithTop ι)) ∨ (↑t : WithTop ι) = ⊤
Tactic: lift τ ω to ι using h with t
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
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 : ι
⊢ (∃ (x : ℕ), (↑t : WithTop ι) ≤ (↑(seq x) : WithTop ι)) ∨ (↑t : WithTop ι) = ⊤
have neg : ∃ (x : ℕ), t ≤ seq x
Tactic: simp only [coe_le_coe, coe_ne_top, or_false]