[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
⊢ hitting u s n m ω = m
[PROOFSTEP]
simp_rw [hitting]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
⊢ (if ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) = m
[PROOFSTEP]
have h_not : ¬∃ (j : ι) (_ : j ∈ Set.Icc n m), u j ω ∈ s :=
  by
  push_neg
  intro j
  rw [Set.Icc_eq_empty_of_lt h]
  simp only [Set.mem_empty_iff_false, IsEmpty.forall_iff]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
⊢ ¬∃ j x, u j ω ∈ s
[PROOFSTEP]
push_neg
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
⊢ ∀ (j : ι), j ∈ Set.Icc n m → ¬u j ω ∈ s
[PROOFSTEP]
intro j
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
j : ι
⊢ j ∈ Set.Icc n m → ¬u j ω ∈ s
[PROOFSTEP]
rw [Set.Icc_eq_empty_of_lt h]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
j : ι
⊢ j ∈ ∅ → ¬u j ω ∈ s
[PROOFSTEP]
simp only [Set.mem_empty_iff_false, IsEmpty.forall_iff]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
h_not : ¬∃ j x, u j ω ∈ s
⊢ (if ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) = m
[PROOFSTEP]
simp only [exists_prop] at h_not 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h : m < n
h_not : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ (if ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) = m
[PROOFSTEP]
simp only [h_not, if_false]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
⊢ hitting u s n m ω ≤ m
[PROOFSTEP]
cases' le_or_lt n m with h_le h_lt
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
h_le : n ≤ m
⊢ hitting u s n m ω ≤ m
[PROOFSTEP]
simp only [hitting]
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
h_le : n ≤ m
⊢ (if ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) ≤ m
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
h_le : n ≤ m
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h
[GOAL]
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
h_le : n ≤ m
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m
[PROOFSTEP]
change j ∈ {i | u i ω ∈ s} at hj₂ 
[GOAL]
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
h_le : n ≤ m
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : j ∈ {i | u i ω ∈ s}
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m
[PROOFSTEP]
exact (csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter hj₁ hj₂)).trans hj₁.2
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
h_le : n ≤ m
h : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ m ≤ m
[PROOFSTEP]
exact le_rfl
[GOAL]
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
ω : Ω
h_lt : m < n
⊢ hitting u s n m ω ≤ m
[PROOFSTEP]
rw [hitting_of_lt h_lt]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
⊢ ¬u k ω ∈ s
[PROOFSTEP]
classical
intro h
have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
refine' ⟨k, ⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩
refine' not_le.2 hk₁ _
simp_rw [hitting, if_pos hexists]
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
⊢ ¬u k ω ∈ s
[PROOFSTEP]
intro h
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ False
[PROOFSTEP]
have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
[GOAL]
case hexists
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ False
[PROOFSTEP]
refine' ⟨k, ⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ False
[PROOFSTEP]
refine' not_le.2 hk₁ _
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ hitting u s n m ω ≤ k
[PROOFSTEP]
simp_rw [hitting, if_pos hexists]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ k
[PROOFSTEP]
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
⊢ hitting u s n m ω = m ↔ (∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s) → sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
rw [hitting, ite_eq_right_iff]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hmn : m ≤ n
⊢ hitting u s n m ω = m
[PROOFSTEP]
obtain rfl | h := le_iff_eq_or_lt.1 hmn
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
m : ι
hmn : m ≤ m
⊢ hitting u s m m ω = m
[PROOFSTEP]
rw [hitting, ite_eq_right_iff, forall_exists_index]
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
m : ι
hmn : m ≤ m
⊢ ∀ (x : ι), x ∈ Set.Icc m m ∧ u x ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
m : ι
hmn : m ≤ m
| ∀ (x : ι), x ∈ Set.Icc m m ∧ u x ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
m : ι
hmn : m ≤ m
| ∀ (x : ι), x ∈ Set.Icc m m ∧ u x ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
m : ι
hmn : m ≤ m
| ∀ (x : ι), x ∈ Set.Icc m m ∧ u x ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
intro
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| x✝ ∈ Set.Icc m m ∧ u x✝ ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
m : ι
hmn : m ≤ m
⊢ ∀ (x : ι), m ≤ x → x ≤ m → u x ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
intro i hi₁ hi₂ hi
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i✝ : ι
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ sInf ({m} ∩ {i | u i ω ∈ s}) = m
[PROOFSTEP]
rw [Set.inter_eq_left_iff_subset.2, csInf_singleton]
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
i✝ : ι
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ {m} ⊆ {i | u i ω ∈ s}
[PROOFSTEP]
exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
[GOAL]
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hmn : m ≤ n
h : m < n
⊢ hitting u s n m ω = m
[PROOFSTEP]
exact hitting_of_lt h
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
⊢ n ≤ hitting u s n m ω
[PROOFSTEP]
simp only [hitting]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
⊢ n ≤ if ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ n ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ s})
[PROOFSTEP]
refine' le_csInf _ fun b hb => _
[GOAL]
case pos.refine'_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ Set.Nonempty (Set.Icc n m ∩ {i | u i ω ∈ s})
[PROOFSTEP]
obtain ⟨k, hk_Icc, hk_s⟩ := h
[GOAL]
case pos.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
k : ι
hk_Icc : k ∈ Set.Icc n m
hk_s : u k ω ∈ s
⊢ Set.Nonempty (Set.Icc n m ∩ {i | u i ω ∈ s})
[PROOFSTEP]
exact ⟨k, hk_Icc, hk_s⟩
[GOAL]
case pos.refine'_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ n ≤ b
[PROOFSTEP]
rw [Set.mem_inter_iff] at hb 
[GOAL]
case pos.refine'_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∧ b ∈ {i | u i ω ∈ s}
⊢ n ≤ b
[PROOFSTEP]
exact hb.1.1
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω✝ : Ω
m : ι
hnm : n ≤ m
ω : Ω
h : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ n ≤ m
[PROOFSTEP]
exact hnm
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ n ≤ hitting u s n m ω
[PROOFSTEP]
refine' le_hitting _ ω
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ n ≤ m
[PROOFSTEP]
by_contra h
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h : ¬n ≤ m
⊢ False
[PROOFSTEP]
rw [Set.Icc_eq_empty_of_lt (not_le.mp h)] at h_exists 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
h_exists : ∃ j, j ∈ ∅ ∧ u j ω ∈ s
h : ¬n ≤ m
⊢ False
[PROOFSTEP]
simp at h_exists 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ u (hitting u s n m ω) ω ∈ s
[PROOFSTEP]
simp_rw [hitting, if_pos h_exists]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
[PROOFSTEP]
have h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty :=
  by
  obtain ⟨k, hk₁, hk₂⟩ := h_exists
  exact ⟨k, Set.mem_inter hk₁ hk₂⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ Set.Nonempty (Set.Icc n m ∩ {i | u i ω ∈ s})
[PROOFSTEP]
obtain ⟨k, hk₁, hk₂⟩ := h_exists
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m k : ι
hk₁ : k ∈ Set.Icc n m
hk₂ : u k ω ∈ s
⊢ Set.Nonempty (Set.Icc n m ∩ {i | u i ω ∈ s})
[PROOFSTEP]
exact ⟨k, Set.mem_inter hk₁ hk₂⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h_nonempty : Set.Nonempty (Set.Icc n m ∩ {i | u i ω ∈ s})
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
[PROOFSTEP]
have h_mem := csInf_mem h_nonempty
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h_nonempty : Set.Nonempty (Set.Icc n m ∩ {i | u i ω ∈ s})
h_mem : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
[PROOFSTEP]
rw [Set.mem_inter_iff] at h_mem 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h_nonempty : Set.Nonempty (Set.Icc n m ∩ {i | u i ω ∈ s})
h_mem : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∧ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
[PROOFSTEP]
exact h_mem.2
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
hl : hitting u s n m ω < m
⊢ u (hitting u s n m ω) ω ∈ s
[PROOFSTEP]
by_cases h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
hl : hitting u s n m ω < m
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ u (hitting u s n m ω) ω ∈ s
[PROOFSTEP]
exact hitting_mem_set h
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
hl : hitting u s n m ω < m
h : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ u (hitting u s n m ω) ω ∈ s
[PROOFSTEP]
simp_rw [hitting, if_neg h] at hl 
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
hl : m < m
⊢ u (hitting u s n m ω) ω ∈ s
[PROOFSTEP]
exact False.elim (hl.ne rfl)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
⊢ hitting u s n m ω ≤ i
[PROOFSTEP]
have h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s := ⟨i, ⟨hin, him⟩, his⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k, k ∈ Set.Icc n m ∧ u k ω ∈ s
⊢ hitting u s n m ω ≤ i
[PROOFSTEP]
simp_rw [hitting, if_pos h_exists]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k, k ∈ Set.Icc n m ∧ u k ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ i
[PROOFSTEP]
exact csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter ⟨hin, him⟩ his)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ hitting u s n m ω ≤ i ↔ ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ hitting u s n m ω ≤ i → ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
intro h'
[GOAL]
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ (∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s) → hitting u s n m ω ≤ i
[PROOFSTEP]
intro h'
[GOAL]
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h' : hitting u s n m ω ≤ i
⊢ ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
exact ⟨hitting u s n m ω, ⟨le_hitting_of_exists h_exists, h'⟩, hitting_mem_set h_exists⟩
[GOAL]
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h' : ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
⊢ hitting u s n m ω ≤ i
[PROOFSTEP]
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
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h' : ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
⊢ ∃ k, k ∈ Set.Icc n (min m i) ∧ u k ω ∈ s
[PROOFSTEP]
obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h' : ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
⊢ ∃ k, k ∈ Set.Icc n (min m i) ∧ u k ω ∈ s
[PROOFSTEP]
obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'
[GOAL]
case intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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, k ∈ Set.Icc n (min m i) ∧ u k ω ∈ s
[PROOFSTEP]
refine' ⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, _⟩
[GOAL]
case intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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
[PROOFSTEP]
exact min_rec' (fun j => u j ω ∈ s) hk₁_s hk₂_s
[GOAL]
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h' : ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
h'' : ∃ k, k ∈ Set.Icc n (min m i) ∧ u k ω ∈ s
⊢ hitting u s n m ω ≤ i
[PROOFSTEP]
obtain ⟨k, hk₁, hk₂⟩ := h''
[GOAL]
case mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h' : ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
k : ι
hk₁ : k ∈ Set.Icc n (min m i)
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω ≤ i
[PROOFSTEP]
refine' le_trans _ (hk₁.2.trans (min_le_right _ _))
[GOAL]
case mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m : ι
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h' : ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
k : ι
hk₁ : k ∈ Set.Icc n (min m i)
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω ≤ k
[PROOFSTEP]
exact hitting_le_of_mem hk₁.1 (hk₁.2.trans (min_le_left _ _)) hk₂
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i < m
⊢ hitting u s n m ω ≤ i ↔ ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
by_cases h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i < m
h_exists : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ hitting u s n m ω ≤ i ↔ ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
rw [hitting_le_iff_of_exists h_exists]
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i < m
h_exists : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ hitting u s n m ω ≤ i ↔ ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
simp_rw [hitting, if_neg h_exists]
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i < m
h_exists : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ m ≤ i ↔ ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
push_neg at h_exists 
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i < m
h_exists : ∀ (j : ι), j ∈ Set.Icc n m → ¬u j ω ∈ s
⊢ m ≤ i ↔ ∃ j, j ∈ Set.Icc n i ∧ u j ω ∈ s
[PROOFSTEP]
simp only [not_le.mpr hi, Set.mem_Icc, false_iff_iff, not_exists, not_and, and_imp]
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i < m
h_exists : ∀ (j : ι), j ∈ Set.Icc n m → ¬u j ω ∈ s
⊢ ∀ (x : ι), n ≤ x → x ≤ i → ¬u x ω ∈ s
[PROOFSTEP]
exact fun k hkn hki => h_exists k ⟨hkn, hki.trans hi.le⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
⊢ hitting u s n m ω < i ↔ ∃ j, j ∈ Set.Ico n i ∧ u j ω ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
⊢ hitting u s n m ω < i → ∃ j, j ∈ Set.Ico n i ∧ u j ω ∈ s
[PROOFSTEP]
intro h'
[GOAL]
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
⊢ (∃ j, j ∈ Set.Ico n i ∧ u j ω ∈ s) → hitting u s n m ω < i
[PROOFSTEP]
intro h'
[GOAL]
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
h' : hitting u s n m ω < i
⊢ ∃ j, j ∈ Set.Ico n i ∧ u j ω ∈ s
[PROOFSTEP]
have h : ∃ j ∈ Set.Icc n m, u j ω ∈ s := by
  by_contra h
  simp_rw [hitting, if_neg h, ← not_le] at h' 
  exact h' hi
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
h' : hitting u s n m ω < i
⊢ ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
[PROOFSTEP]
by_contra h
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
h' : hitting u s n m ω < i
h : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ False
[PROOFSTEP]
simp_rw [hitting, if_neg h, ← not_le] at h' 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
h : ¬∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
h' : ¬i ≤ m
⊢ False
[PROOFSTEP]
exact h' hi
[GOAL]
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
h' : hitting u s n m ω < i
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ ∃ j, j ∈ Set.Ico n i ∧ u j ω ∈ s
[PROOFSTEP]
exact ⟨hitting u s n m ω, ⟨le_hitting_of_exists h, h'⟩, hitting_mem_set h⟩
[GOAL]
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
h' : ∃ j, j ∈ Set.Ico n i ∧ u j ω ∈ s
⊢ hitting u s n m ω < i
[PROOFSTEP]
obtain ⟨k, hk₁, hk₂⟩ := h'
[GOAL]
case mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
k : ι
hk₁ : k ∈ Set.Ico n i
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω < i
[PROOFSTEP]
refine' lt_of_le_of_lt _ hk₁.2
[GOAL]
case mpr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
m i : ι
hi : i ≤ m
k : ι
hk₁ : k ∈ Set.Ico n i
hk₂ : u k ω ∈ s
⊢ hitting u s n m ω ≤ k
[PROOFSTEP]
exact hitting_le_of_mem hk₁.1 (hk₁.2.le.trans hi) hk₂
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
h' : ∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
⊢ hitting u s n m₁ ω = hitting u s n m₂ ω
[PROOFSTEP]
simp only [hitting, if_pos h']
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
h' : ∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) =
    if ∃ j, j ∈ Set.Icc n m₂ ∧ u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s}) else m₂
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h'
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
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}) =
    if ∃ j, j ∈ Set.Icc n m₂ ∧ u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s}) else m₂
[PROOFSTEP]
rw [if_pos]
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
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})
[PROOFSTEP]
refine'
  le_antisymm _
    (csInf_le_csInf bddBelow_Icc.inter_of_left ⟨j, hj₁, hj₂⟩
      (Set.inter_subset_inter_left _ (Set.Icc_subset_Icc_right h)))
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
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})
[PROOFSTEP]
refine' le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => _
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
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}
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) ≤ i
[PROOFSTEP]
by_cases hi' : i ≤ m₁
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
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
[PROOFSTEP]
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
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
[PROOFSTEP]
change j ∈ {i | u i ω ∈ s} at hj₂ 
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
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₂ : j ∈ {i | u i ω ∈ s}
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) ≤ i
[PROOFSTEP]
exact ((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans (hj₁.2.trans le_rfl)).trans (le_of_lt (not_le.1 hi'))
[GOAL]
case intro.intro.hc
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ ∃ j, j ∈ Set.Icc n m₂ ∧ u j ω ∈ s
[PROOFSTEP]
exact ⟨j, ⟨hj₁.1, hj₁.2.trans h⟩, hj₂⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω
[PROOFSTEP]
by_cases h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω
[PROOFSTEP]
exact (hitting_eq_hitting_of_exists hm h).le
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
⊢ hitting u s n m₁ ω ≤ hitting u s n m₂ ω
[PROOFSTEP]
simp_rw [hitting, if_neg h]
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
⊢ m₁ ≤ if ∃ j, j ∈ Set.Icc n m₂ ∧ u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s}) else m₂
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
h' : ∃ j, j ∈ Set.Icc n m₂ ∧ u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h'
[GOAL]
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, 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})
[PROOFSTEP]
refine' le_csInf ⟨j, hj₁, hj₂⟩ _
[GOAL]
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
⊢ ∀ (b : ι), b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s} → m₁ ≤ b
[PROOFSTEP]
by_contra hneg
[GOAL]
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
hneg : ¬∀ (b : ι), b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s} → m₁ ≤ b
⊢ False
[PROOFSTEP]
push_neg at hneg 
[GOAL]
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
hneg : ∃ b, b ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s} ∧ b < m₁
⊢ False
[PROOFSTEP]
obtain ⟨i, hi₁, hi₂⟩ := hneg
[GOAL]
case pos.intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i✝ : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, 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
[PROOFSTEP]
exact h ⟨i, ⟨hi₁.1.1, hi₂.le⟩, hi₁.2⟩
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j, j ∈ Set.Icc n m₁ ∧ u j ω ∈ s
h' : ¬∃ j, j ∈ Set.Icc n m₂ ∧ u j ω ∈ s
⊢ m₁ ≤ m₂
[PROOFSTEP]
exact hm
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
⊢ IsStoppingTime f (hitting u s n n')
[PROOFSTEP]
intro i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
⊢ MeasurableSet {ω | hitting u s n n' ω ≤ i}
[PROOFSTEP]
cases' le_or_lt n' i with hi hi
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : n' ≤ i
⊢ MeasurableSet {ω | hitting u s n n' ω ≤ i}
[PROOFSTEP]
have h_le : ∀ ω, hitting u s n n' ω ≤ i := fun x => (hitting_le x).trans hi
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : n' ≤ i
h_le : ∀ (ω : Ω), hitting u s n n' ω ≤ i
⊢ MeasurableSet {ω | hitting u s n n' ω ≤ i}
[PROOFSTEP]
simp [h_le]
[GOAL]
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
⊢ MeasurableSet {ω | hitting u s n n' ω ≤ i}
[PROOFSTEP]
have h_set_eq_Union : {ω | hitting u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s :=
  by
  ext x
  rw [Set.mem_setOf_eq, hitting_le_iff_of_lt _ hi]
  simp only [Set.mem_Icc, exists_prop, Set.mem_iUnion, Set.mem_preimage]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
⊢ {ω | hitting u s n n' ω ≤ i} = ⋃ (j : ι) (_ : j ∈ Set.Icc n i), u j ⁻¹' s
[PROOFSTEP]
ext x
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
x : Ω
⊢ x ∈ {ω | hitting u s n n' ω ≤ i} ↔ x ∈ ⋃ (j : ι) (_ : j ∈ Set.Icc n i), u j ⁻¹' s
[PROOFSTEP]
rw [Set.mem_setOf_eq, hitting_le_iff_of_lt _ hi]
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
x : Ω
⊢ (∃ j, j ∈ Set.Icc n i ∧ u j x ∈ s) ↔ x ∈ ⋃ (j : ι) (_ : j ∈ Set.Icc n i), u j ⁻¹' s
[PROOFSTEP]
simp only [Set.mem_Icc, exists_prop, Set.mem_iUnion, Set.mem_preimage]
[GOAL]
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
h_set_eq_Union : {ω | hitting u s n n' ω ≤ i} = ⋃ (j : ι) (_ : j ∈ Set.Icc n i), u j ⁻¹' s
⊢ MeasurableSet {ω | hitting u s n n' ω ≤ i}
[PROOFSTEP]
rw [h_set_eq_Union]
[GOAL]
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
h_set_eq_Union : {ω | hitting u s n n' ω ≤ i} = ⋃ (j : ι) (_ : j ∈ Set.Icc n i), u j ⁻¹' s
⊢ MeasurableSet (⋃ (j : ι) (_ : j ∈ Set.Icc n i), u j ⁻¹' s)
[PROOFSTEP]
exact MeasurableSet.iUnion fun j => MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j).measurable hs)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ stoppedValue u (hitting u s n m) ω ∈ s
[PROOFSTEP]
simp only [stoppedValue, hitting, if_pos h]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j, j ∈ Set.Icc n m ∧ u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
[PROOFSTEP]
have : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s} :=
  csInf_mem (Set.nonempty_of_mem ⟨hj₁, hj₂⟩)
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
this : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
[PROOFSTEP]
exact this.2
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
⊢ IsStoppingTime f fun x => hitting u s (τ x) N x
[PROOFSTEP]
intro n
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
⊢ MeasurableSet {ω | (fun x => hitting u s (τ x) N x) ω ≤ n}
[PROOFSTEP]
have h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ i ≤ n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪ ⋃ i > n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} :=
  by
  ext x
  simp [← exists_or, ← or_and_right, le_or_lt]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
⊢ {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
[PROOFSTEP]
ext x
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
x : Ω
⊢ x ∈ {x | hitting u s (τ x) N x ≤ n} ↔
    x ∈
      (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
        ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
[PROOFSTEP]
simp [← exists_or, ← or_and_right, le_or_lt]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
⊢ MeasurableSet {ω | (fun x => hitting u s (τ x) N x) ω ≤ n}
[PROOFSTEP]
have h₂ : ⋃ i > n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅ :=
  by
  ext x
  simp only [gt_iff_lt, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq, exists_prop, Set.mem_empty_iff_false,
    iff_false_iff, not_exists, not_and, not_le]
  rintro m hm rfl
  exact lt_of_lt_of_le hm (le_hitting (hτbdd _) _)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
⊢ ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅
[PROOFSTEP]
ext x
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
x : Ω
⊢ x ∈ ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} ↔ x ∈ ∅
[PROOFSTEP]
simp only [gt_iff_lt, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq, exists_prop, Set.mem_empty_iff_false,
  iff_false_iff, not_exists, not_and, not_le]
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
x : Ω
⊢ ∀ (x_1 : ι), n < x_1 → τ x = x_1 → n < hitting u s x_1 N x
[PROOFSTEP]
rintro m hm rfl
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
x : Ω
hm : n < τ x
⊢ n < hitting u s (τ x) N x
[PROOFSTEP]
exact lt_of_lt_of_le hm (le_hitting (hτbdd _) _)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
h₂ : ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅
⊢ MeasurableSet {ω | (fun x => hitting u s (τ x) N x) ω ≤ n}
[PROOFSTEP]
rw [h₁, h₂, Set.union_empty]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
h₂ : ⋃ (i : ι) (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅
⊢ MeasurableSet (⋃ (i : ι) (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n})
[PROOFSTEP]
exact
  MeasurableSet.iUnion fun i =>
    MeasurableSet.iUnion fun hi => (f.mono hi _ (hτ.measurableSet_eq i)).inter (hitting_isStoppingTime hf hs n)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
f : Filtration ι m
ω : Ω
⊢ hitting u s ⊥ ⊤ ω = sInf {i | u i ω ∈ s}
[PROOFSTEP]
simp only [hitting, Set.mem_Icc, bot_le, le_top, and_self_iff, exists_true_left, Set.Icc_bot, Set.Iic_top,
  Set.univ_inter, ite_eq_left_iff, not_exists]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
f : Filtration ι m
ω : Ω
⊢ (∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)) → ⊤ = sInf {i | u i ω ∈ s}
[PROOFSTEP]
intro h_nmem_s
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
f : Filtration ι m
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ⊤ = sInf {i | u i ω ∈ s}
[PROOFSTEP]
symm
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
f : Filtration ι m
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ sInf {i | u i ω ∈ s} = ⊤
[PROOFSTEP]
rw [sInf_eq_top]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
f : Filtration ι m
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ∀ (a : ι), a ∈ {i | u i ω ∈ s} → a = ⊤
[PROOFSTEP]
simp only [Set.mem_univ, true_and] at h_nmem_s 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
f : Filtration ι m
ω : Ω
h_nmem_s : ∀ (x : ι), ¬u x ω ∈ s
⊢ ∀ (a : ι), a ∈ {i | u i ω ∈ s} → a = ⊤
[PROOFSTEP]
exact fun i hi_mem_s => absurd hi_mem_s (h_nmem_s i)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
f : Filtration ℕ m
i n : ι
ω : Ω
hx : ∃ j, j ≤ n ∧ u j ω ∈ s
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j, j ≤ i ∧ u j ω ∈ s
[PROOFSTEP]
cases' lt_or_le i n with hi hi
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
f : Filtration ℕ m
i n : ι
ω : Ω
hx : ∃ j, j ≤ n ∧ u j ω ∈ s
hi : i < n
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j, j ≤ i ∧ u j ω ∈ s
[PROOFSTEP]
rw [hitting_le_iff_of_lt _ hi]
[GOAL]
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
f : Filtration ℕ m
i n : ι
ω : Ω
hx : ∃ j, j ≤ n ∧ u j ω ∈ s
hi : i < n
⊢ (∃ j, j ∈ Set.Icc ⊥ i ∧ u j ω ∈ s) ↔ ∃ j, j ≤ i ∧ u j ω ∈ s
[PROOFSTEP]
simp
[GOAL]
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
f : Filtration ℕ m
i n : ι
ω : Ω
hx : ∃ j, j ≤ n ∧ u j ω ∈ s
hi : n ≤ i
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j, j ≤ i ∧ u j ω ∈ s
[PROOFSTEP]
simp only [(hitting_le ω).trans hi, true_iff_iff]
[GOAL]
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
f : Filtration ℕ m
i n : ι
ω : Ω
hx : ∃ j, j ≤ n ∧ u j ω ∈ s
hi : n ≤ i
⊢ ∃ j, j ≤ i ∧ u j ω ∈ s
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := hx
[GOAL]
case inr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
u : ι → Ω → β
s : Set β
f : Filtration ℕ m
i n : ι
ω : Ω
hi : n ≤ i
j : ι
hj₁ : j ≤ n
hj₂ : u j ω ∈ s
⊢ ∃ j, j ≤ i ∧ u j ω ∈ s
[PROOFSTEP]
exact ⟨j, hj₁.trans hi, hj₂⟩
