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 ι
k : ι
hk₁ : n ≤ k
hk₂ : u k ω ∈ s
⊢ Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}

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 ι
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}

Tactic:
have h_nonempty : {i : ι | n ≤ 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 ι
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_nonempty : Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
⊢ u (WithTop.untopA (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι)) ω ∈ s

Tactic:
(csInf_mem h_nonempty).2

Premises used: csInf_mem, Set.Mem, And.right, WithTop.untopD, WithTop.recTopCoe
-- 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
h_nonempty : Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
⊢ u (WithTop.untopA (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι)) ω ∈ s

Tactic:
exact (csInf_mem h_nonempty).2

Premises used: csInf_mem, 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 : ι
hl : hittingBtwn u s n m ω < m
pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), u (hittingBtwn u s n m ω) ω ∈ s
neg : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), u (hittingBtwn u s n m ω) ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
by_cases h : ∃ j ∈ Set.Icc n m, u j ω ∈ s

Premises used: Set.Icc
-- 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 : ι
hl : hittingBtwn u s n m ω < m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
hittingBtwn_mem_set h

Premises used: MeasureTheory.hittingBtwn_mem_set
-- 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 : ι
hl : hittingBtwn u s n m ω < m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
exact hittingBtwn_mem_set h

Premises used: MeasureTheory.hittingBtwn_mem_set
-- 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 : ι
hl : hittingBtwn u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m < m

Tactic:
simp_rw [hittingBtwn, if_neg h] at hl

Premises used: 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
hl : m < m
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
False.elim (hl.ne rfl)

Premises used: False.elim, rfl, LT.lt.ne
-- 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 : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
hl : m < m
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
exact False.elim (hl.ne rfl)

Premises used: False.elim, rfl, LT.lt.ne
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
hl : hittingAfter u s n ω ≠ ⊤
⊢ ∃ (x : ι) (_ : n ≤ x), u x ω ∈ s

Tactic:
simp only [ne_eq, hittingAfter_eq_top_iff, not_forall, not_not] at hl

Premises used: Classical.not_not, MeasureTheory.hittingAfter_eq_top_iff, ne_eq, Classical.not_forall
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
hl : ∃ (x : ι) (_ : n ≤ x), u x ω ∈ s
obtain : ∀ (j : ι) (hj₁ : n ≤ j) (hj₂ : u j ω ∈ s), u (hittingAfter u s n ω).untopA ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hl
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst_1 : WellFoundedLT ι
j : ι
hj₁ : n ≤ j
hj₂ : u j ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
hittingAfter_mem_set ⟨j, hj₁, hj₂⟩

Premises used: MeasureTheory.hittingAfter_mem_set, 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
j : ι
hj₁ : n ≤ j
hj₂ : u j ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
exact hittingAfter_mem_set ⟨j, hj₁, hj₂⟩

Premises used: MeasureTheory.hittingAfter_mem_set, 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 : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
⊢ ∃ k ∈ Set.Icc n m, u k ω ∈ s

Tactic:
have h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s := ⟨i, ⟨hin, him⟩, his⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
simp_rw : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ i
⊢ hittingBtwn u s n m ω ≤ i

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 i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ i

Tactic:
csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter ⟨hin, him⟩ his)

Premises used: BddBelow.inter_of_left, Set.mem_inter, And.intro, bddBelow_Icc, csInf_le
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ i

Tactic:
exact csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter ⟨hin, him⟩ his)

Premises used: BddBelow.inter_of_left, Set.mem_inter, And.intro, bddBelow_Icc, csInf_le
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
hin : n ≤ i
his : u i ω ∈ s
⊢ ∃ (k : ι), n ≤ k ∧ u k ω ∈ s

Tactic:
have h_exists : ∃ k, n ≤ k ∧ u k ω ∈ s := ⟨i, hin, his⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
hin : n ≤ i
his : u i ω ∈ s
h_exists : ∃ (k : ι), n ≤ k ∧ u k ω ∈ s
rw : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) ≤ (↑i : WithTop ι)
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι)

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 i : ι
ω : Ω
hin : n ≤ i
his : u i ω ∈ s
h_exists : ∃ (k : ι), n ≤ k ∧ u k ω ∈ s
⊢ (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) ≤ (↑i : WithTop ι)

Tactic:
exact_mod_cast csInf_le (BddBelow.inter_of_left bddBelow_Ici) (Set.mem_inter hin his)

Premises used: bddBelow_Ici, BddBelow.inter_of_left, Set.mem_inter, csInf_le
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
mp : hittingBtwn u s n m ω ≤ i → ∃ j ∈ Set.Icc n i, u j ω ∈ s
mpr : (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingBtwn u s n m ω ≤ i
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : hittingBtwn u s n m ω ≤ i
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
⟨hittingBtwn u s n m ω, ⟨le_hittingBtwn_of_exists h_exists, h'⟩,
      hittingBtwn_mem_set h_exists⟩

Premises used: MeasureTheory.hittingBtwn_mem_set, MeasureTheory.hittingBtwn, And.intro, Exists.intro, MeasureTheory.le_hittingBtwn_of_exists
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : hittingBtwn u s n m ω ≤ i
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
exact ⟨hittingBtwn u s n m ω, ⟨le_hittingBtwn_of_exists h_exists, h'⟩,
      hittingBtwn_mem_set h_exists⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
obtain : ∀ (k₁ : ι) (hk₁_mem : k₁ ∈ Set.Icc n m) (hk₁_s : u k₁ ω ∈ s), ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s

Tactic:
obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
obtain : ∀ (k₂ : ι) (hk₂_mem : k₂ ∈ Set.Icc n i) (hk₂_s : u k₂ ω ∈ s), ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s

Tactic:
obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
k₂ : ι
hk₂_mem : k₂ ∈ Set.Icc n i
hk₂_s : u k₂ ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s

Tactic:
⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, ?_⟩

Premises used: le_min, And.right, And.left, And.intro, Exists.intro, Min.min, min_le_min
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
k₂ : ι
hk₂_mem : k₂ ∈ Set.Icc n i
hk₂_s : u k₂ ω ∈ s
refine : u (min k₁ k₂) ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s

Tactic:
refine ⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, ?_⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
k₂ : ι
hk₂_mem : k₂ ∈ Set.Icc n i
hk₂_s : u k₂ ω ∈ s
⊢ u (min k₁ k₂) ω ∈ s

Tactic:
min_rec' (fun j => u j ω ∈ s) hk₁_s hk₂_s

Premises used: Set.Mem, Membership.mem, min_rec'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
k₂ : ι
hk₂_mem : k₂ ∈ Set.Icc n i
hk₂_s : u k₂ ω ∈ s
⊢ u (min k₁ k₂) ω ∈ s

Tactic:
exact min_rec' (fun j => u j ω ∈ s) hk₁_s hk₂_s

Premises used: Membership.mem, min_rec'
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s

Tactic:
have h'' : ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s := by
      obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists
      obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'
      refine ⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, ?_⟩
      exact min_rec' (fun j => u j ω ∈ s) hk₁_s hk₂_s
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
h'' : ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
mpr : ∀ (k : ι) (hk₁ : k ∈ Set.Icc n (min m 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k : ι
hk₁ : k ∈ Set.Icc n (min m i)
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i

Tactic:
le_trans ?_ (hk₁.2.trans (min_le_right _ _))

Premises used: And.right, min_le_right, LE.le.trans, le_trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k : ι
hk₁ : k ∈ Set.Icc n (min m i)
hk₂ : u k ω ∈ s
mpr : hittingBtwn u s n m ω ≤ k
⊢ hittingBtwn u s n m ω ≤ i

Tactic:
refine le_trans ?_ (hk₁.2.trans (min_le_right _ _))

Premises used: And.right, min_le_right, LE.le.trans, le_trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k : ι
hk₁ : k ∈ Set.Icc n (min m i)
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ k

Tactic:
hittingBtwn_le_of_mem hk₁.1 (hk₁.2.trans (min_le_left _ _)) hk₂

Premises used: MeasureTheory.hittingBtwn_le_of_mem, min_le_left, 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k : ι
hk₁ : k ∈ Set.Icc n (min m i)
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ k

Tactic:
exact hittingBtwn_le_of_mem hk₁.1 (hk₁.2.trans (min_le_left _ _)) hk₂

Premises used: MeasureTheory.hittingBtwn_le_of_mem, min_le_left, 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
mp : hittingAfter u s n ω ≤ (↑i : WithTop ι) → ∃ j ∈ Set.Icc n i, u j ω ∈ s
mpr : (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingAfter u s n ω ≤ (↑i : WithTop ι)
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι) ↔ ∃ j ∈ Set.Icc 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
⊢ (↑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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
⟨(hittingAfter u s n ω).untopA, ?_, hittingAfter_mem_set_of_ne_top h_top⟩

Premises used: MeasureTheory.hittingAfter, MeasureTheory.hittingAfter_mem_set_of_ne_top, And.intro, Exists.intro, WithTop.untopA
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
mp : (hittingAfter u s n ω).untopA ∈ Set.Icc n i
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
refine ⟨(hittingAfter u s n ω).untopA, ?_, hittingAfter_mem_set_of_ne_top h_top⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ hittingAfter u s n ω ≠ ⊤

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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
mp :
  ∀ (i' : ι)
    (hittingAfter_le_iff : ∀ [WellFoundedLT ι], (↑i' : WithTop ι) ≤ (↑i : WithTop ι) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s)
    (h' : (↑i' : WithTop ι) ≤ (↑i : WithTop ι)) (h_le : (↑n : WithTop ι) ≤ (↑i' : WithTop ι)),
    (↑i' : WithTop ι).untopA ∈ Set.Icc n i
⊢ (hittingAfter u s n ω).untopA ∈ Set.Icc n i

Tactic:
lift (hittingAfter u s n ω) to ι using h_top with i'

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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
i' : ι
hittingAfter_le_iff : ∀ [WellFoundedLT ι], (↑i' : WithTop ι) ≤ (↑i : WithTop ι) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
h' : (↑i' : WithTop ι) ≤ (↑i : WithTop ι)
h_le : (↑n : WithTop ι) ≤ (↑i' : WithTop ι)
mp mp₁ mp₂ mp₃ : ∀ (h' : i' ≤ i) (h_le : n ≤ i'), (↑i' : WithTop ι).untopA ∈ Set.Icc n i
⊢ (↑i' : WithTop ι).untopA ∈ Set.Icc n i

Tactic:
norm_cast at h' h_le
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
mpr : ∀ (j : ι) (hj₁ : j ∈ Set.Icc 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
j : ι
hj₁ : j ∈ Set.Icc n i
hj₂ : u j ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι)

Tactic:
le_trans ?_ (mod_cast hj₁.2 : (j : WithTop ι) ≤ i)

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

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

Premises used: WithTop.coe_le_coe._simp_1, cast, And.right, Eq.symm, le_trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
j : ι
hj₁ : j ∈ Set.Icc 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
j : ι
hj₁ : j ∈ Set.Icc 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m i : ι
hi : i < m
pos : ∀ (h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
neg : ∀ (h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
by_cases h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s

Premises used: Set.Icc
-- 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 ∈ Set.Icc n m, u j ω ∈ s
pos pos₁ : (∃ j ∈ Set.Icc n i, u j ω ∈ s) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
rw [hittingBtwn_le_iff_of_exists h_exists]

Premises used: MeasureTheory.hittingBtwn_le_iff_of_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 i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
neg : m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
simp_rw [hittingBtwn, if_neg h_exists]

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

Tactic:
push Not at h_exists

Premises used: Not