-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_le_iff_of_exists [WellFoundedLT ι] {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 mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i)
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω ≤ k

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

Result:
no goals

Proof state:
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
⊢ ∃ k ∈ Set.Icc n (m ⊓ i), u k ω ∈ s

Tactic:
obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'

Result:
case intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i), u k ω ∈ s

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i), u k ω ∈ s

Tactic:
obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists

Result:
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
⊢ ∃ k ∈ Set.Icc n (m ⊓ i), u k ω ∈ s

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

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

Result:
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i), u k ω ∈ s
⊢ hitting u s n m ω ≤ i

Proof state:
case intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (k₁ ⊓ k₂) ω ∈ s

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

Result:
no goals

Proof state:
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i), u k ω ∈ s
⊢ hitting u s n m ω ≤ i

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := h''

Result:
case mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i)
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω ≤ i

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
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:
constructor <;> intro h'

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

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

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

Tactic:
exact ⟨hitting u s n m ω, ⟨le_hitting_of_exists h_exists, h'⟩, hitting_mem_set h_exists⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (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⟩, ?_⟩

Result:
case intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (k₁ ⊓ k₂) ω ∈ s

Proof state:
case mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i)
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω ≤ i

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

Result:
case mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : 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 (m ⊓ i)
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω ≤ k