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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∀ (j : ι) (_ : j ∈ Set.Icc n m), u j ω ∉ s
neg : ∀ (x : ι), n ≤ x → x ≤ i → u x ω ∉ s
⊢ m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
simp only [not_le.mpr hi, Set.mem_Icc, false_iff, not_exists, not_and, and_imp]

Premises used: not_le, Iff.mpr, and_imp, not_exists, false_iff, Set.mem_Icc, not_and
-- 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 i : ι
hi : i < m
h_exists : ∀ (j : ι) (_ : j ∈ Set.Icc n m), u j ω ∉ s
⊢ ∀ (x : ι), n ≤ x → x ≤ i → u x ω ∉ s

Tactic:
fun k hkn hki => h_exists k ⟨hkn, hki.trans hi.le⟩

Premises used: LT.lt.le, And.intro, LE.le.trans
-- 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 i : ι
hi : i < m
h_exists : ∀ (j : ι) (_ : j ∈ Set.Icc n m), u j ω ∉ s
⊢ ∀ (x : ι), n ≤ x → x ≤ i → u x ω ∉ s

Tactic:
exact fun k hkn hki => h_exists k ⟨hkn, hki.trans hi.le⟩

Premises used: And.intro
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
mp : hittingBtwn u s n m ω < i → ∃ j ∈ Set.Ico n i, u j ω ∈ s
mpr : (∃ j ∈ Set.Ico n i, u j ω ∈ s) → hittingBtwn u s n m ω < i
⊢ hittingBtwn u s n m ω < i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
constructor
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
by_contra : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), False
⊢ ∃ j ∈ Set.Icc n m, u j ω ∈ s

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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ ¬i ≤ m

Tactic:
simp_rw [hittingBtwn, if_neg h, ← not_le] at h'

Premises used: not_le, MeasureTheory.hittingBtwn, if_neg
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ¬i ≤ m
⊢ False

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

Tactic:
exact h' hi
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
⊢ ∃ j ∈ Set.Icc n m, u j ω ∈ s

Tactic:
have h : ∃ j ∈ Set.Icc n m, u j ω ∈ s := by
      by_contra h
      simp_rw [hittingBtwn, if_neg h, ← not_le] at h'
      exact h' hi
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n < i

Tactic:
have hni : n < i := (le_hittingBtwn_of_exists h).trans_lt h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
⊢ n ≤ hittingBtwn u s n m ω

Tactic:
have h_le := le_hittingBtwn (u := u) (s := s) (hni.le.trans hi) ω
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
mp :
  ∀ (h' : ∃ b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}, b < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
    (h_le : n ≤ hittingBtwn u s n m ω), ∃ j ∈ Set.Ico n i, u j ω ∈ s
mp₁ :
  ∀ (h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
    (h_le : n ≤ hittingBtwn u s n m ω), BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
mp₂ :
  ∀ (h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
    (h_le : n ≤ hittingBtwn u s n m ω), (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
rw [hittingBtwn, if_pos h, csInf_lt_iff] at h'

Premises used: csInf_lt_iff, 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 i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
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 β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∀ (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 β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ s})

Tactic:
exact ⟨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 i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
h

Premises used: Set.Mem, setOf, Set.inter, Set.Nonempty
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
exact h
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}, b < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∃ (b : ι), ((n ≤ b ∧ b ≤ m) ∧ u b ω ∈ s) ∧ b < i

Tactic:
simp only [Set.mem_inter_iff, Set.mem_Icc, Set.mem_setOf_eq] at h'

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, 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 i : ι
hi : i ≤ m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
h' : ∃ (b : ι), ((n ≤ b ∧ b ≤ m) ∧ u b ω ∈ s) ∧ b < i
mp : ∀ (j : ι) (hji : j < i) (hj_mem : u j ω ∈ s) (hnj : n ≤ j) (hjm : j ≤ m), ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
obtain ⟨j, ⟨⟨hnj, hjm⟩, hj_mem⟩, hji⟩ := h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
j : ι
hji : j < i
hj_mem : u j ω ∈ s
hnj : n ≤ j
hjm : j ≤ m
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
⟨j, ⟨hnj, hji⟩, hj_mem⟩

Premises used: 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 i : ι
hi : i ≤ m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
j : ι
hji : j < i
hj_mem : u j ω ∈ s
hnj : n ≤ j
hjm : j ≤ m
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
exact ⟨j, ⟨hnj, hji⟩, hj_mem⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ j ∈ Set.Ico n i, u j ω ∈ s
mpr : ∀ (k : ι) (hk₁ : k ∈ Set.Ico n i) (hk₂ : u k ω ∈ s), hittingBtwn u s n m ω < i
⊢ hittingBtwn u s n m ω < i

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
k : ι
hk₁ : k ∈ Set.Ico n i
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω < i

Tactic:
lt_of_le_of_lt ?_ hk₁.2

Premises used: lt_of_le_of_lt, And.right
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
k : ι
hk₁ : k ∈ Set.Ico n i
hk₂ : u k ω ∈ s
mpr : hittingBtwn u s n m ω ≤ k
⊢ hittingBtwn u s n m ω < i

Tactic:
refine lt_of_le_of_lt ?_ hk₁.2

Premises used: lt_of_le_of_lt, And.right
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
k : ι
hk₁ : k ∈ Set.Ico n i
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ k

Tactic:
hittingBtwn_le_of_mem hk₁.1 (hk₁.2.le.trans hi) hk₂

Premises used: MeasureTheory.hittingBtwn_le_of_mem, LT.lt.le, And.right, And.left, 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 i : ι
hi : i ≤ m
k : ι
hk₁ : k ∈ Set.Ico n i
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ k

Tactic:
exact hittingBtwn_le_of_mem hk₁.1 (hk₁.2.le.trans hi) hk₂

Premises used: MeasureTheory.hittingBtwn_le_of_mem, LT.lt.le, And.right, And.left, LE.le.trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
mp : hittingAfter u s n ω < (↑i : WithTop ι) → ∃ j ∈ Set.Ico n i, u j ω ∈ s
mpr : (∃ j ∈ Set.Ico n i, u j ω ∈ s) → hittingAfter u s n ω < (↑i : WithTop ι)
⊢ hittingAfter u s n ω < (↑i : WithTop ι) ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
constructor
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h : hittingAfter u s n ω = ⊤
⊢ False

Tactic:
simp [h] at h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
⊢ hittingAfter u s n ω ≠ ⊤

Tactic:
have h_top : hittingAfter u s n ω ≠ ⊤ := fun h ↦ by simp [h] at h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
⊢ ¬∀ (j : ι), n ≤ j → u j ω ∉ s

Tactic:
rw [ne_eq, hittingAfter_eq_top_iff] at h_top

Premises used: MeasureTheory.hittingAfter_eq_top_iff, ne_eq
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : ¬∀ (j : ι), n ≤ j → u j ω ∉ s
⊢ ∃ (j : ι), n ≤ j ∧ u j ω ∈ s

Tactic:
push Not at h_top

Premises used: Not
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ ∃ (j : ι), n ≤ j ∧ u j ω ∈ s

Tactic:
h_top
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ ∃ (j : ι), n ≤ j ∧ u j ω ∈ s

Tactic:
exact h_top
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
⊢ ∃ (j : ι), n ≤ j ∧ u j ω ∈ s

Tactic:
have h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s := by
      rw [ne_eq, hittingAfter_eq_top_iff] at h_top
      push Not at h_top
      exact h_top
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ (↑n : WithTop ι) ≤ hittingAfter u s n ω

Tactic:
have h_le := le_hittingAfter (u := u) (s := s) (n := n) ω
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) < (↑i : WithTop ι)

Tactic:
rw [hittingAfter, if_pos h_exists] at 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 i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h'₁ : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) < (↑i : WithTop ι)
⊢ hittingAfter u s n ω ≠ ⊤

Tactic:
rw [hittingAfter, if_pos h_exists] at 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 i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h'₁ : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) < (↑i : WithTop ι)
h_top₁ : hittingAfter u s n ω ≠ ⊤
⊢ ∃ (j : ι), n ≤ j ∧ u j ω ∈ s

Tactic:
rw [hittingAfter, if_pos h_exists] at 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 i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h'₁ : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) < (↑i : WithTop ι)
h_top₁ : hittingAfter u s n ω ≠ ⊤
h_exists₁ : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ (↑n : WithTop ι) ≤ hittingAfter u s n ω

Tactic:
rw [hittingAfter, if_pos h_exists] at 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 i : ι
ω : Ω
h' : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i

Tactic:
norm_cast at h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
mp : ∀ (h' : ∃ (b : ι), Membership.mem (γ := Set ι) {i : ι | n ≤ i ∧ u i ω ∈ s} b ∧ b < i), ∃ j ∈ Set.Ico n i, u j ω ∈ s
mp₁ : BddBelow.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
mp₂ : Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
rw [csInf_lt_iff] at h'

Premises used: csInf_lt_iff
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
simp : ∀ (x : ι), n ≤ x → u x ω ∈ s → n ≤ x
⊢ Membership.mem (γ := Set ι) (lowerBounds {i : ι | n ≤ i ∧ u i ω ∈ 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 i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
⊢ ∀ (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 i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
⊢ BddBelow.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}

Tactic:
exact ⟨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 i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
⊢ Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}

Tactic:
h_exists

Premises used: Set.Mem, setOf, Set.Nonempty
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
⊢ Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}

Tactic:
exact h_exists
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : ∃ (b : ι), (n ≤ b ∧ u b ω ∈ s) ∧ b < i
mp : ∀ (j : ι) (hj₁ : n ≤ j ∧ u j ω ∈ s) (hj₂ : j < i), ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
j : ι
hj₁ : n ≤ j ∧ u j ω ∈ s
hj₂ : j < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
⟨j, ⟨hj₁.1, hj₂⟩, hj₁.2⟩

Premises used: 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 i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
j : ι
hj₁ : n ≤ j ∧ u j ω ∈ s
hj₂ : j < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
exact ⟨j, ⟨hj₁.1, hj₂⟩, hj₁.2⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : ∃ j ∈ Set.Ico n i, u j ω ∈ s
mpr : ∀ (j : ι) (hj₁ : j ∈ Set.Ico n i) (hj₂ : u j ω ∈ s), hittingAfter u s n ω < (↑i : WithTop ι)
⊢ hittingAfter u s n ω < (↑i : WithTop ι)

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Ico n i
hj₂ : u j ω ∈ s
⊢ hittingAfter u s n ω < (↑i : WithTop ι)

Tactic:
lt_of_le_of_lt ?_ (mod_cast hj₁.2 : (j : WithTop ι) < i)

Premises used: lt_of_le_of_lt, cast, WithTop.coe_lt_coe._simp_1, And.right, Eq.symm
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Ico n i
hj₂ : u j ω ∈ s
mpr : hittingAfter u s n ω ≤ (↑j : WithTop ι)
⊢ hittingAfter u s n ω < (↑i : WithTop ι)

Tactic:
refine lt_of_le_of_lt ?_ (mod_cast hj₁.2 : (j : WithTop ι) < i)

Premises used: lt_of_le_of_lt, cast, WithTop.coe_lt_coe._simp_1, And.right, Eq.symm
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Ico n i
hj₂ : u j ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑j : WithTop ι)

Tactic:
hittingAfter_le_of_mem hj₁.1 hj₂

Premises used: And.left, MeasureTheory.hittingAfter_le_of_mem
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Ico n i
hj₂ : u j ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑j : WithTop ι)

Tactic:
exact hittingAfter_le_of_mem hj₁.1 hj₂

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

Tactic:
simp only [hittingBtwn, if_pos h']

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₁ m₂ : ι
h : m₁ ≤ m₂
h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
obtain :
  ∀ (j : ι) (hj₁ : j ∈ Set.Icc n m₁) (hj₂ : u j ω ∈ s),
    sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) =
      if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) else m₂
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) =
    if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) else m₂

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h'