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₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
rw : sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
hc : ∃ j ∈ Set.Icc n m₂, 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₂

Tactic:
rw [if_pos]

Premises used: 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
ht : BddBelow (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
hs : (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}).Nonempty
⊢ 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 β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ BddBelow (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})

Tactic:
bddBelow_Icc.inter_of_left

Premises used: BddBelow.inter_of_left, bddBelow_Icc
-- 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}).Nonempty

Tactic:
⟨j, hj₁, hj₂⟩

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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ BddBelow (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})

Tactic:
exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩]

Premises used: BddBelow.inter_of_left, bddBelow_Icc
-- 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
refine : sInf (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}) = sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})

Tactic:
refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])

Premises used: le_antisymm
-- 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})

Tactic:
le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => ?_

Premises used: Set.Icc_subset_Icc_right, le_csInf, 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₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
refine : ∀ (i : ι) (hi : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}), sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})

Tactic:
refine le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => ?_
-- 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
i : ι
hi : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}
pos : ∀ (hi' : i ≤ m₁), sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
neg : ∀ (hi' : ¬i ≤ m₁), sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i

Tactic:
by_cases hi' : i ≤ m₁
-- 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₂
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₁
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i

Tactic:
csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩

Premises used: BddBelow.inter_of_left, And.right, And.left, 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 : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
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₁
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i

Tactic:
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩

Premises used: BddBelow.inter_of_left, And.right, And.left, 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 : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
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₁
⊢ Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} j

Tactic:
change j ∈ {i | u i ω ∈ s} at hj₂
-- 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
i : ι
hi : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}
hi' : ¬i ≤ m₁
hj₂ : Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} j
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i

Tactic:
((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans hj₁.2).trans (le_of_not_ge hi')

Premises used: BddBelow.inter_of_left, le_of_not_ge, And.right, And.intro, bddBelow_Icc, LE.le.trans, csInf_le
-- 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
i : ι
hi : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}
hi' : ¬i ≤ m₁
hj₂ : Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} j
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i

Tactic:
exact ((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans hj₁.2).trans (le_of_not_ge hi')

Premises used: BddBelow.inter_of_left, le_of_not_ge, And.right, And.intro, bddBelow_Icc, LE.le.trans, csInf_le
-- 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₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ ∃ j ∈ Set.Icc n m₂, u j ω ∈ s

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

Premises used: And.right, And.left, And.intro, Exists.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 : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ ∃ j ∈ Set.Icc n m₂, u j ω ∈ s

Tactic:
exact ⟨j, ⟨hj₁.1, hj₁.2.trans h⟩, hj₂⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
simp :
  (if ∃ j ∈ Set.Icc n m, u j ω ∈ F then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) else m) ≤
    if ∃ j ∈ Set.Icc n m, u j ω ∈ E then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E}) else m
⊢ LE.le.{u_3} (α := (fun (a : Ω) ↦ ι) ω) ((fun (x : Set β) ↦ hittingBtwn u x n m) F ω)
    ((fun (x : Set β) ↦ hittingBtwn u x n m) E ω)

Tactic:
simp only [hittingBtwn_def]

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

Tactic:
split_ifs with hF hE hE
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
pos : BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ F})
pos₁ : ∀ (a : ι), E ⊆ F
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})

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

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 : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → n ≤ x

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
a : ι
⊢ E ⊆ F

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

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

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

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 : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ F
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → n ≤ x

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ F
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ 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 : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
pos : ∀ (t : ι) (ht : t ∈ Set.Icc n m ∧ u t ω ∈ E), m ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
⊢ m ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})

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

Tactic:
absurd ⟨t, ht.1, hEF ht.2⟩ hF

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

Tactic:
exact absurd ⟨t, ht.1, hEF ht.2⟩ hF

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ m ≤ m

Tactic:
simp
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
pos :
  ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι)
      (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
neg :
  ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι) ⊤
pos₁ :
  ∀ (hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
neg₁ : ∀ (hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E), LE.le.{u_3} (α := WithTop ι) ⊤ ⊤
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ F then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ F}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ E then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ E}) : WithTop ι) else ⊤)

Tactic:
split_ifs with hF hE hE
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
pos : LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) (sInf {j : ι | n ≤ j ∧ u j ω ∈ E})
⊢ LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι)
    (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
pos : BddBelow.{u_3} (α := ι) {j : ι | n ≤ j ∧ u j ω ∈ F}
pos₁ : ∀ (a : ι), n ≤ a → E ⊆ F
⊢ LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) (sInf {j : ι | n ≤ j ∧ u j ω ∈ E})

Tactic:
gcongr
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
simp : ∀ (x : ι), Membership.mem (γ := Set ι) {j : ι | n ≤ j ∧ u j ω ∈ F} x → n ≤ x
⊢ Membership.mem (γ := Set ι) (lowerBounds {j : ι | n ≤ j ∧ u j ω ∈ F}) n

Tactic:
simp only [mem_lowerBounds]

Premises used: mem_lowerBounds
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ ∀ (x : ι), Membership.mem (γ := Set ι) {j : ι | n ≤ j ∧ u j ω ∈ F} x → n ≤ x

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
a : ι
h : n ≤ a
⊢ E ⊆ F

Tactic:
hEF
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ BddBelow.{u_3} (α := ι) {j : ι | n ≤ j ∧ u j ω ∈ F}

Tactic:
exacts [⟨n, by simp only [mem_lowerBounds]; grind⟩, hEF]
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι) ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
pos :
  ∀ (t : ι) (ht : n ≤ t ∧ u t ω ∈ E), LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)

Tactic:
obtain ⟨t, ht⟩ := hE
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F
t : ι
ht : n ≤ t ∧ u t ω ∈ E
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)

Tactic:
absurd ⟨t, ht.1, hEF ht.2⟩ hF

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F
t : ι
ht : n ≤ t ∧ u t ω ∈ E
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)

Tactic:
exact absurd ⟨t, ht.1, hEF ht.2⟩ hF

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ 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 : ι → Ω → β
n m : ι
ω : Ω
⊢ Antitone.{u_2, u_3} (β := ι) fun (x : Set β) ↦ hittingBtwn u x n m ω

Tactic:
fun _ _ hEF ↦ hittingBtwn_anti u n m hEF ω

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

Tactic:
fun _ _ hst ↦ hittingAfter_anti u n hst ω

Premises used: Antitone, MeasureTheory.hittingAfter_anti
-- 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₂
pos :
  ∀ (h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s),
    LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
neg :
  ∀ (h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s),
    LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
⊢ LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)

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 m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)

Tactic:
(hittingBtwn_eq_hittingBtwn_of_exists hm h).le

Premises used: Eq.le, MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
-- 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
⊢ LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)

Tactic:
exact (hittingBtwn_eq_hittingBtwn_of_exists hm h).le

Premises used: Eq.le, MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
-- 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
neg : 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 (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)

Tactic:
simp_rw [hittingBtwn, if_neg h]

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

Tactic:
le_csInf ⟨j, hj₁, hj₂⟩ ?_

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

Tactic:
refine le_csInf ⟨j, hj₁, hj₂⟩ ?_