-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedValue_sub_eq_sum' [AddCommGroup β] (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ ω, π ω ≤ N) :
    stoppedValue u π - stoppedValue u τ = fun ω =>
      (∑ i ∈ Finset.range (N + 1), Set.indicator {ω | τ ω ≤ i ∧ i < π ω} (u (i + 1) - u i)) ω

Proof state:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ (fun ω => (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω) = fun ω =>
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω

Tactic:
ext ω

Result:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
⊢ (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω =
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω

Proof state:
case h.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
i : ℕ
⊢ τ ω ≤ i ∧ i < π ω ↔ i < N + 1 ∧ τ ω ≤ i ∧ i < π ω

Tactic:
exact ⟨fun h => ⟨lt_trans h.2 (Nat.lt_succ_iff.2 <| hbdd _), h⟩, fun h => h.2⟩

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ stoppedValue u π - stoppedValue u τ = fun ω =>
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω

Tactic:
rw [stoppedValue_sub_eq_sum hle]

Result:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ (fun ω => (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω) = fun ω =>
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω

Proof state:
case h.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
i : ℕ
⊢ i ∈ Finset.Ico (τ ω) (π ω) ↔ i ∈ Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1))

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

Result:
case h.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
i : ℕ
⊢ τ ω ≤ i ∧ i < π ω ↔ i < N + 1 ∧ τ ω ≤ i ∧ i < π ω

Proof state:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
⊢ (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω =
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω

Tactic:
simp only [Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]

Result:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
⊢ ∑ c ∈ Finset.Ico (τ ω) (π ω), (u (c + 1) - u c) ω =
    ∑ c ∈ Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1)), (u (c + 1) - u c) ω

Proof state:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
⊢ Finset.Ico (τ ω) (π ω) = Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1))

Tactic:
ext i

Result:
case h.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
i : ℕ
⊢ i ∈ Finset.Ico (τ ω) (π ω) ↔ i ∈ Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1))

Proof state:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
⊢ ∑ c ∈ Finset.Ico (τ ω) (π ω), (u (c + 1) - u c) ω =
    ∑ c ∈ Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1)), (u (c + 1) - u c) ω

Tactic:
refine Finset.sum_congr ?_ fun _ _ => rfl

Result:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
ω : Ω
⊢ Finset.Ico (τ ω) (π ω) = Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1))