-- 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_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
⊢ τ ω = π ω

Tactic:
obtain ⟨h_eq, hτ_le⟩ := h'

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

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 = π ω ⊓ j}

Tactic:
apply measurableSet_eq_fun_of_countable

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

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

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 = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j})

Tactic:
refine
  MeasurableSet.inter (MeasurableSet.inter ?_ (hτ.measurableSet_le j)) (hπ.measurableSet_le 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 : ι
this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | τ ω ⊓ j = π ω ⊓ j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}
⊢ MeasurableSet {ω | τ ω ⊓ j = π ω ⊓ j}

Proof state:
case hg
Ω : 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
Ω : 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:
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✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
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✝⁶ : Countable ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : BorelSpace ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSingletonClass ι
inst✝ : SecondCountableTopology ι
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✝⁶ : 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
⊢ τ ω = π ω

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:
rw [← h.1]

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