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

Proof state:
case pos
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
hτi : τ ω ≤ i
a✝ : ω ∈ s
⊢ τ ω ≤ π ω ↔ τ ω ≤ π ω ∨ i ≤ π ω

Tactic:
constructor <;> intro h

Result:
case pos.mp
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
hτi : τ ω ≤ i
a✝ : ω ∈ s
h : τ ω ≤ π ω
⊢ τ ω ≤ π ω ∨ i ≤ π ω

case pos.mpr
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
hτi : τ ω ≤ i
a✝ : ω ∈ s
h : τ ω ≤ π ω ∨ i ≤ π ω
⊢ τ ω ≤ π ω

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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
this :
  s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ⊓ π ω ≤ i} ∩ {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i}
⊢ Measurable fun a => τ a ⊓ π a ⊓ i

Tactic:
exact ((hτ.min hπ).min_const i).measurable_of_le fun _ => min_le_right _ _

Result:
no goals

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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
this :
  s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ⊓ π ω ≤ i} ∩ {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i}
⊢ Measurable fun a => τ a ⊓ i

Tactic:
exact (hτ.min_const i).measurable_of_le fun _ => min_le_right _ _

Result:
no goals

Proof state:
case pos.mpr.inl
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
hτi : τ ω ≤ i
a✝ : ω ∈ s
h : τ ω ≤ π ω
⊢ τ ω ≤ π ω

Tactic:
exact h

Result:
no goals

Proof state:
case pos.mpr
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
hτi : τ ω ≤ i
a✝ : ω ∈ s
h : τ ω ≤ π ω ∨ i ≤ π ω
⊢ τ ω ≤ π ω

Tactic:
rcases h with h | h

Result:
case pos.mpr.inl
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
hτi : τ ω ≤ i
a✝ : ω ∈ s
h : τ ω ≤ π ω
⊢ τ ω ≤ π ω

case pos.mpr.inr
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
hτi : τ ω ≤ i
a✝ : ω ∈ s
h : i ≤ π ω
⊢ τ ω ≤ π ω

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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
this :
  s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ⊓ π ω ≤ i} ∩ {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i}
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ i})

Tactic:
rw [this]

Result:
Ω : 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
this :
  s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ⊓ π ω ≤ i} ∩ {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i}
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ⊓ π ω ≤ i} ∩ {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i})