-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSpace_const (f : Filtration ι m) (i : ι) :
    (isStoppingTime_const f i).measurableSpace = f i

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet s

Tactic:
exact f.mono hij _ h

Result:
no goals

Proof state:
case h.mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
⊢ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | i ≤ i_1})

Tactic:
intro j

Result:
case h.mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
⊢ MeasurableSet (s ∩ {ω | i ≤ j})

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω | i ≤ j})

Tactic:
simp only [hij, Set.setOf_true, Set.inter_univ]

Result:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet s

Proof state:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | i ≤ i_1})
⊢ MeasurableSet s

Tactic:
specialize h i

Result:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet (s ∩ {ω | i ≤ i})
⊢ MeasurableSet s

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ (∀ (i_1 : ι), MeasurableSet (s ∩ {ω | i ≤ i_1})) ↔ MeasurableSet s

Tactic:
constructor <;> intro h

Result:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | i ≤ i_1})
⊢ MeasurableSet s

case h.mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
⊢ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | i ≤ i_1})

Proof state:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ {ω | i ≤ j})

Tactic:
simp only [hij, Set.setOf_false, Set.inter_empty, @MeasurableSet.empty _ (f.1 j)]

Result:
no goals

Proof state:
case h.mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
⊢ MeasurableSet (s ∩ {ω | i ≤ j})

Tactic:
by_cases hij : i ≤ j

Result:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω | i ≤ j})

case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ {ω | i ≤ j})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
⊢ ⋯.measurableSpace = ↑f i

Tactic:
ext1 s

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ MeasurableSet s ↔ MeasurableSet s

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ MeasurableSet s ↔ MeasurableSet s

Tactic:
rw [IsStoppingTime.measurableSet]

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ (∀ (i_1 : ι), MeasurableSet (s ∩ {ω | i ≤ i_1})) ↔ MeasurableSet s

Proof state:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet (s ∩ {ω | i ≤ i})
⊢ MeasurableSet s

Tactic:
simpa only [le_refl, Set.setOf_true, Set.inter_univ] using h

Result:
no goals