awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
have rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)}
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) < τ ω}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ
Tactic: have : {ω : Ω | i < τ ω} = {ω : Ω | τ ω ≤ i}ᶜ := by ext1 ω; simp
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
Tactic: rw [← Set.univ_inter {ω | τ ω = i}, measurableSet_inter_eq_iff, Set.univ_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω}) ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω}) ω
have h : (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω
Tactic: simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
a : ι
⊢ (↑i : WithTop ι) < (↑a : WithTop ι) ∨ (↑i : WithTop ι) = (↑a : WithTop ι) ↔
    (↑a : WithTop ι) = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < (↑a : WithTop ι)
have h : i < a ∨ i = a ↔ a = i ∨ i < a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
a : ι
⊢ i < a ∨ i = a ↔ a = i ∨ i < a
have h : i < a ∨ a = i ↔ a = i ∨ i < a
Tactic: rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
a : ι
h : i < a ∨ a = i ↔ a = i ∨ i < a
⊢ i < a ∨ i = a ↔ a = i ∨ i < a
have h₁ : a = i ∨ i < a ↔ a = i ∨ i < a
Tactic: rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω
have h : ∀ (x : WithTop ι), (↑i : WithTop ι) < x ∨ (↑i : WithTop ι) = x ↔ x = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < x
Tactic: cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
  ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
Tactic: have : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω} := by
    ext1 ω
    simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
    cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
have rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)}) ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
  ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
Tactic: have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
Tactic: rw [← Set.univ_inter {ω | τ ω = i}, measurableSet_inter_eq_iff, Set.univ_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω}) ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω}) ω
have h : (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω
Tactic: simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
a : ι
⊢ (↑i : WithTop ι) < (↑a : WithTop ι) ∨ (↑i : WithTop ι) = (↑a : WithTop ι) ↔
    (↑a : WithTop ι) = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < (↑a : WithTop ι)
have h : i < a ∨ i = a ↔ a = i ∨ i < a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
a : ι
⊢ i < a ∨ i = a ↔ a = i ∨ i < a
have h : i < a ∨ a = i ↔ a = i ∨ i < a
Tactic: rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
a : ι
h : i < a ∨ a = i ↔ a = i ∨ i < a
⊢ i < a ∨ i = a ↔ a = i ∨ i < a
have h₁ : a = i ∨ i < a ↔ a = i ∨ i < a
Tactic: rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω
have h : ∀ (x : WithTop ι), (↑i : WithTop ι) < x ∨ (↑i : WithTop ι) = x ↔ x = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < x
Tactic: cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
  ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
Tactic: have : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω} := by
    ext1 ω
    simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
    cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
have rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)}) ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
  ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
Tactic: have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
⊢ Measurable τ
have refine : ∀ (i : WithTop ι), MeasurableSet (τ ⁻¹' Set.Iic i)
Tactic: refine measurable_of_Iic fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
i : WithTop ι
⊢ MeasurableSet (τ ⁻¹' Set.Iic i)
have top : MeasurableSet (τ ⁻¹' Set.Iic ⊤)
Tactic: cases i with
  | top => simp
  | coe i => exact hτ.measurableSet_le' i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
i : WithTop ι
top : MeasurableSet (τ ⁻¹' Set.Iic ⊤)
⊢ MeasurableSet (τ ⁻¹' Set.Iic i)
have coe : ∀ (i : ι), MeasurableSet (τ ⁻¹' Set.Iic (↑i : WithTop ι))
Tactic: cases i with
  | top => simp
  | coe i => exact hτ.measurableSet_le' i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace
have refine_1 : sorry.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
refine_1 : ⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace
have refine_2 : hτ.measurableSpace ⊓ hπ.measurableSpace ≤ sorry.measurableSpace
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
i : WithTop ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i}) ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})) →
    MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)})
have this : ∀ (i : WithTop ι), Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})
Tactic: have : ∀ i, {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i} := by
      intro i; ext1 ω; simp
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
this :
  ∀ (i : WithTop ι), Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})
⊢ ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})) →
    MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)})
have refine_2 : ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})) ∧
    MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})) →
  MeasurableSet s ∧
    ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∪ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
Tactic: simp_rw [this, Set.inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
have rw : MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
Tactic: rw [measurableSpace_min hτ hπ]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i
have rw : hτ.measurableSpace ⊓ sorry.measurableSpace = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i
Tactic: rw [hτ.measurableSpace_min (isStoppingTime_const _ i), measurableSpace_const]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
rw : hτ.measurableSpace ⊓ ⋯.measurableSpace = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i
have rw₁ : hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i
Tactic: rw [hτ.measurableSpace_min (isStoppingTime_const _ i), measurableSpace_const]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
have rw : MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
Tactic: rw [measurableSpace_min_const hτ]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
have hs₁ : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: simp_rw [IsStoppingTime.measurableSet] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : WithTop ι
⊢ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
    s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
have h : ∀ (ω : Ω),
  ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : WithTop ι
ω : Ω
⊢ ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
have pos : ∀ (hτi : τ ω ≤ i),
  ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
Tactic: by_cases hτi : τ ω ≤ i