-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSpace_le_of_countable_range (hτ : IsStoppingTime f τ)
    (h_countable : (Set.range τ).Countable) : hτ.measurableSpace ≤ m

Proof state:
case h.mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
⊢ (∃ i, ω ∈ ⋃ (_ : i ∈ Set.range τ), s ∩ {ω | τ ω ≤ i}) → ω ∈ s

Tactic:
rintro ⟨i, hx⟩

Result:
case h.mpr.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
i : ι
hx : ω ∈ ⋃ (_ : i ∈ Set.range τ), s ∩ {ω | τ ω ≤ i}
⊢ ω ∈ s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
⊢ s = ⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i}

Tactic:
ext ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
⊢ ω ∈ s ↔ ω ∈ ⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i}

Proof state:
case h.mpr.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
i : ι
hx : (∃ y, τ y = i) ∧ ω ∈ s ∧ τ ω ≤ i
⊢ ω ∈ s

Tactic:
exact hx.2.1

Result:
no goals

Proof state:
case h.mpr.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
i : ι
hx : ω ∈ ⋃ (_ : i ∈ Set.range τ), s ∩ {ω | τ ω ≤ i}
⊢ ω ∈ s

Tactic:
simp only [Set.mem_range, Set.iUnion_exists, Set.mem_iUnion, Set.mem_inter_iff,
  Set.mem_setOf_eq, exists_prop, exists_and_right] at hx

Result:
case h.mpr.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
i : ι
hx : (∃ y, τ y = i) ∧ ω ∈ s ∧ τ ω ≤ i
⊢ ω ∈ s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
hx : ω ∈ s
⊢ ω ∈ ⋃ (_ : τ ω ∈ Set.range τ), s ∩ {ω_1 | τ ω_1 ≤ τ ω}

Tactic:
simpa using hx

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
change ∀ i, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) at hs

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet (⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i})

Tactic:
exact MeasurableSet.biUnion h_countable fun i _ => f.le i _ (hs i)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet s

Tactic:
rw [(_ : s = ⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i})]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet (⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i})

Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
⊢ s = ⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i}

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
⊢ ω ∈ s ↔ ω ∈ ⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i}

Tactic:
constructor <;> rw [Set.mem_iUnion]

Result:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
⊢ ω ∈ s → ∃ i, ω ∈ ⋃ (_ : i ∈ Set.range τ), s ∩ {ω | τ ω ≤ i}

case h.mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
⊢ (∃ i, ω ∈ ⋃ (_ : i ∈ Set.range τ), s ∩ {ω | τ ω ≤ i}) → ω ∈ s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
⊢ hτ.measurableSpace ≤ m

Tactic:
intro s hs

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Proof state:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
s : Set Ω
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
ω : Ω
⊢ ω ∈ s → ∃ i, ω ∈ ⋃ (_ : i ∈ Set.range τ), s ∩ {ω | τ ω ≤ i}

Tactic:
exact fun hx => ⟨τ ω, by simpa using hx⟩

Result:
no goals