-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_le_stopping_time [TopologicalSpace ι] [SecondCountableTopology ι]
    [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] (hτ : IsStoppingTime f τ)
    (hπ : IsStoppingTime f π) : MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ π ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
⊢ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | τ ω ⊓ j ≤ π ω ⊓ j} ∩ {ω | τ ω ≤ j}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
⊢ ω ∈ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} ↔ ω ∈ {ω | τ ω ⊓ j ≤ π ω ⊓ j} ∩ {ω | τ ω ≤ j}

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω ≤ j
⊢ τ ω ≤ π ω ↔ (τ ω ≤ π ω ∨ j ≤ π ω) ∧ (τ ω ≤ j ∨ True)

Tactic:
simp only [h, or_self_iff, and_true]

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω ≤ j
⊢ τ ω ≤ π ω ↔ τ ω ≤ π ω ∨ j ≤ π ω

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
⊢ τ ω ≤ j → (τ ω ≤ π ω ↔ (τ ω ≤ π ω ∨ j ≤ π ω) ∧ (τ ω ≤ j ∨ True))

Tactic:
intro h

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω ≤ j
⊢ τ ω ≤ π ω ↔ (τ ω ≤ π ω ∨ j ≤ π ω) ∧ (τ ω ≤ j ∨ True)

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω ≤ j
⊢ τ ω ≤ π ω ↔ τ ω ≤ π ω ∨ j ≤ π ω

Tactic:
rw [Iff.comm, or_iff_left_iff_imp]

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω ≤ j
⊢ j ≤ π ω → τ ω ≤ π ω

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω ≤ j
⊢ j ≤ π ω → τ ω ≤ π ω

Tactic:
exact h.trans

Result:
no goals