-- 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.inr.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 ∈ Finset.filter (fun x => x < n) s, b ≠ τ ω → {ω | τ ω = b}.indicator (u b) ω = 0

Tactic:
intro b _ hneq

Result:
case h.inr.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}.indicator (u b) ω = 0

Proof state:
case h.inr
Ω : 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
⊢ stoppedProcess u τ n ω =
    {a | n ≤ τ a}.indicator (u n) ω + ∑ c ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = c}.indicator (u c) ω

Tactic:
rw [stoppedProcess_eq_of_ge (le_of_lt h), Finset.sum_eq_single_of_mem (τ ω)]

Result:
case h.inr
Ω : 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
⊢ u (τ ω) ω = {a | n ≤ τ a}.indicator (u n) ω + {ω_1 | τ ω_1 = τ ω}.indicator (u (τ ω)) ω

case h.inr.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
⊢ τ ω ∈ Finset.filter (fun x => x < n) s

case h.inr.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 ∈ Finset.filter (fun x => x < n) s, b ≠ τ ω → {ω | τ ω = b}.indicator (u b) ω = 0

Proof state:
case h.inr.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}.indicator (u b) ω = 0

Tactic:
rw [Set.indicator_of_not_mem]

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 ≤ τ ω
⊢ stoppedProcess u τ n ω =
    {a | n ≤ τ a}.indicator (u n) ω + ∑ c ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = c}.indicator (u c) ω

Tactic:
rw [stoppedProcess_eq_of_le h, Set.indicator_of_mem, Finset.sum_eq_zero, add_zero]

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 ≤ τ ω
⊢ ∀ x ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = x}.indicator (u x) ω = 0

case h.inl.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 ≤ τ ω
⊢ ω ∈ {a | n ≤ τ a}

Proof state:
case h.inr.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
⊢ ¬n ≤ τ ω

Tactic:
exact not_le.2 h

Result:
no goals

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) ω + ∑ c ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = c}.indicator (u c) ω

Tactic:
rcases le_or_lt n (τ ω) with h | h

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 ≤ τ ω
⊢ stoppedProcess u τ n ω =
    {a | n ≤ τ a}.indicator (u n) ω + ∑ c ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = c}.indicator (u c) ω

case h.inr
Ω : 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
⊢ 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 ≤ τ ω
m : ι
hm : m ∈ Finset.filter (fun x => x < n) s
⊢ {ω | τ ω = m}.indicator (u m) ω = 0

Tactic:
refine Set.indicator_of_not_mem ?_ _

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}

Proof state:
case h.inr.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
⊢ τ ω ∈ s ∧ τ ω < n

Tactic:
exact ⟨hbdd ω h, h⟩

Result:
no goals

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 ∈ s ∧ m < n
⊢ ω ∉ {ω | τ ω = m}

Tactic:
exact (hm.2.trans_le h).ne'

Result:
no goals

Proof state:
case h.inl.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 ≤ τ ω
⊢ ω ∈ {a | n ≤ τ a}

Tactic:
exact h

Result:
no goals

Proof state:
case h.inr.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
⊢ τ ω ∈ Finset.filter (fun x => x < n) s

Tactic:
rw [Finset.mem_filter]

Result:
case h.inr.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
⊢ τ ω ∈ s ∧ τ ω < n

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:
exact hneq.symm

Result:
no goals

Proof state:
case h.inr
Ω : 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
⊢ u (τ ω) ω = {a | n ≤ τ a}.indicator (u n) ω + {ω_1 | τ ω_1 = τ ω}.indicator (u (τ ω)) ω

Tactic:
rw [Set.indicator_of_not_mem, zero_add, Set.indicator_of_mem] <;> rw [Set.mem_setOf]

Result:
case h.inr.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
⊢ ¬n ≤ τ ω