-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_mono {m₁ m₂ : ι} (hm : m₁ ≤ m₂) : hitting u s n m₁ ω ≤ hitting u s n m₂ ω

Proof state:
case pos.intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
i : ι
hi₁ : i ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}
hi₂ : i < m₁
⊢ False

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

Result:
no goals

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ¬∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ m₂

Tactic:
exact hm

Result:
no goals

Proof state:
case neg
Ω : 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
⊢ 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'

Result:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ¬∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ m₂

Proof state:
case pos.intro.intro
Ω : 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
hneg : ∃ b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}, b < m₁
⊢ False

Tactic:
obtain ⟨i, hi₁, hi₂⟩ := hneg

Result:
case pos.intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
i : ι
hi₁ : i ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}
hi₂ : i < m₁
⊢ False

Proof state:
case pos.intro.intro
Ω : 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
⊢ ∀ b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}, m₁ ≤ b

Tactic:
by_contra hneg

Result:
case pos.intro.intro
Ω : 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
hneg : ¬∀ b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}, m₁ ≤ b
⊢ False

Proof state:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

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

Result:
case pos.intro.intro
Ω : 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})

Proof state:
case neg
Ω : 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
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω

Tactic:
simp_rw [hitting, if_neg h]

Result:
case neg
Ω : 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
⊢ m₁ ≤ if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s}) else m₂

Proof state:
case pos.intro.intro
Ω : 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
hneg : ¬∀ b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}, m₁ ≤ b
⊢ False

Tactic:
push_neg at hneg

Result:
case pos.intro.intro
Ω : 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
hneg : ∃ b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}, b < m₁
⊢ False

Proof state:
case pos
Ω : 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
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω

Tactic:
exact (hitting_eq_hitting_of_exists hm h).le

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω

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

Result:
case pos
Ω : 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
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω

case neg
Ω : 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
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω

Proof state:
case pos.intro.intro
Ω : 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:
refine le_csInf ⟨j, hj₁, hj₂⟩ ?_

Result:
case pos.intro.intro
Ω : 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
⊢ ∀ b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}, m₁ ≤ b