awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
pos : ∀ (i : ι) (hi₁ : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) (hi₂ : i < m₁), False
⊢ ∀ b ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}, m₁ ≤ b

Tactic:
by_contra! ⟨i, hi₁, hi₂⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
i : ι
hi₁ : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}
hi₂ : i < m₁
⊢ False

Tactic:
h ⟨i, ⟨hi₁.1.1, hi₂.le⟩, hi₁.2⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
i : ι
hi₁ : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}
hi₂ : i < m₁
⊢ False

Tactic:
exact h ⟨i, ⟨hi₁.1.1, hi₂.le⟩, hi₁.2⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ¬∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ m₂

Tactic:
hm
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ¬∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ m₂

Tactic:
exact hm
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
simp :
  (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤
    if ∃ j ∈ Set.Icc n' m, u j ω ∈ s then sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s}) else m
⊢ LE.le.{u_3} (α := (fun (a : Ω) ↦ ι) ω) ((fun (x : ι) ↦ hittingBtwn u s x m) n ω)
    ((fun (x : ι) ↦ hittingBtwn u s x m) n' ω)

Tactic:
simp only [hittingBtwn]

Premises used: MeasureTheory.hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
pos :
  ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
neg :
  ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
pos₁ :
  ∀ (h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s),
    m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
neg₁ : ∀ (h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s), m ≤ m
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤
    if ∃ j ∈ Set.Icc n' m, u j ω ∈ s then sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s}) else m

Tactic:
split_ifs with h_n h_n' h_n'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
pos : BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})

Tactic:
gcongr
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
simp : ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x
⊢ n ∈ lowerBounds (Set.Icc n m ∩ {i : ι | u i ω ∈ s})

Tactic:
simp [mem_lowerBounds]

Premises used: mem_lowerBounds
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ s})

Tactic:
exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
neg : ∀ (t : ι) (ht : t ∈ Set.Icc n m ∧ u t ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m

Tactic:
obtain ⟨t, ht⟩ := h_n
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ s
simp : ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x
⊢ n ∈ lowerBounds (Set.Icc n m ∩ {i : ι | u i ω ∈ s})

Tactic:
simp [mem_lowerBounds]

Premises used: mem_lowerBounds
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ s
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m

Tactic:
exact csInf_le_of_le ⟨n, by simp [mem_lowerBounds]; grind⟩ ht ht.1.2

Premises used: csInf_le_of_le, And.right, And.left, Exists.intro
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
pos : ∀ (t : ι) (ht : t ∈ Set.Icc n' m ∧ u t ω ∈ s), m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
⊢ m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})

Tactic:
have ⟨t, ht⟩ := h_n'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
t : ι
ht : t ∈ Set.Icc n' m ∧ u t ω ∈ s
⊢ m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})

Tactic:
absurd ⟨t, ⟨hnn'.trans ht.1.1, ht.1.2⟩, ht.2⟩ h_n

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
t : ι
ht : t ∈ Set.Icc n' m ∧ u t ω ∈ s
⊢ m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})

Tactic:
exact absurd ⟨t, ⟨hnn'.trans ht.1.1, ht.1.2⟩, ht.2⟩ h_n

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ m ≤ m

Tactic:
simp
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
neg₁ : ∀ (h_n : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s) (h_m : ¬∃ (j : ι), m ≤ j ∧ u j ω ∈ s), LE.le.{u_3} (α := 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 ⊤)

Tactic:
split_ifs with h_n h_m h_m
-- Module: Mathlib.Probability.Process.HittingTime
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
pos : LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) (sInf {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:
norm_cast
-- Module: Mathlib.Probability.Process.HittingTime
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
pos : BddBelow.{u_3} (α := ι) {j : ι | n ≤ j ∧ u j ω ∈ s}
⊢ LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) (sInf {j : ι | m ≤ j ∧ u j ω ∈ s})

Tactic:
gcongr
-- Module: Mathlib.Probability.Process.HittingTime
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
simp : ∀ (x : ι), n ≤ x → u x ω ∈ s → n ≤ x
⊢ Membership.mem (γ := Set ι) (lowerBounds {j : ι | n ≤ j ∧ u j ω ∈ s}) n

Tactic:
simp [mem_lowerBounds]

Premises used: mem_lowerBounds
-- Module: Mathlib.Probability.Process.HittingTime
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
⊢ ∀ (x : ι), n ≤ x → u x ω ∈ s → n ≤ x

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
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
⊢ BddBelow.{u_3} (α := ι) {j : ι | n ≤ j ∧ u j ω ∈ s}

Tactic:
exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]
-- Module: Mathlib.Probability.Process.HittingTime
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 ι) ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Process.HittingTime
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
pos :
  ∀ (t : ι) (ht : m ≤ t ∧ u t ω ∈ s), LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)

Tactic:
have ⟨t, ht⟩ := h_m
-- Module: Mathlib.Probability.Process.HittingTime
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
t : ι
ht : m ≤ t ∧ u t ω ∈ s
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)

Tactic:
absurd ⟨t, hnm.trans ht.1, ht.2⟩ h_n

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
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
t : ι
ht : m ≤ t ∧ u t ω ∈ s
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | m ≤ j ∧ u j ω ∈ s}) : WithTop ι)

Tactic:
exact absurd ⟨t, hnm.trans ht.1, ht.2⟩ h_n

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
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 ι) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
⊢ Monotone (β := ι) fun (x : ι) ↦ hittingBtwn u s n x ω

Tactic:
fun _ _ hnn' ↦ hittingBtwn_mono_right u s n hnn'

Premises used: Monotone, MeasureTheory.hittingBtwn_mono_right
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m : ι
ω : Ω
⊢ Monotone (β := ι) fun (x : ι) ↦ hittingBtwn u s x m ω

Tactic:
fun _ _ hnn' ↦ hittingBtwn_mono_left u s m hnn' ω

Premises used: MeasureTheory.hittingBtwn_mono_left, Monotone
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
⊢ Monotone (β := WithTop ι) fun (x : ι) ↦ hittingAfter u s x ω

Tactic:
fun _ _ hnm ↦ hittingAfter_mono u s hnm ω

Premises used: MeasureTheory.hittingAfter_mono, Monotone
-- 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 ι
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 ι)}
inr :
  ∀ (hi : i < n'),
    MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}

Tactic:
rcases le_or_gt n' i with hi | hi

Premises used: 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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : n' ≤ i
⊢ ∀ (ω : Ω), hittingBtwn u s n n' ω ≤ i

Tactic:
have h_le : ∀ ω, hittingBtwn u s n n' ω ≤ i := fun x => (hittingBtwn_le x).trans hi
-- 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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : n' ≤ i
h_le : ∀ (ω : Ω), hittingBtwn u s n n' ω ≤ i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}

Tactic:
simp [h_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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : i < n'
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | hittingBtwn u s n n' ω ≤ i} x ↔
      Membership.mem (γ := Set Ω) (⋃ j ∈ Set.Icc n i, u j ⁻¹' s) x
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingBtwn u s n n' ω ≤ i} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)

Tactic:
ext
-- 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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : i < n'
x_1 : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | hittingBtwn u s n n' ω ≤ i} x_1 ↔
    Membership.mem (γ := Set Ω) (⋃ j ∈ Set.Icc n i, u j ⁻¹' s) x_1

Tactic:
simp [hittingBtwn_le_iff_of_lt _ hi]

Premises used: MeasureTheory.hittingBtwn_le_iff_of_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 ι
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)

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]
-- 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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
hi : i < n'
h_set_eq_Union : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingBtwn u s n n' ω ≤ i} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ (↑(hittingBtwn u s n n' ω) : WithTop ι)) ω ≤ (↑i : WithTop ι)}

Tactic:
simpa [h_set_eq_Union] using MeasurableSet.iUnion fun j =>
      MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j) hs)

Premises used: Set.preimage, MeasureTheory.Filtration.mono, MeasurableSet.iUnion
-- 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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)} x ↔
      Membership.mem (γ := Set Ω) (⋃ j ∈ Set.Icc n i, u j ⁻¹' s) x
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)

Tactic:
ext
-- 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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
x_1 : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)} x_1 ↔
    Membership.mem (γ := Set Ω) (⋃ j ∈ Set.Icc n i, u j ⁻¹' s) x_1

Tactic:
simp [hittingAfter_le_iff]

Premises used: MeasureTheory.hittingAfter_le_iff
-- 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 ι
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)

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]
-- 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 ι
x : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted (β := fun (i : ι) ↦ β) f u
hs : MeasurableSet s
i : ι
h_set_eq_Union :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)} (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | hittingAfter u s n ω ≤ (↑i : WithTop ι)}

Tactic:
simpa [h_set_eq_Union] using MeasurableSet.iUnion fun j =>
    MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j) hs)

Premises used: Set.preimage, MeasureTheory.Filtration.mono, MeasurableSet.iUnion
-- Module: Mathlib.Probability.Process.HittingTime
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
simp : u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s
⊢ stoppedValue u (fun (ω : Ω) ↦ (↑(hittingBtwn u s n m ω) : WithTop ι)) ω ∈ s

Tactic:
simp only [stoppedValue, hittingBtwn, if_pos h]

Premises used: MeasureTheory.stoppedValue, MeasureTheory.hittingBtwn, if_pos
-- Module: Mathlib.Probability.Process.HittingTime
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
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
⊢ u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h
-- Module: Mathlib.Probability.Process.HittingTime
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
⊢ 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₂⟩)
-- Module: Mathlib.Probability.Process.HittingTime
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
this : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
⊢ u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s

Tactic:
this.2

Premises used: Set.Mem, setOf, And.right, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.Probability.Process.HittingTime
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
this : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
⊢ u (↑(sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) : WithTop ι).untopA ω ∈ s

Tactic:
exact this.2

Premises used: And.right