-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_le_iff_of_lt [WellFoundedLT ι] {m : ι} (i : ι) (hi : i < m) :
    hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
simp_rw [hitting, if_neg h_exists]

Result:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∀ 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⟩

Result:
no goals

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
push_neg at h_exists

Result:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∀ j ∈ Set.Icc n m, u j ω ∉ s
⊢ m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
⊢ hitting 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

Result:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∀ j ∈ Set.Icc n m, u j ω ∉ 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]

Result:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∀ j ∈ Set.Icc n m, u j ω ∉ s
⊢ ∀ (x : ι), n ≤ x → x ≤ i → u x ω ∉ s

Proof state:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
rw [hitting_le_iff_of_exists h_exists]

Result:
no goals