-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedProcess_eq_of_mem_finset [LinearOrder ι] [AddCommMonoid E] {s : Finset ι} (n : ι)
    (hbdd : ∀ ω, τ ω < n → τ ω ∈ s) : stoppedProcess u τ n = Set.indicator {a | n ≤ τ a} (u n) +
      ∑ i ∈ s.filter (· < n), Set.indicator {ω | τ ω = i} (u i)

Proof state:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
⊢ stoppedProcess u τ n ω =
    ({a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) ω

Tactic:
rw [Pi.add_apply, Finset.sum_apply]

Result:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
⊢ stoppedProcess u τ n ω =
    {a | n ≤ τ a}.indicator (u n) ω + ∑ c ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = c}.indicator (u c) ω

Proof state:
case h.inl
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
h : n ≤ τ ω
⊢ ∀ x ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = x}.indicator (u x) ω = 0

Tactic:
intro m hm

Result:
case h.inl
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
h : n ≤ τ ω
m : ι
hm : m ∈ Finset.filter (fun x => x < n) s
⊢ {ω | τ ω = m}.indicator (u m) ω = 0

Proof state:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ stoppedProcess u τ n =
    {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)

Tactic:
ext ω

Result:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
⊢ stoppedProcess u τ n ω =
    ({a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) ω

Proof state:
case h.inr.h₀.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
h : τ ω < n
b : ι
a✝ : b ∈ Finset.filter (fun x => x < n) s
hneq : b ≠ τ ω
⊢ ω ∉ {ω | τ ω = b}

Tactic:
rw [Set.mem_setOf]

Result:
case h.inr.h₀.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
h : τ ω < n
b : ι
a✝ : b ∈ Finset.filter (fun x => x < n) s
hneq : b ≠ τ ω
⊢ ¬τ ω = b

Proof state:
case h.inl
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
h : n ≤ τ ω
m : ι
hm : m ∈ Finset.filter (fun x => x < n) s
⊢ ω ∉ {ω | τ ω = m}

Tactic:
rw [Finset.mem_filter] at hm

Result:
case h.inl
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
ω : Ω
h : n ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ ω ∉ {ω | τ ω = m}