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

Tactic:
intro 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 : ι
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ 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} ∩ {ω | τ ω ⊓ π ω ≤ i} ∩ {ω | τ ω ⊓ i ≤ τ ω ⊓ π ω ⊓ i})

Tactic:
refine ((hs i).inter ((hτ.min hπ) i)).inter ?_

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

Proof state:
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
x✝ : ω ∈ s
hτ_le_π : τ ω ≤ π ω
⊢ i < τ ω

Tactic:
rw [← not_le]

Result:
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
x✝ : ω ∈ s
hτ_le_π : τ ω ≤ π ω
⊢ ¬τ ω ≤ i

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 ≤ π ω)

Tactic:
intro

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
a✝ : ω ∈ s
⊢ τ ω ≤ π ω ↔ τ ω ≤ π ω ∨ i ≤ π ω

Proof state:
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)

Tactic:
simp only [hτi, false_or, and_false, false_and, iff_false, not_and, not_le, and_imp]

Result:
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 < π ω

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

Tactic:
refine fun _ hτ_le_π => lt_of_lt_of_le ?_ hτ_le_π

Result:
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
x✝ : ω ∈ s
hτ_le_π : τ ω ≤ π ω
⊢ 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 : MeasurableSet s
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
simp_rw [IsStoppingTime.measurableSet] at hs ⊢

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 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ⊓ π ω ≤ i})

Proof state:
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
x✝ : ω ∈ s
hτ_le_π : τ ω ≤ π ω
⊢ ¬τ ω ≤ i

Tactic:
exact hτi

Result:
no goals

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

Tactic:
exact Or.inl h

Result:
no goals