-- 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 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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
⊢ (ω ∈ s ∧ τ ω ≤ π ω) ∧ (τ ω ≤ i ∨ π ω ≤ i) ↔
    ((ω ∈ s ∧ τ ω ≤ i) ∧ (τ ω ≤ i ∨ π ω ≤ i)) ∧ (τ ω ≤ π ω ∨ i ≤ π ω) ∧ (τ ω ≤ i ∨ True)

Tactic:
by_cases hτi : τ ω ≤ i

Result:
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
⊢ (ω ∈ s ∧ τ ω ≤ π ω) ∧ (τ ω ≤ i ∨ π ω ≤ i) ↔
    ((ω ∈ s ∧ τ ω ≤ i) ∧ (τ ω ≤ i ∨ π ω ≤ i)) ∧ (τ ω ≤ π ω ∨ i ≤ π ω) ∧ (τ ω ≤ i ∨ True)

case neg
Ω : 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
⊢ (ω ∈ s ∧ τ ω ≤ π ω) ∧ (τ ω ≤ i ∨ π ω ≤ i) ↔
    ((ω ∈ s ∧ τ ω ≤ i) ∧ (τ ω ≤ i ∨ π ω ≤ i)) ∧ (τ ω ≤ π ω ∨ i ≤ π ω) ∧ (τ ω ≤ i ∨ True)

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
⊢ (ω ∈ s ∧ τ ω ≤ π ω) ∧ (τ ω ≤ i ∨ π ω ≤ i) ↔
    ((ω ∈ s ∧ τ ω ≤ i) ∧ (τ ω ≤ i ∨ π ω ≤ i)) ∧ (τ ω ≤ π ω ∨ i ≤ π ω) ∧ (τ ω ≤ i ∨ True)

Tactic:
simp only [hτi, true_or, and_true, and_congr_right_iff]

Result:
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
⊢ ω ∈ s → (τ ω ≤ π ω ↔ τ ω ≤ π ω ∨ i ≤ π ω)

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

Tactic:
simp only [min_le_iff, Set.mem_inter_iff, Set.mem_setOf_eq, le_min_iff, le_refl, true_and,
  true_or]

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 π
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
i : ι
ω : Ω
⊢ (ω ∈ s ∧ τ ω ≤ π ω) ∧ (τ ω ≤ i ∨ π ω ≤ i) ↔
    ((ω ∈ s ∧ τ ω ≤ i) ∧ (τ ω ≤ i ∨ π ω ≤ i)) ∧ (τ ω ≤ π ω ∨ i ≤ π ω) ∧ (τ ω ≤ i ∨ True)

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 {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i}

Tactic:
apply @measurableSet_le _ _ _ _ _ (Filtration.seq f i) _ _ _ _ _ ?_ ?_

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}
⊢ Measurable fun a => τ a ⊓ i

Ω : 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

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 : ι
⊢ s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ⊓ π ω ≤ i} ∩ {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i}

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

Proof state:
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 ≤ π ω
⊢ τ ω ≤ π ω

Tactic:
exact hτi.trans h

Result:
no goals