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

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 Ω
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
constructor <;> intro h

Result:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Proof state:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
this : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω}
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
rw [this]

Result:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
this : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω}
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω})

Proof state:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
rw [measurableSet_min_iff hτ hπ] at h

Result:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) ∧ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω}

Tactic:
rw [Set.inter_assoc, Set.inter_self]

Result:
no goals

Proof state:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) ∧ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
exact h.1

Result:
no goals

Proof state:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
this : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω}
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω})

Tactic:
exact measurableSet_inter_le _ hπ _ h

Result:
no goals

Proof state:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
have : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω} := by
  rw [Set.inter_assoc, Set.inter_self]

Result:
case 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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
this : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω}
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})