-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_eq_stopping_time [AddGroup ι] [TopologicalSpace ι] [MeasurableSpace ι]
    [BorelSpace ι] [OrderTopology ι] [MeasurableSingletonClass ι] [SecondCountableTopology ι]
    [MeasurableSub₂ ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω = π ω}

Proof state:
case hg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}
⊢ Measurable fun x => π x ⊓ j

Tactic:
exact (hπ.min_const j).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✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}
⊢ MeasurableSet ({ω | τ ω = π ω} ∩ {ω | τ ω ≤ j})

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}
⊢ MeasurableSet ({ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j})

Proof state:
case h.refine_3
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : (τ ω ⊓ j = π ω ⊓ j ∧ τ ω ≤ j) ∧ π ω ≤ j
⊢ τ ω = π ω

Tactic:
obtain ⟨h', hσ_le⟩ := h

Result:
case h.refine_3.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h' : τ ω ⊓ j = π ω ⊓ j ∧ τ ω ≤ j
hσ_le : π ω ≤ j
⊢ τ ω = π ω

Proof state:
case h.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω = π ω ∧ τ ω ≤ j
⊢ τ ω ⊓ j = π ω ⊓ j

Tactic:
rw [h.1]

Result:
no goals

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

Tactic:
ext1 ω

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

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
⊢ τ ω = π ω ∧ τ ω ≤ j ↔ (τ ω ⊓ j = π ω ⊓ j ∧ τ ω ≤ j) ∧ π ω ≤ j

Tactic:
refine ⟨fun h => ⟨⟨?_, h.2⟩, ?_⟩, fun h => ⟨?_, h.1.2⟩⟩

Result:
case h.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω = π ω ∧ τ ω ≤ j
⊢ τ ω ⊓ j = π ω ⊓ j

case h.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω = π ω ∧ τ ω ≤ j
⊢ π ω ≤ j

case h.refine_3
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : (τ ω ⊓ j = π ω ⊓ j ∧ τ ω ≤ j) ∧ π ω ≤ j
⊢ τ ω = π ω

Proof state:
case h.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω = π ω ∧ τ ω ≤ j
⊢ τ ω ≤ j

Tactic:
exact h.2

Result:
no goals

Proof state:
case hf
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁷ : AddGroup ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : OrderTopology ι
inst✝² : MeasurableSingletonClass ι
inst✝¹ : SecondCountableTopology ι
inst✝ : MeasurableSub₂ ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}
⊢ Measurable fun x => τ x ⊓ j

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

Result:
no goals