awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.HittingTime
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 :
  ∀ (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
⊢ 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:
ext x
-- Module: Mathlib.Probability.Process.HittingTime
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 : Ω
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
⊢ 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:
simp only [Set.mem_setOf_eq, gt_iff_lt, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff,
      exists_and_left, exists_prop]

Premises used: Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, exists_and_left, Set.mem_setOf_eq, exists_prop, gt_iff_lt
-- Module: Mathlib.Probability.Process.HittingTime
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 : Ω
⊢ τ x ≤ (↑N : WithTop ι)

Tactic:
specialize hτbdd x
-- Module: Mathlib.Probability.Process.HittingTime
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 : τ x = ⊤
⊢ False

Tactic:
simp [h] at hτbdd
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
⊢ τ x ≠ ⊤

Tactic:
have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd
-- Module: Mathlib.Probability.Process.HittingTime
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 ≠ ⊤
⊢ τ x ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Process.HittingTime
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 ≠ ⊤
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
⊢ 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:
lift τ x to ι using h_top with t
-- Module: Mathlib.Probability.Process.HittingTime
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 : Ω
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:
simp [← or_and_right, le_or_gt]

Premises used: le_or_gt, or_and_right
-- Module: Mathlib.Probability.Process.HittingTime
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})

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]
-- Module: Mathlib.Probability.Process.HittingTime
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})
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
⊢ Eq.{u_1 + 1} (α := Set Ω)
    (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∅

Tactic:
ext x
-- Module: Mathlib.Probability.Process.HittingTime
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 : Ω
h : ∀ (x_1 : ι), n < x_1 → τ x = (↑x_1 : WithTop ι) → n < hittingBtwn u s x_1 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

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]

Premises used: not_le, iff_false, Set.mem_inter_iff, Set.mem_iUnion, not_exists, Set.mem_setOf_eq, exists_prop, gt_iff_lt, Set.mem_empty_iff_false, not_and
-- Module: Mathlib.Probability.Process.HittingTime
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

Tactic:
fun m hm hτ ↦ hm.trans_le <| le_hittingBtwn ?_ x

Premises used: MeasureTheory.le_hittingBtwn, LT.lt.trans_le
-- Module: Mathlib.Probability.Process.HittingTime
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 : Ω
h : ∀ (m : ι) (hm : n < m) (hτ : τ x = (↑m : WithTop ι)), m ≤ N
⊢ ∀ (x_1 : ι), n < x_1 → τ x = (↑x_1 : WithTop ι) → n < hittingBtwn u s x_1 N x

Tactic:
refine fun m hm hτ ↦ hm.trans_le <| le_hittingBtwn ?_ x
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
⊢ τ x ≤ (↑N : WithTop ι)

Tactic:
specialize hτbdd x
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
h : τ x = ⊤
⊢ False

Tactic:
simp [h] at hτbdd
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
⊢ τ x ≠ ⊤

Tactic:
have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
h_top : τ x ≠ ⊤
⊢ τ x ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
h_top : τ x ≠ ⊤
h : ∀ (t : ι) (hτ : (↑t : WithTop ι) = (↑m : WithTop ι)) (hτbdd : (↑t : WithTop ι) ≤ (↑N : WithTop ι)), m ≤ N
⊢ m ≤ N

Tactic:
lift τ x to ι using h_top with t
-- Module: Mathlib.Probability.Process.HittingTime
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
t : ι
hτ : (↑t : WithTop ι) = (↑m : WithTop ι)
hτbdd : (↑t : WithTop ι) ≤ (↑N : WithTop ι)
⊢ (↑m : WithTop ι) ≤ (↑N : WithTop ι)

Tactic:
rw [hτ] at hτbdd
-- Module: Mathlib.Probability.Process.HittingTime
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
t : ι
hτ : (↑t : WithTop ι) = (↑m : WithTop ι)
hτbdd : (↑m : WithTop ι) ≤ (↑N : WithTop ι)
⊢ m ≤ N

Tactic:
mod_cast hτbdd

Premises used: WithTop.coe_le_coe._simp_1, cast
-- Module: Mathlib.Probability.Process.HittingTime
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
t : ι
hτ : (↑t : WithTop ι) = (↑m : WithTop ι)
hτbdd : (↑m : WithTop ι) ≤ (↑N : WithTop ι)
⊢ m ≤ N

Tactic:
exact mod_cast hτbdd
-- Module: Mathlib.Probability.Process.HittingTime
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}) ∅

Tactic:
have h₂ : ⋃ i > n, {x | τ x = i} ∩ {x | hittingBtwn u s i N x ≤ n} = ∅ := by
    ext x
    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]
    refine fun m hm hτ ↦ hm.trans_le <| le_hittingBtwn ?_ x
    specialize hτbdd x
    have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd
    lift τ x to ι using h_top with t
    rw [hτ] at hτbdd
    exact mod_cast hτbdd
-- Module: Mathlib.Probability.Process.HittingTime
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})
h₂ :
  Eq.{u_1 + 1} (α := Set Ω)
    (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∅
simp :
  MeasurableSet.{u_1} (α := Ω)
    (⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (x : Ω) ↦ (↑(hittingBtwn u s (τ x).untopA N x) : WithTop ι)) ω ≤ (↑n : WithTop ι)}

Tactic:
simp only [WithTop.coe_le_coe, h₁, h₂, Set.union_empty]

Premises used: Set.union_empty, WithTop.coe_le_coe
-- Module: Mathlib.Probability.Process.HittingTime
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})
h₂ :
  Eq.{u_1 + 1} (α := Set Ω)
    (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∅
⊢ MeasurableSet.{u_1} (α := Ω)
    (⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})

Tactic:
MeasurableSet.iUnion fun i => MeasurableSet.iUnion fun hi =>
    (f.mono hi _ (hτ.measurableSet_eq i)).inter ?_

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_eq, WithTop.some, MeasureTheory.Filtration.mono, MeasurableSet.iUnion, Eq, MeasurableSet.inter