-- Mathlib/Probability/Process/Stopping.lean
theorem memLp_stoppedValue_of_mem_finset (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, MemLp (u n) p μ)
    {s : Finset ι} (hbdd : ∀ ω, τ ω ∈ s) : MemLp (stoppedValue u τ) p μ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
⊢ (Set.range τ).Countable

Tactic:
refine ((Finset.finite_toSet s).subset fun ω hω => ?_).countable

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
ω : ι
hω : ω ∈ Set.range τ
⊢ ω ∈ ↑s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
⊢ MemLp (stoppedValue u τ) p μ

Tactic:
rw [stoppedValue_eq_of_mem_finset hbdd]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
⊢ MemLp (∑ i ∈ s, {ω | τ ω = i}.indicator (u i)) p μ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
⊢ MeasurableSet {ω | τ ω = i}

Tactic:
refine ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq_of_countable_range ?_ i)

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
⊢ (Set.range τ).Countable

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
⊢ MemLp (∑ i ∈ s, {ω | τ ω = i}.indicator (u i)) p μ

Tactic:
refine memLp_finset_sum' _ fun i _ => MemLp.indicator ?_ (hu i)

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
⊢ MeasurableSet {ω | τ ω = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
ω : ι
hω : ω ∈ Set.range τ
⊢ ω ∈ ↑s

Tactic:
obtain ⟨y, rfl⟩ := hω

Result:
case intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
y : Ω
⊢ τ y ∈ ↑s

Proof state:
case intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
i : ι
x✝ : i ∈ s
y : Ω
⊢ τ y ∈ ↑s

Tactic:
exact hbdd y

Result:
no goals