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

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ MemLp (fun ω => ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω) p μ

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

Result:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
i : ι
x✝ : i ∈ Finset.filter (fun x => x < n) s
⊢ MeasurableSet {a | τ a = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ MemLp ({a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) p μ

Tactic:
refine MemLp.add ?_ ?_

Result:
case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ MemLp ({a | n ≤ τ a}.indicator (u n)) p μ

case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ MemLp (∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) p μ

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
i : ι
x✝ : i ∈ Finset.filter (fun x => x < n) s
⊢ MeasurableSet {a | τ a = i}

Tactic:
exact ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq i)

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ MemLp ({a | n ≤ τ a}.indicator (u n)) p μ

Tactic:
exact MemLp.indicator (ℱ.le n {a : Ω | n ≤ τ a} (hτ.measurableSet_ge n)) (hu n)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
this : MemLp (fun ω => ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω) p μ
⊢ MemLp (∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) p μ

Tactic:
convert this using 1

Result:
case h.e'_6
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
this : MemLp (fun ω => ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω) p μ
⊢ ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i) = fun ω =>
    ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω

Proof state:
case h.e'_6
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
this : MemLp (fun ω => ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω) p μ
⊢ ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i) = fun ω =>
    ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω

Tactic:
ext1 ω

Result:
case h.e'_6.h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
this : MemLp (fun ω => ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω) p μ
ω : Ω
⊢ (∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) ω =
    ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω

Proof state:
case h.e'_6.h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
this : MemLp (fun ω => ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω) p μ
ω : Ω
⊢ (∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) ω =
    ∑ i ∈ Finset.filter (fun x => x < n) s, {a | τ a = i}.indicator (u i) ω

Tactic:
simp only [Finset.sum_apply]

Result:
no goals