-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_inter_eq_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i : ι) :
    MeasurableSet[hτ.measurableSpace] (s ∩ {ω | τ ω = i}) ↔
      MeasurableSet[f i] (s ∩ {ω | τ ω = i})

Proof state:
case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
⊢ MeasurableSet (s ∩ {ω | τ ω = i})

Tactic:
intro j

Result:
case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
⊢ MeasurableSet (s ∩ {ω | τ ω = i} ∩ {ω | τ ω ≤ j})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
⊢ MeasurableSet (s ∩ {ω | τ ω = i}) ↔ MeasurableSet (s ∩ {ω | τ ω = i})

Tactic:
constructor <;> intro h

Result:
case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
⊢ MeasurableSet (s ∩ {ω | τ ω = i})

case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
⊢ MeasurableSet (s ∩ {ω | τ ω = i})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
⊢ {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = i} ∩ {ω | τ ω ≤ j} ↔ ω ∈ {ω | τ ω = i} ∩ {_ω | i ≤ j}

Proof state:
case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
⊢ MeasurableSet (s ∩ {ω | τ ω = i} ∩ {ω | τ ω ≤ j})

Tactic:
rw [Set.inter_assoc, this]

Result:
case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
⊢ MeasurableSet (s ∩ ({ω | τ ω = i} ∩ {_ω | i ≤ j}))

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
ω : Ω
hxi : τ ω = i
⊢ τ ω ≤ j ↔ i ≤ j

Tactic:
rw [hxi]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω | τ ω = i})

Tactic:
exact f.mono hij _ h

Result:
no goals

Proof state:
case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
⊢ MeasurableSet (s ∩ ({ω | τ ω = i} ∩ {_ω | i ≤ j}))

Tactic:
by_cases hij : i ≤ j

Result:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = i} ∩ {_ω | i ≤ j}))

case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = i} ∩ {_ω | i ≤ j}))

Proof state:
case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
⊢ MeasurableSet (s ∩ {ω | τ ω = i})

Tactic:
specialize h i

Result:
case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i} ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet (s ∩ {ω | τ ω = i})

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = i} ∩ {ω | τ ω ≤ j} ↔ ω ∈ {ω | τ ω = i} ∩ {_ω | i ≤ j}

Tactic:
simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
ω : Ω
⊢ τ ω = i → (τ ω ≤ j ↔ i ≤ j)

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet (s ∩ {ω | τ ω = i}) ↔ MeasurableSet (s ∩ {ω | τ ω = i})

Tactic:
have : ∀ j, {ω : Ω | τ ω = i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω = i} ∩ {_ω | i ≤ j} := by
  intro j
  ext1 ω
  simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]
  intro hxi
  rw [hxi]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
⊢ MeasurableSet (s ∩ {ω | τ ω = i}) ↔ MeasurableSet (s ∩ {ω | τ ω = i})

Proof state:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = i} ∩ {_ω | i ≤ j}))

Tactic:
simp [hij]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = i} ∩ {_ω | i ≤ j}))

Tactic:
simp only [hij, Set.setOf_true, Set.inter_univ]

Result:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω | τ ω = i})