-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSpace_min (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
    (hτ.min hπ).measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
this : ∀ (i : ι), {ω | τ ω ⊓ π ω ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}
⊢ ((∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})) ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ i})) →
    ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∪ s ∩ {ω | π ω ≤ i})

Tactic:
exact fun h i => (h.left i).union (h.right i)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
i : ι
⊢ {ω | τ ω ⊓ π ω ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω ⊓ π ω ≤ i} ↔ ω ∈ {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}

Proof state:
case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
exact le_inf (measurableSpace_mono _ hτ fun _ => min_le_left _ _)
  (measurableSpace_mono _ hπ fun _ => min_le_right _ _)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace

case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ hτ.measurableSpace ⊓ hπ.measurableSpace ≤ ⋯.measurableSpace

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω ⊓ π ω ≤ i} ↔ ω ∈ {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s → MeasurableSet s

Tactic:
change MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[hπ.measurableSpace] s →
  MeasurableSet[(hτ.min hπ).measurableSpace] s

Result:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s ∧ MeasurableSet s → MeasurableSet s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ ∀ (i : ι), {ω | τ ω ⊓ π ω ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}

Tactic:
intro i

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
i : ι
⊢ {ω | τ ω ⊓ π ω ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
this : ∀ (i : ι), {ω | τ ω ⊓ π ω ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}
⊢ ((∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})) ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ i})) →
    ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ⊓ π ω ≤ i})

Tactic:
simp_rw [this, Set.inter_union_distrib_left]

Result:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
this : ∀ (i : ι), {ω | τ ω ⊓ π ω ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}
⊢ ((∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})) ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ i})) →
    ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∪ s ∩ {ω | π ω ≤ i})

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ hτ.measurableSpace ⊓ hπ.measurableSpace ≤ ⋯.measurableSpace

Tactic:
intro s

Result:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s → MeasurableSet s

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s ∧ MeasurableSet s → MeasurableSet s

Tactic:
simp_rw [IsStoppingTime.measurableSet]

Result:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ ((∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})) ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ i})) →
    ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ⊓ π ω ≤ i})

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ ((∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})) ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ i})) →
    ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ⊓ π ω ≤ i})

Tactic:
have : ∀ i, {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i} := by
  intro i; ext1 ω; simp

Result:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
this : ∀ (i : ι), {ω | τ ω ⊓ π ω ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}
⊢ ((∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})) ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ i})) →
    ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ⊓ π ω ≤ i})