-- Mathlib/Probability/Process/HittingTime.lean
theorem isStoppingTime_hitting_isStoppingTime [ConditionallyCompleteLinearOrder ι]
    [WellFoundedLT ι] [Countable ι] [TopologicalSpace ι] [OrderTopology ι]
    [FirstCountableTopology ι] [TopologicalSpace β] [PseudoMetrizableSpace β] [MeasurableSpace β]
    [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

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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}

Tactic:
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, not_exists, not_and, not_le]
  rintro m hm rfl
  exact lt_of_lt_of_le hm (le_hitting (hτbdd _) _)

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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}

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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}

Tactic:
ext x

Result:
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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}

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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}

Tactic:
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]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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}

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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

Tactic:
intro n

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
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}