awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
⊢ Tendsto (fun (m : ℕ) ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))
have refine_3 : Tendsto (fun (m : ℕ) ↦ X m (0, ω)) atTop (𝓝 (Function.uncurry u (0, ω)))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
refine_3 : Tendsto (fun (m : ℕ) ↦ X m (0, ω)) atTop (𝓝 (Function.uncurry u (0, ω)))
⊢ Tendsto (fun (m : ℕ) ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))
have refine_3₁ : ∀ (n : ℕ), Tendsto (fun (m : ℕ) ↦ X m (n + 1, ω)) atTop (𝓝 (Function.uncurry u (n + 1, ω)))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
⊢ ({ toFun := Y m, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : (a : ℕ × Ω) → E) (n, ω) = X m (n, ω)
have simp : Y m (n, ω) = X m (n, ω)
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
⊢ EventuallyEq.{0, u_3} (β := E) atTop
    (fun (n_1 : ℕ) ↦
      ((fun (m_1 : ℕ) ↦
              ({ toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
            n_1 :
          (a : ℕ × Ω) → E)
        (n, ω))
    fun (m : ℕ) ↦ X m (n, ω)
have h₁ : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n ≤ x) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                Eq.{u_3 + 1} (α := E)
                  ((fun (n_1 : ℕ) ↦
                      (((fun (m_1 : ℕ) ↦
                                ({ toFun := Y m_1, measurableSet_fiber' := sorry, finite_range' := sorry } :
                                  SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
                              n_1 :
                            (a : ℕ × Ω) → E)
                          (n, ω) :
                        E))
                    x)
                  ((fun (m : ℕ) ↦ X m (n, ω)) x))
              x}
          x}
    a
Tactic: filter_upwards [eventually_ge_atTop n] with m hm using by simp; grind
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n ≤ x) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq.{u_3 + 1} (α := E)
                    ((fun (n_1 : ℕ) ↦
                        (((fun (m_1 : ℕ) ↦
                                  ({ toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } :
                                    SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
                                n_1 :
                              (a : ℕ × Ω) → E)
                            (n, ω) :
                          E))
                      x)
                    ((fun (m : ℕ) ↦ X m (n, ω)) x))
                x}
            x}
      a
⊢ EventuallyEq.{0, u_3} (β := E) atTop
    (fun (n_1 : ℕ) ↦
      ((fun (m_1 : ℕ) ↦
              ({ toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
            n_1 :
          (a : ℕ × Ω) → E)
        (n, ω))
    fun (m : ℕ) ↦ X m (n, ω)
have h₂ : ∀ (a : ℕ),
  n ≤ a → ({ toFun := Y a, measurableSet_fiber' := sorry, finite_range' := sorry } : (a : ℕ × Ω) → E) (n, ω) = X a (n, ω)
Tactic: filter_upwards [eventually_ge_atTop n] with m hm using by simp; grind
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have pos : ∀ (hi_min : IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: by_cases hi_min : IsMin i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
pos : ∀ (hi_min : IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have neg : ∀ (hi_min : ¬IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: by_cases hi_min : IsMin i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) ∅
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have pos : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
Tactic: suffices {ω : Ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
have pos : ∀ (ω : Ω), Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ Membership.mem (γ := Set Ω) ∅ ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ Membership.mem (γ := Set Ω) ∅ ω
have pos : ¬τ ω < (↑i : WithTop ι)
Tactic: simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
ω : Ω
⊢ ¬τ ω < (↑i : WithTop ι)
have pos : ∀ (hi_min : ∀ (b : ι), ¬b < i) (ω : Ω), ¬τ ω < (↑i : WithTop ι)
Tactic: rw [isMin_iff_forall_not_lt] at hi_min
Cleared hypotheses: hi_min, ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ∀ (b : ι), ¬b < i
ω : Ω
⊢ ¬τ ω < (↑i : WithTop ι)
have pos : ∀ (x : WithTop ι), ¬x < (↑i : WithTop ι)
Tactic: cases τ ω with
    | top => simp
    | coe t => exact mod_cast hi_min t
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
⊢ {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ ω ∈ τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
t : ι
⊢ (↑t : WithTop ι) < (↑i : WithTop ι) ↔ (↑t : WithTop ι) ≤ (↑(Order.pred i) : WithTop ι)
have h : t < i ↔ t ≤ Order.pred i
Tactic: simp only [coe_lt_coe, coe_le_coe]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
t : ι
⊢ t < i ↔ t ≤ Order.pred i
have h : t < i ↔ t < i
Tactic: rw [le_pred_iff_of_not_isMin hi_min]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
⊢ τ ω < (↑i : WithTop ι) ↔ τ ω ≤ (↑(Order.pred i) : WithTop ι)
have h : ∀ (x : WithTop ι), x < (↑i : WithTop ι) ↔ x ≤ (↑(Order.pred i) : WithTop ι)
Tactic: cases τ ω with
    | top => simp
    | coe t =>
      simp only [coe_lt_coe, coe_le_coe]
      rw [le_pred_iff_of_not_isMin hi_min]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have this : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
Tactic: have : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iic (pred i : ι) := by
    ext ω
    push _ ∈ _
    cases τ ω with
    | top => simp
    | coe t =>
      simp only [coe_lt_coe, coe_le_coe]
      rw [le_pred_iff_of_not_isMin hi_min]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have neg : MeasurableSet (τ ⁻¹' Set.Iic (↑(Order.pred 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 : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} a ↔
    Membership.mem (γ := Set Ω)
      ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j}) a
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} a ↔
    Membership.mem (γ := Set Ω)
      ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j}) a
have h : τ a = (↑i : WithTop ι) ↔ τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
Tactic: simp only [Set.mem_setOf_eq, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_diff, Set.mem_iUnion, exists_prop, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
⊢ τ a = (↑i : WithTop ι) ↔ τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
have h : τ a = (↑i : WithTop ι) → τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
h : τ a = (↑i : WithTop ι) → τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
⊢ τ a = (↑i : WithTop ι) ↔ τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
have h₁ : (τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x) → τ a = (↑i : WithTop ι)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
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 ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
Tactic: have : {ω | τ ω = i} = {ω | τ ω ≤ i} \ ⋃ (j ∈ Set.range τ) (_ : j < i), {ω | τ ω ≤ j} := by
    ext1 a
    simp only [Set.mem_setOf_eq, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_diff, Set.mem_iUnion, exists_prop, not_exists, not_and]
    constructor <;> intro h
    · simp only [h, lt_iff_le_not_ge, le_refl, and_imp, imp_self, imp_true_iff, and_self_iff]
    · exact h.1.eq_or_lt.resolve_right fun h_lt => h.2 a h_lt le_rfl
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω)
  ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ MeasurableSet.{u_1} (α := Ω)
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
have refine : MeasurableSet.{u_1} (α := Ω) (⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
Tactic: refine (hτ.measurableSet_le i).diff ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
have refine : ∀ j ∈ Set.range τ, MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
Tactic: refine MeasurableSet.biUnion h_countable fun j _ => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
have rw : MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
Tactic: rw [Set.iUnion_eq_if]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
⊢ MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
have pos : ∀ (hji : j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}
Tactic: split_ifs with hji
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
pos : ∀ (hji : j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}
⊢ MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
have neg : ∀ (hji : ¬j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) ∅
Tactic: split_ifs with hji
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
hji : j < (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}
have pos : ∀ (j : ι),
  (↑j : WithTop ι) ∈ Set.range τ →
    ∀ (hji : (↑j : WithTop ι) < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑j : WithTop ι)}
Tactic: lift j to ι using (ne_top_of_lt hji)
Cleared hypotheses: j, h, hji
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
have rw : MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
Tactic: classical
  rw [Set.iUnion_eq_if]
  split_ifs with hji
  · lift j to ι using (ne_top_of_lt hji)
    exact f.mono (mod_cast hji.le) _ (hτ.measurableSet_le j)
  · exact @MeasurableSet.empty _ (f i)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
rw rw₁ rw₂ : MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
have pos : ∀ (hji : j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}
Tactic: classical
  rw [Set.iUnion_eq_if]
  split_ifs with hji
  · lift j to ι using (ne_top_of_lt hji)
    exact f.mono (mod_cast hji.le) _ (hτ.measurableSet_le j)
  · exact @MeasurableSet.empty _ (f i)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
rw rw₁ rw₂ : MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
pos : ∀ (hji : j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
have neg : ∀ (hji : ¬j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) ∅
Tactic: classical
  rw [Set.iUnion_eq_if]
  split_ifs with hji
  · lift j to ι using (ne_top_of_lt hji)
    exact f.mono (mod_cast hji.le) _ (hτ.measurableSet_le j)
  · exact @MeasurableSet.empty _ (f i)