-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedValue_eq_of_mem_finset [AddCommMonoid E] {s : Finset ι} (hbdd : ∀ ω, τ ω ∈ s) :
    stoppedValue u τ = ∑ i ∈ s, Set.indicator {ω | τ ω = i} (u i)

Proof state:
case h.h.mp
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω ∈ s ∧ τ y = ω
⊢ ω = τ y

Tactic:
exact h.2.symm

Result:
no goals

Proof state:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
⊢ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s = {τ y}

Tactic:
ext1 ω

Result:
case h.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
⊢ ω ∈ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s ↔ ω ∈ {τ y}

Proof state:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
⊢ stoppedValue u τ = ∑ i ∈ s, {ω | τ ω = i}.indicator (u i)

Tactic:
ext y

Result:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
⊢ stoppedValue u τ y = (∑ i ∈ s, {ω | τ ω = i}.indicator (u i)) y

Proof state:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
⊢ u (τ y) y = ∑ i ∈ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s, u i y

Tactic:
suffices Finset.filter (fun i => y ∈ {ω : Ω | τ ω = i}) s = ({τ y} : Finset ι) by
  rw [this, Finset.sum_singleton]

Result:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
⊢ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s = {τ y}

Proof state:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
this : Finset.filter (fun i => y ∈ {ω | τ ω = i}) s = {τ y}
⊢ u (τ y) y = ∑ i ∈ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s, u i y

Tactic:
rw [this, Finset.sum_singleton]

Result:
no goals

Proof state:
case h.h.mpr
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω = τ y
⊢ τ y ∈ s

Tactic:
exact hbdd y

Result:
no goals

Proof state:
case h.h.mpr
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω = τ y
⊢ ω ∈ s ∧ τ y = ω

Tactic:
refine ⟨?_, h.symm⟩

Result:
case h.h.mpr
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω = τ y
⊢ ω ∈ s

Proof state:
case h.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
⊢ ω ∈ s ∧ τ y = ω ↔ ω = τ y

Tactic:
constructor <;> intro h

Result:
case h.h.mp
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω ∈ s ∧ τ y = ω
⊢ ω = τ y

case h.h.mpr
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω = τ y
⊢ ω ∈ s ∧ τ y = ω

Proof state:
case h.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
⊢ ω ∈ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s ↔ ω ∈ {τ y}

Tactic:
simp only [Set.mem_setOf_eq, Finset.mem_filter, Finset.mem_singleton]

Result:
case h.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
⊢ ω ∈ s ∧ τ y = ω ↔ ω = τ y

Proof state:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
⊢ stoppedValue u τ y = (∑ i ∈ s, {ω | τ ω = i}.indicator (u i)) y

Tactic:
rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]

Result:
case h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
⊢ u (τ y) y = ∑ i ∈ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s, u i y

Proof state:
case h.h.mpr
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω = τ y
⊢ ω ∈ s

Tactic:
rw [h]

Result:
case h.h.mpr
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
y : Ω
ω : ι
h : ω = τ y
⊢ τ y ∈ s