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 k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
simp_rw : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ k
⊢ hittingBtwn u s n m ω ≤ k

Tactic:
simp_rw [hittingBtwn, if_pos hexists]

Premises used: MeasureTheory.hittingBtwn, if_pos
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ k

Tactic:
csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩

Premises used: BddBelow.inter_of_left, LT.lt.le, And.intro, MeasureTheory.hittingBtwn_le, bddBelow_Icc, csInf_le, le_trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ k

Tactic:
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩

Premises used: BddBelow.inter_of_left, LT.lt.le, And.intro, MeasureTheory.hittingBtwn_le, bddBelow_Icc, csInf_le, le_trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
intro : ∀ (h : u k ω ∈ s), False
intro₁ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), False
intro₂ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), hittingBtwn u s n m ω ≤ k
intro₃ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ k
⊢ u k ω ∉ s

Tactic:
classical
  intro h
  have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
  refine not_le.2 hk₁ ?_
  simp_rw [hittingBtwn, if_pos hexists]
  exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩

Premises used: not_le, Iff.mpr, MeasureTheory.hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : (↑k : WithTop ι) < hittingAfter u s n ω
hk₂ : n ≤ k
⊢ u k ω ∉ s

Tactic:
fun h ↦ not_le.2 hk₁ ?_

Premises used: not_le, Iff.mpr, Not
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : (↑k : WithTop ι) < hittingAfter u s n ω
hk₂ : n ≤ k
refine : ∀ (h : u k ω ∈ s), hittingAfter u s n ω ≤ (↑k : WithTop ι)
⊢ u k ω ∉ s

Tactic:
refine fun h ↦ not_le.2 hk₁ ?_

Premises used: not_le, Iff.mpr
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : (↑k : WithTop ι) < hittingAfter u s n ω
hk₂ : n ≤ k
h : u k ω ∈ s
rw : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) ≤ (↑k : WithTop ι)
⊢ hittingAfter u s n ω ≤ (↑k : WithTop ι)

Tactic:
rw [hittingAfter, if_pos ⟨k, hk₂, h⟩]

Premises used: MeasureTheory.hittingAfter, if_pos
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : (↑k : WithTop ι) < hittingAfter u s n ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) ≤ (↑k : WithTop ι)

Tactic:
exact_mod_cast csInf_le bddBelow_Ici.inter_of_left ⟨hk₂, h⟩

Premises used: bddBelow_Ici, BddBelow.inter_of_left, And.intro, csInf_le
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
rw :
  (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) = m ↔
    (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
rw₁ rw₂ :
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m ↔
    (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
⊢ hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m

Tactic:
rw [hittingBtwn, ite_eq_right_iff]

Premises used: MeasureTheory.hittingBtwn, ite_eq_right_iff
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
rw :
  (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) = m ↔
    (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
rw₁ rw₂ :
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m ↔
    (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
⊢ hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m

Tactic:
classical
  rw [hittingBtwn, ite_eq_right_iff]

Premises used: MeasureTheory.hittingBtwn, ite_eq_right_iff
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
⊢ hittingAfter u s n ω = ⊤ ↔ ∀ (j : ι), n ≤ j → u j ω ∉ s

Tactic:
simp [hittingAfter]

Premises used: MeasureTheory.hittingAfter
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
hmn : m ≤ n
inl : ∀ (hmn : m ≤ m), hittingBtwn u s m m ω = m
inr : ∀ (h : m < n), hittingBtwn u s n m ω = m
⊢ hittingBtwn u s n m ω = m

Tactic:
obtain rfl | h := le_iff_eq_or_lt.1 hmn

Premises used: le_iff_eq_or_lt, Iff.mp, rfl
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
inl : ∀ (x : ι) (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
⊢ hittingBtwn u s m m ω = m

Tactic:
rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]

Premises used: forall_exists_index, MeasureTheory.hittingBtwn, ite_eq_right_iff
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x : ι
rw : m ≤ x → x ≤ m → u x ω ∈ s → sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
| ∀ (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m

Tactic:
rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]

Premises used: Set.Icc_self, and_imp, Set.mem_Icc
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
inl : ∀ (x : ι), m ≤ x → x ≤ m → u x ω ∈ s → sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
⊢ ∀ (x : ι) (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m

Tactic:
conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]

Premises used: Set.Icc_self, and_imp, Set.mem_Icc
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
inl : Subset (α := Set ι) {m} {i : ι | u i ω ∈ s}
⊢ sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m

Tactic:
rw [Set.inter_eq_left.2, csInf_singleton]

Premises used: Set.inter_eq_left, Iff.mpr, csInf_singleton
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ Subset (α := Set ι) {m} {i : ι | u i ω ∈ s}

Tactic:
Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)

Premises used: Iff.mpr, Set.singleton_subset_iff, Eq.rec, le_antisymm
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ Subset (α := Set ι) {m} {i : ι | u i ω ∈ s}

Tactic:
exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)

Premises used: Iff.mpr, Set.singleton_subset_iff
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
inl : (if ∃ j ∈ Set.Icc m m, u j ω ∈ s then sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) else m) = m
inl₁ : (∃ j ∈ Set.Icc m m, u j ω ∈ s) → sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
inl₂ inl₃ inl₄ : ∀ (x : ι) (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
inl₅ inl₆ : ∀ (i : ι) (hi₁ : m ≤ i) (hi₂ : i ≤ m) (hi : u i ω ∈ s), sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
inl₇ : ∀ (i : ι) (hi₁ : m ≤ i) (hi₂ : i ≤ m) (hi : u i ω ∈ s), Subset (α := Set ι) {m} {i : ι | u i ω ∈ s}
⊢ hittingBtwn u s m m ω = m

Tactic:
classical
    rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
    conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
    intro i hi₁ hi₂ hi
    rw [Set.inter_eq_left.2, csInf_singleton]
    exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)

Premises used: Set.inter_eq_left, Iff.mpr, Set.singleton_subset_iff, Set.Icc_self, csInf_singleton, and_imp, forall_exists_index, MeasureTheory.hittingBtwn, ite_eq_right_iff, Set.mem_Icc
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
hmn : m ≤ n
h : m < n
⊢ hittingBtwn u s n m ω = m

Tactic:
hittingBtwn_of_lt h

Premises used: MeasureTheory.hittingBtwn_of_lt
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
hmn : m ≤ n
h : m < n
⊢ hittingBtwn u s n m ω = m

Tactic:
exact hittingBtwn_of_lt h

Premises used: MeasureTheory.hittingBtwn_of_lt
-- 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
ω : Ω
simp : n ≤ if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m
⊢ n ≤ hittingBtwn u s n m ω

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 β
n m : ι
hnm : n ≤ m
ω : Ω
pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), n ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
neg : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), n ≤ m
⊢ n ≤ 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
-- 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 : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})

Tactic:
le_csInf ?_ fun b hb => ?_

Premises used: le_csInf
-- 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 : ∃ j ∈ Set.Icc n m, u j ω ∈ s
pos : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
pos₁ : ∀ (b : ι) (hb : b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}), n ≤ b
⊢ n ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})

Tactic:
refine le_csInf ?_ fun b hb => ?_

Premises used: le_csInf
-- 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 : ∃ j ∈ Set.Icc n m, u j ω ∈ s
pos : ∀ (k : ι) (hk_Icc : k ∈ Set.Icc n m) (hk_s : u k ω ∈ s), (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
obtain ⟨k, hk_Icc, hk_s⟩ := h
-- 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
ω : Ω
k : ι
hk_Icc : k ∈ Set.Icc n m
hk_s : u k ω ∈ s
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
⟨k, hk_Icc, hk_s⟩

Premises used: Set.Nonempty, 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 : ι
hnm : n ≤ m
ω : Ω
k : ι
hk_Icc : k ∈ Set.Icc n m
hk_s : u k ω ∈ s
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
exact ⟨k, hk_Icc, hk_s⟩
-- 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 : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
⊢ b ∈ Set.Icc n m ∧ Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} b

Tactic:
rw [Set.mem_inter_iff] at hb

Premises used: Set.mem_inter_iff
-- 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 : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∧ Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} b
⊢ n ≤ b

Tactic:
hb.1.1

Premises used: And.left
-- 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 : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∧ Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} b
⊢ n ≤ b

Tactic:
exact hb.1.1

Premises used: And.left
-- 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 : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m

Tactic:
hnm
-- 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 : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m

Tactic:
exact hnm
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
pos : ∀ (h : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s), (↑n : WithTop ι) ≤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
neg : ∀ (h : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s), (↑n : WithTop ι) ≤ ⊤
⊢ (↑n : WithTop ι) ≤ if ∃ (j : ι), n ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
h : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ (↑n : WithTop ι) ≤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)

Tactic:
exact_mod_cast le_csInf h fun b hb => hb.1

Premises used: le_csInf, And.left
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
h : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ (↑n : 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 : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ hittingBtwn u s n m ω

Tactic:
le_hittingBtwn ?_ ω

Premises used: MeasureTheory.le_hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
refine : n ≤ m
⊢ n ≤ hittingBtwn u s n m ω

Tactic:
refine le_hittingBtwn ?_ ω

Premises used: MeasureTheory.le_hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
by_contra : ∀ (h : ¬n ≤ m), False
⊢ n ≤ m

Tactic:
by_contra h
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h : ¬n ≤ m
⊢ ∃ (j : ι), Membership.mem (γ := Set ι) ∅ j ∧ u j ω ∈ s

Tactic:
rw [Set.Icc_eq_empty_of_lt (not_le.mp h)] at h_exists

Premises used: not_le, Set.Icc_eq_empty_of_lt, Iff.mp
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h : ¬n ≤ m
h_exists₁ : ∃ (j : ι), Membership.mem (γ := Set ι) ∅ j ∧ u j ω ∈ s
⊢ ¬n ≤ m

Tactic:
rw [Set.Icc_eq_empty_of_lt (not_le.mp h)] at h_exists

Premises used: not_le, Set.Icc_eq_empty_of_lt, Iff.mp
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ (j : ι), Membership.mem (γ := Set ι) ∅ j ∧ u j ω ∈ s
h : ¬n ≤ m
⊢ False

Tactic:
simp at h_exists
-- 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
ω : Ω
⊢ hittingBtwn u s n m ω ∈ Set.Icc n m

Tactic:
⟨le_hittingBtwn hnm ω, hittingBtwn_le ω⟩

Premises used: Set.Mem, setOf, MeasureTheory.le_hittingBtwn, Set.Icc, And.intro, MeasureTheory.hittingBtwn_le
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
simp_rw : u (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
simp_rw [hittingBtwn, if_pos h_exists]

Premises used: MeasureTheory.hittingBtwn, if_pos
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
obtain : ∀ (k : ι) (hk₁ : k ∈ Set.Icc n m) (hk₂ : u k ω ∈ s), (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := h_exists
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m k : ι
hk₁ : k ∈ Set.Icc n m
hk₂ : u k ω ∈ s
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
⟨k, Set.mem_inter hk₁ hk₂⟩

Premises used: Set.mem_inter, Set.Nonempty, Exists.intro
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m k : ι
hk₁ : k ∈ Set.Icc n m
hk₂ : u k ω ∈ s
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
exact ⟨k, Set.mem_inter hk₁ hk₂⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
have h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty := by
    obtain ⟨k, hk₁, hk₂⟩ := h_exists
    exact ⟨k, Set.mem_inter hk₁ hk₂⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}

Tactic:
have h_mem := csInf_mem h_nonempty
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
h_mem : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∧
    Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}))

Tactic:
rw [Set.mem_inter_iff] at h_mem

Premises used: Set.mem_inter_iff
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
h_mem :
  sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∧
    Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}))
⊢ u (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) ω ∈ s

Tactic:
h_mem.2

Premises used: Set.Mem, setOf, And.right
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
h_mem :
  sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∧
    Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}))
⊢ u (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) ω ∈ s

Tactic:
exact h_mem.2

Premises used: And.right
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
rw : u (WithTop.untopA (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι)) ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
rw [hittingAfter, if_pos h_exists]

Premises used: MeasureTheory.hittingAfter, if_pos
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
obtain : ∀ (k : ι) (hk₁ : n ≤ k) (hk₂ : u k ω ∈ s), Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
⊢ Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := h_exists
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
k : ι
hk₁ : n ≤ k
hk₂ : u k ω ∈ s
⊢ Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}

Tactic:
⟨k, Set.mem_inter hk₁ hk₂⟩

Premises used: Set.mem_inter, Set.Nonempty, Exists.intro