awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), m ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | m ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
have pos : ∀ (h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
  LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
    (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
Tactic: split_ifs with h_n h_m h_m
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
pos :
  ∀ (h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
      (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), m ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | m ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
have neg : ∀ (h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ¬∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
  LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι) ⊤
Tactic: split_ifs with h_n h_m h_m
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
pos :
  ∀ (h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
      (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
neg :
  ∀ (h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ¬∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι) ⊤
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), m ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | m ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
have pos₁ : ∀ (h_n : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
  LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
Tactic: split_ifs with h_n h_m h_m
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
pos :
  ∀ (h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
      (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
neg :
  ∀ (h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ¬∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι) ⊤
pos₁ :
  ∀ (h_n : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s),
    LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), m ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | m ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤)
have neg₁ : ∀ (h_n : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ¬∃ (j : ι), m ≤ j ∧ u j ω ∈ s), LE.le.{u_3} (α := WithTop ι) ⊤ ⊤
Tactic: split_ifs with h_n h_m h_m
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s
⊢ LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
    (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
have pos : LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) (sInf {j : ι | m ≤ j ∧ u j ω ∈ s})
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s
⊢ LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) (sInf {j : ι | m ≤ j ∧ u j ω ∈ s})
have pos : BddBelow.{u_3} (α := ι) {j : ι | n ≤ j ∧ u j ω ∈ s}
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s
⊢ Membership.mem (γ := Set ι) (lowerBounds {j : ι | n ≤ j ∧ u j ω ∈ s}) n
have simp : ∀ (x : ι), n ≤ x → u x ω ∈ s → n ≤ x
Tactic: simp [mem_lowerBounds]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_m : ∃ (j : ι), m ≤ j ∧ u j ω ∈ s
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
have pos : ∀ (t : ι) (ht : m ≤ t ∧ u t ω ∈ s), LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
Tactic: have ⟨t, ht⟩ := h_m
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
have inl : ∀ (hi : n' ≤ i),
  MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
Tactic: rcases le_or_gt n' i with hi | hi
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
inl :
  ∀ (hi : n' ≤ i),
    MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
have inr : ∀ (hi : i < n'),
  MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
Tactic: rcases le_or_gt n' i with hi | hi
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : n' ≤ i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
have h_le : ∀ (ω : Ω), hittingBtwn u s n n' ω ≤ i
Tactic: have h_le : ∀ ω, hittingBtwn u s n n' ω ≤ i := fun x => (hittingBtwn_le x).trans hi
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : i < n'
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingBtwn u s n n' ω ≤ i} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | hittingBtwn u s n n' ω ≤ i} x ↔
    Membership.mem (γ := Set Ω) (⋃ j ∈ Set.Icc n i, u j ⁻¹' s) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : i < n'
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
have h_set_eq_Union : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingBtwn u s n n' ω ≤ i} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)
Tactic: have h_set_eq_Union : {ω | hittingBtwn u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s := by
      ext; simp [hittingBtwn_le_iff_of_lt _ hi]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)} x ↔
    Membership.mem (γ := Set Ω) (⋃ j ∈ Set.Icc n i, u j ⁻¹' s) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)}
have h_set_eq_Union : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)
Tactic: have h_set_eq_Union : {ω | hittingAfter u s n ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s := by
    ext; simp [hittingAfter_le_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ stoppedValue u (fun (ω : Ω) ↦ (↑(hittingBtwn u s n m ω) : WithTop ι)) ω ∈ s
have simp : u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s
Tactic: simp only [stoppedValue, hittingBtwn, if_pos h]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s
have obtain : ∀ (j : ι) (hj₁ : j ∈ Set.Icc n m) (hj₂ : u j ω ∈ s),
  u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s
Tactic: obtain ⟨j, hj₁, hj₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s
have this : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
Tactic: have : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s} :=
    csInf_mem (Set.nonempty_of_mem ⟨hj₁, hj₂⟩)
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n} x ↔
    Membership.mem (γ := Set Ω)
      ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
        ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
x : Ω
⊢ Membership.mem (γ := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n} x ↔
    Membership.mem (γ := Set Ω)
      ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
        ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
      x
have h : hittingBtwn u s (τ x).untopA N x ≤ n ↔
  (∃ (i : ι), τ x = (↑i : WithTop ι) ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨
    ∃ (i : ι), τ x = (↑i : WithTop ι) ∧ n < i ∧ hittingBtwn u s i N x ≤ n
Tactic: simp only [Set.mem_setOf_eq, gt_iff_lt, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff,
      exists_and_left, exists_prop]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
x : Ω
⊢ hittingBtwn u s (τ x).untopA N x ≤ n ↔
    (∃ (i : ι), τ x = (↑i : WithTop ι) ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨
      ∃ (i : ι), τ x = (↑i : WithTop ι) ∧ n < i ∧ hittingBtwn u s i N x ≤ n
have hτbdd₁ : τ x ≤ (↑N : WithTop ι)
Tactic: specialize hτbdd x
Cleared hypotheses: hτbdd
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
x : Ω
hτbdd : τ x ≤ (↑N : WithTop ι)
⊢ hittingBtwn u s (τ x).untopA N x ≤ n ↔
    (∃ (i : ι), τ x = (↑i : WithTop ι) ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨
      ∃ (i : ι), τ x = (↑i : WithTop ι) ∧ n < i ∧ hittingBtwn u s i N x ≤ n
have h_top : τ x ≠ ⊤
Tactic: have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
x : Ω
hτbdd : τ x ≤ (↑N : WithTop ι)
h_top : τ x ≠ ⊤
⊢ hittingBtwn u s (τ x).untopA N x ≤ n ↔
    (∃ (i : ι), τ x = (↑i : WithTop ι) ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨
      ∃ (i : ι), τ x = (↑i : WithTop ι) ∧ n < i ∧ hittingBtwn u s i N x ≤ n
have h : ∀ (t : ι) (hτbdd : (↑t : WithTop ι) ≤ (↑N : WithTop ι)),
  hittingBtwn u s (↑t : WithTop ι).untopA N x ≤ n ↔
    (∃ (i : ι), (↑t : WithTop ι) = (↑i : WithTop ι) ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨
      ∃ (i : ι), (↑t : WithTop ι) = (↑i : WithTop ι) ∧ n < i ∧ hittingBtwn u s i N x ≤ n
Tactic: lift τ x to ι using h_top with t
Cleared hypotheses: hτbdd, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (x : Ω) ↦ (↑(hittingBtwn u s (τ x).untopA N x) : WithTop ι)) ω ≤ (↑n : WithTop ι)}
have h₁ : Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
  ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
    ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
Tactic: have h₁ : {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i ≤ n, {x | τ x = i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i > n, {x | τ x = i} ∩ {x | hittingBtwn u s i N x ≤ n} := by
    ext x
    simp only [Set.mem_setOf_eq, gt_iff_lt, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff,
      exists_and_left, exists_prop]
    specialize hτbdd x
    have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd
    lift τ x to ι using h_top with t
    simp [← or_and_right, le_or_gt]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
h₁ :
  Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
⊢ Eq.{u_1 + 1} (α := Set Ω)
    (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∅
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω)
      (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) x ↔
    Membership.mem (γ := Set Ω) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
h₁ :
  Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
x : Ω
⊢ Membership.mem (γ := Set Ω)
      (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) x ↔
    Membership.mem (γ := Set Ω) ∅ x
have h : ∀ (x_1 : ι), n < x_1 → τ x = (↑x_1 : WithTop ι) → n < hittingBtwn u s x_1 N x
Tactic: simp only [gt_iff_lt, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq, exists_prop,
      Set.mem_empty_iff_false, iff_false, not_exists, not_and, not_le]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
h₁ :
  Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
x : Ω
⊢ ∀ (x_1 : ι), n < x_1 → τ x = (↑x_1 : WithTop ι) → n < hittingBtwn u s x_1 N x
have h : ∀ (m : ι) (hm : n < m) (hτ : τ x = (↑m : WithTop ι)), m ≤ N
Tactic: refine fun m hm hτ ↦ hm.trans_le <| le_hittingBtwn ?_ x
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m_1 : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m_1
u : ι → Ω → β
τ : Ω → WithTop ι
hτ_1 : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
h₁ :
  Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
x : Ω
m : ι
hm : n < m
hτ : τ x = (↑m : WithTop ι)
⊢ m ≤ N
have hτbdd₁ : τ x ≤ (↑N : WithTop ι)
Tactic: specialize hτbdd x
Cleared hypotheses: hτbdd
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m_1 : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m_1
u : ι → Ω → β
τ : Ω → WithTop ι
hτ_1 : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
h₁ :
  Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
x : Ω
m : ι
hm : n < m
hτ : τ x = (↑m : WithTop ι)
hτbdd : τ x ≤ (↑N : WithTop ι)
⊢ m ≤ N
have h_top : τ x ≠ ⊤
Tactic: have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd