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

Proof state:
case h.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
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✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ∀ (i : ι), MeasurableSet ({ω | τ ω = π ω} ∩ {ω | τ ω ≤ i})

Tactic:
intro j

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

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
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✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} ↔ ω ∈ {ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ MeasurableSet {ω | τ ω = π ω}

Tactic:
rw [hτ.measurableSet]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ∀ (i : ι), MeasurableSet ({ω | τ ω = π ω} ∩ {ω | τ ω ≤ i})

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

Tactic:
simp only [Set.mem_inter_iff, Set.mem_setOf_eq]

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

Proof state:
case hf
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
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:
case h.refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h : τ ω = π ω ∧ τ ω ≤ j
⊢ τ ω ≤ j

Tactic:
exact h.2

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
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✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}
⊢ MeasurableSet ({ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j})

Proof state:
case h.refine_3.intro.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
hπ_le : π ω ≤ j
h_eq : τ ω ⊓ j = π ω ⊓ j
hτ_le : τ ω ≤ j
⊢ τ ω = π ω

Tactic:
rwa [min_eq_left hτ_le, min_eq_left hπ_le] at h_eq

Result:
no goals

Proof state:
case h.refine_3
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
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✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h' : τ ω ⊓ j = π ω ⊓ j ∧ τ ω ≤ j
hπ_le : π ω ≤ j
⊢ τ ω = π ω