awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
h :
  Eq.{u_2 + 1} (α := β) (∑ c ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (c + 1) - u c) ω)
    (∑ c ∈ Finset.range (N + 1) with Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} ω,
      (u (c + 1) - u c) ω)
⊢ Eq.{u_2 + 1} (α := β) ((∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω)
    ((∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω)

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

Premises used: Finset.sum_apply, Finset.sum_indicator_eq_sum_filter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
⊢ Eq.{u_2 + 1} (α := β) (∑ c ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (c + 1) - u c) ω)
    (∑ c ∈ Finset.range (N + 1) with Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} ω,
      (u (c + 1) - u c) ω)

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
h :
  Finset.Ico (untopA (τ ω)) (untopA (π ω)) =
    {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}
⊢ Eq.{u_2 + 1} (α := β) (∑ c ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (c + 1) - u c) ω)
    (∑ c ∈ Finset.range (N + 1) with Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} ω,
      (u (c + 1) - u c) ω)

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
h :
  ∀ (i : ℕ),
    i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)) ↔
      i ∈ {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}
⊢ Finset.Ico (untopA (τ ω)) (untopA (π ω)) =
    {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}

Tactic:
ext i
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
h : untopA (τ ω) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω
⊢ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)) ↔
    i ∈ {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}

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

Premises used: Set.mem_setOf_eq, Finset.mem_range, Finset.mem_filter, Finset.mem_Ico
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
⊢ π ω ≤ (↑N : ℕ∞)

Tactic:
specialize hbdd ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
hbdd : π ω ≤ (↑N : ℕ∞)
⊢ τ ω ≠ ⊤

Tactic:
hτ_top ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
hbdd : π ω ≤ (↑N : ℕ∞)
h :
  ∀ (t : ℕ) (ht : (↑t : ℕ∞) = τ ω),
    untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω
⊢ untopA (τ ω) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω

Tactic:
lift τ ω to ℕ using hτ_top ω with t ht
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
hbdd : π ω ≤ (↑N : ℕ∞)
t : ℕ
ht : (↑t : ℕ∞) = τ ω
⊢ π ω ≠ ⊤

Tactic:
hπ_top ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
hbdd : π ω ≤ (↑N : ℕ∞)
t : ℕ
ht : (↑t : ℕ∞) = τ ω
h :
  ∀ (b : ℕ) (hb : (↑b : ℕ∞) = π ω) (hbdd : LE.le (α := ℕ∞) (↑b : ℕ∞) (↑N : ℕ∞)),
    untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (↑b : ℕ∞) ↔
      i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑b : ℕ∞)
⊢ untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω

Tactic:
lift π ω to ℕ using hπ_top ω with b hb
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i t : ℕ
ht : (↑t : ℕ∞) = τ ω
b : ℕ
hb : (↑b : ℕ∞) = π ω
hbdd : LE.le (α := ℕ∞) (↑b : ℕ∞) (↑N : ℕ∞)
⊢ b ≤ N

Tactic:
simp only [Nat.cast_le] at hbdd

Premises used: Nat.cast_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i t : ℕ
ht : (↑t : ℕ∞) = τ ω
b : ℕ
hb : (↑b : ℕ∞) = π ω
hbdd : b ≤ N
h : t ≤ i → i < b → i ≤ N
⊢ untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (↑b : ℕ∞) ↔
    i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑b : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i t : ℕ
ht : (↑t : ℕ∞) = τ ω
b : ℕ
hb : (↑b : ℕ∞) = π ω
hbdd : b ≤ N
⊢ t ≤ i → i < b → i ≤ N

Tactic:
grind
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : ℕ∞)
⊢ stoppedValue u τ = fun (x : Ω) ↦ (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i)) x

Tactic:
stoppedValue_eq_of_mem_finset fun ω ↦ ?_

Premises used: setOf, ENat, MeasureTheory.stoppedValue_eq_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : ℕ∞)
refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
⊢ stoppedValue u τ = fun (x : Ω) ↦ (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i)) x

Tactic:
refine stoppedValue_eq_of_mem_finset fun ω ↦ ?_

Premises used: MeasureTheory.stoppedValue_eq_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : ℕ∞)
ω : Ω
⊢ τ ω ≤ (↑N : ℕ∞)

Tactic:
specialize hbdd ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
hbdd : τ ω ≤ (↑N : ℕ∞)
h_contra : τ ω = ⊤
⊢ False

Tactic:
simp [h_contra] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
hbdd : τ ω ≤ (↑N : ℕ∞)
⊢ τ ω ≠ ⊤

Tactic:
have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
hbdd : τ ω ≤ (↑N : ℕ∞)
h_top : τ ω ≠ ⊤
⊢ τ ω ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
hbdd : τ ω ≤ (↑N : ℕ∞)
h_top : τ ω ≠ ⊤
lift :
  ∀ (t : ℕ) (ht : (↑t : ℕ∞) = τ ω) (hbdd : LE.le (α := ℕ∞) (↑t : ℕ∞) (↑N : ℕ∞)),
    (↑t : ℕ∞) ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
⊢ τ ω ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)

Tactic:
lift τ ω to ℕ using h_top with t ht
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : (↑t : ℕ∞) = τ ω
hbdd : LE.le (α := ℕ∞) (↑t : ℕ∞) (↑N : ℕ∞)
⊢ t ≤ N

Tactic:
simp only [Nat.cast_le] at hbdd

Premises used: Nat.cast_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : (↑t : ℕ∞) = τ ω
hbdd : t ≤ N
simp : t < N + 1
⊢ (↑t : ℕ∞) ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)

Tactic:
simp only [ENat.some_eq_coe, Finset.coe_range, Set.mem_image, Set.mem_Iio, Nat.cast_inj,
    exists_eq_right, gt_iff_lt]

Premises used: ENat.some_eq_coe, Set.mem_Iio, Finset.coe_range, Set.mem_image, exists_eq_right, Nat.cast_inj, gt_iff_lt
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : (↑t : ℕ∞) = τ ω
hbdd : t ≤ N
⊢ t < N + 1

Tactic:
grind
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
rw :
  Set.indicator {a : Ω | (↑n : WithTop ℕ) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ℕ)} (u i) =
    Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i)

Tactic:
rw [stoppedProcess_eq'' n]

Premises used: MeasureTheory.stoppedProcess_eq''
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
e_a : ∀ (i : ℕ), i ∈ Finset.Iio n ↔ i ∈ Finset.range n
⊢ Set.indicator {a : Ω | (↑n : WithTop ℕ) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ℕ)} (u i) =
    Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i)

Tactic:
congr with i
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n i : ℕ
e_a : i < n ↔ i ∈ Finset.range n
e_a₁ e_a₂ : i < n ↔ i < n
⊢ i ∈ Finset.Iio n ↔ i ∈ Finset.range n

Tactic:
rw [Finset.mem_Iio, Finset.mem_range]

Premises used: Finset.mem_range, Finset.mem_Iio
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
h :
  ∀ (x : Ω),
    Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) x =
      (Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
          Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n))
        x
⊢ Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n)

Tactic:
ext x
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) x =
    Set.indicator ({a : Ω | τ a = (↑n : ℕ∞)} ∪ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}) (u n) x
h₁ : x ∉ {a : Ω | τ a = (↑n : ℕ∞)} ∩ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}
⊢ Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) x =
    (Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
        Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n))
      x

Tactic:
rw [add_comm, Pi.add_apply, ← Set.indicator_union_of_notMem_inter]

Premises used: Set.indicator_union_of_notMem_inter, add_comm, Pi.add_apply
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h :
  Set.indicator {a : Ω | (↑n : WithTop ℕ) = τ a ∨ (↑n : WithTop ℕ) < τ a} (u n) x =
    Set.indicator ({a : Ω | (↑n : WithTop ℕ) = τ a} ∪ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}) (u n) x
⊢ Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) x =
    Set.indicator ({a : Ω | τ a = (↑n : ℕ∞)} ∪ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}) (u n) x

Tactic:
simp_rw [@eq_comm _ _ (n : WithTop ℕ), @le_iff_eq_or_lt _ _ (n : WithTop ℕ)]

Premises used: le_iff_eq_or_lt, eq_comm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} ω ↔
      Membership.mem (γ := Set Ω) {a : Ω | (↑n : ℕ∞) < τ a} ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} {a : Ω | (↑n : ℕ∞) < τ a}

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x ω : Ω
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ⊤ ↔ LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x ω : Ω
t : ℕ
h : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑t : ℕ∞) ↔ n < t
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑t : ℕ∞) ↔ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑t : ℕ∞)

Tactic:
simp only [Nat.cast_lt]

Premises used: Nat.cast_lt
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x ω : Ω
t : ℕ
h h₁ h₂ h₃ : n + 1 ≤ t ↔ n < t
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑t : ℕ∞) ↔ n < t

Tactic:
norm_cast
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x ω : Ω
h : ∀ (x : ℕ∞), HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ x ↔ (↑n : ℕ∞) < x
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ ω ↔ (↑n : ℕ∞) < τ ω

Tactic:
cases τ ω with
        | top => simp
        | coe t =>
          simp only [Nat.cast_lt]
          norm_cast

Premises used: WithTop.top, Nat.cast_lt, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} {a : Ω | (↑n : ℕ∞) < τ a}

Tactic:
have : {a | ↑n + 1 ≤ τ a} = {a | ↑n < τ a} := by
        ext ω
        simp only [Set.mem_setOf_eq]
        cases τ ω with
        | top => simp
        | coe t =>
          simp only [Nat.cast_lt]
          norm_cast
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
this : Eq.{u_1 + 1} (α := Set Ω) {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} {a : Ω | (↑n : ℕ∞) < τ a}
h :
  Set.indicator {a : Ω | (↑n : WithTop ℕ) = τ a ∨ (↑n : WithTop ℕ) < τ a} (u n) x =
    Set.indicator ({a : Ω | (↑n : WithTop ℕ) = τ a} ∪ {a : Ω | (↑n : ℕ∞) < τ a}) (u n) x
h₁ h₂ :
  Set.indicator ({a : Ω | (↑n : WithTop ℕ) = τ a} ∪ {a : Ω | (↑n : WithTop ℕ) < τ a}) (u n) x =
    Set.indicator ({a : Ω | (↑n : WithTop ℕ) = τ a} ∪ {a : Ω | (↑n : ℕ∞) < τ a}) (u n) x
⊢ Set.indicator {a : Ω | (↑n : WithTop ℕ) = τ a ∨ (↑n : WithTop ℕ) < τ a} (u n) x =
    Set.indicator ({a : Ω | (↑n : WithTop ℕ) = τ a} ∪ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}) (u n) x

Tactic:
rw [this, Set.setOf_or]

Premises used: Set.setOf_or
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h₁ : Membership.mem (γ := Set Ω) {a : Ω | τ a = (↑n : ℕ∞)} x
h₂ : Membership.mem (γ := Set Ω) {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} x
⊢ τ x = (↑n : ℕ∞)

Tactic:
rw [Set.mem_setOf] at h₁ h₂

Premises used: Set.mem_setOf
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h₁ : Membership.mem (γ := Set Ω) {a : Ω | τ a = (↑n : ℕ∞)} x
h₂ : Membership.mem (γ := Set Ω) {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} x
h₃ : τ x = (↑n : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ x

Tactic:
rw [Set.mem_setOf] at h₁ h₂

Premises used: Set.mem_setOf
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = (↑n : ℕ∞)
h₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ x
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑n : ℕ∞)

Tactic:
rw [h₁] at h₂
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = (↑n : ℕ∞)
h₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑n : ℕ∞)
⊢ n + 1 ≤ n

Tactic:
norm_cast at h₂
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = (↑n : ℕ∞)
h₂ : n + 1 ≤ n
⊢ False

Tactic:
grind
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
⊢ Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n)

Tactic:
have : {a | n ≤ τ a}.indicator (u n) =
      {a | n + 1 ≤ τ a}.indicator (u n) + {a | τ a = n}.indicator (u n) := by
    ext x
    rw [add_comm, Pi.add_apply, ← Set.indicator_union_of_notMem_inter]
    · simp_rw [@eq_comm _ _ (n : WithTop ℕ), @le_iff_eq_or_lt _ _ (n : WithTop ℕ)]
      have : {a | ↑n + 1 ≤ τ a} = {a | ↑n < τ a} := by
        ext ω
        simp only [Set.mem_setOf_eq]
        cases τ ω with
        | top => simp
        | coe t =>
          simp only [Nat.cast_lt]
          norm_cast
      rw [this, Set.setOf_or]
    · rintro ⟨h₁, h₂⟩
      rw [Set.mem_setOf] at h₁ h₂
      rw [h₁] at h₂
      norm_cast at h₂
      grind
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
this :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n)
rw :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
rw₁ :
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
rw₂ :
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      (Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
        ∑ x ∈ Finset.range n, Set.indicator {a : Ω | τ a = (↑x : ℕ∞)} (u x))
rw₃ rw₄ :
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
        Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ x ∈ Finset.range n, Set.indicator {a : Ω | τ a = (↑x : ℕ∞)} (u x)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)

Tactic:
rw [stoppedProcess_eq, this, Finset.sum_range_succ_comm, ← add_assoc]

Premises used: add_assoc, Finset.sum_range_succ_comm, MeasureTheory.stoppedProcess_eq
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} ω ↔
      ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
⊢ {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
ω : Ω
pos :
  ∀ (hx : ω ∈ s),
    (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
      ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
neg :
  ∀ (hx : ω ∉ s),
    (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
      ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
⊢ (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}

Tactic:
by_cases hx : ω ∈ s
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
ω : Ω
hx : ω ∈ s
⊢ (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
ω : Ω
hx : ω ∉ s
⊢ (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
⊢ {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}

Tactic:
have : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n} := by
    ext1 ω
    simp only [Set.piecewise, Set.mem_setOf_eq]
    by_cases hx : ω ∈ s <;> simp [hx]