awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ ¬τ ω = (↑m : WithTop ι)

Tactic:
(lt_of_lt_of_le ?_ h).ne'

Premises used: LT.lt.ne', lt_of_lt_of_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
h₁ : (↑m : WithTop ι) < (↑n : WithTop ι)
⊢ ¬τ ω = (↑m : WithTop ι)

Tactic:
refine (lt_of_lt_of_le ?_ h).ne'

Premises used: LT.lt.ne', lt_of_lt_of_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ (↑m : WithTop ι) < (↑n : WithTop ι)

Tactic:
mod_cast hm.2

Premises used: cast, WithTop.coe_lt_coe._simp_1, And.right, Eq.symm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ (↑m : WithTop ι) < (↑n : WithTop ι)

Tactic:
exact mod_cast hm.2

Premises used: And.right
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
⊢ Membership.mem (γ := Set Ω) {a : Ω | (↑n : WithTop ι) ≤ τ a} ω

Tactic:
h

Premises used: Set.Mem, setOf
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
⊢ Membership.mem (γ := Set Ω) {a : Ω | (↑n : WithTop ι) ≤ τ a} ω

Tactic:
exact h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : τ ω < (↑n : WithTop ι)
h₁ :
  u (τ ω).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
⊢ stoppedProcess u τ n ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω

Tactic:
rw [stoppedProcess_eq_of_ge (le_of_lt h)]

Premises used: MeasureTheory.stoppedProcess_eq_of_ge, le_of_lt
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_contra : τ ω = ⊤
⊢ False

Tactic:
simp [h_contra] at h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ τ ω ≠ ⊤

Tactic:
have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ τ ω ∈ WithTop.some '' (↑s : Set ι)

Tactic:
specialize hbdd ω h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
hbdd : τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ τ ω ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
hbdd : τ ω ∈ WithTop.some '' (↑s : Set ι)
h₁ :
  ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (h : (↑i : WithTop ι) < (↑n : WithTop ι))
    (hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)),
    u (↑i : WithTop ι).untopA ω =
      Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
        ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
⊢ u (τ ω).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω

Tactic:
lift τ ω to ι using h_top with i hi
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
h₁ :
  u (↑i : WithTop ι).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω
h₂ : i ∈ {i ∈ s | i < n}
h₃ : ∀ b ∈ {i ∈ s | i < n}, b ≠ i → Set.indicator {ω : Ω | τ ω = (↑b : WithTop ι)} (u b) ω = 0
⊢ u (↑i : WithTop ι).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω

Tactic:
rw [Finset.sum_eq_single_of_mem i]

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
h₁ :
  u i ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω
⊢ u (↑i : WithTop ι).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω

Tactic:
simp only [untopD_coe]

Premises used: WithTop.untopD_coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
h₁ : Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} ω
h₂ : ω ∉ {a : Ω | (↑n : WithTop ι) ≤ τ a}
⊢ u i ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω

Tactic:
rw [Set.indicator_of_notMem, zero_add, Set.indicator_of_mem]

Premises used: zero_add, Set.indicator_of_mem, Set.indicator_of_notMem
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
⊢ τ ω = (↑i : WithTop ι)

Tactic:
hi.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
⊢ τ ω = (↑i : WithTop ι)

Tactic:
exact hi.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
h₁ : ¬(↑n : WithTop ι) ≤ (↑i : WithTop ι)
⊢ ¬(↑n : WithTop ι) ≤ τ ω

Tactic:
rw [← hi]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
⊢ ¬(↑n : WithTop ι) ≤ (↑i : WithTop ι)

Tactic:
not_le.2 h

Premises used: not_le, Iff.mpr
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
⊢ ¬(↑n : WithTop ι) ≤ (↑i : WithTop ι)

Tactic:
exact not_le.2 h

Premises used: not_le, Iff.mpr
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
h₁ : i ∈ s ∧ i < n
⊢ i ∈ {i ∈ s | i < n}

Tactic:
rw [Finset.mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
⊢ i ∈ s

Tactic:
simp only [Set.mem_image, Finset.mem_coe, coe_eq_coe, exists_eq_right] at hbdd

Premises used: Set.mem_image, exists_eq_right, WithTop.coe_eq_coe, Finset.mem_coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : i ∈ s
⊢ i ∈ s ∧ i < n

Tactic:
⟨hbdd, mod_cast h⟩

Premises used: cast, WithTop.coe_lt_coe._simp_1, And.intro
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : i ∈ s
⊢ i ∈ s ∧ i < n

Tactic:
exact ⟨hbdd, mod_cast h⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
b : ι
h₁ : b ∈ {i ∈ s | i < n} → b ≠ i → Set.indicator {ω : Ω | τ ω = (↑b : WithTop ι)} (u b) ω = 0
⊢ b ∈ {i ∈ s | i < n} → b ≠ i → Set.indicator {ω : Ω | τ ω = (↑b : WithTop ι)} (u b) ω = 0

Tactic:
_
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
b : ι
h_1 : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
h₁ : ω ∉ {ω : Ω | τ ω = (↑b : WithTop ι)}
⊢ Set.indicator {ω : Ω | τ ω = (↑b : WithTop ι)} (u b) ω = 0

Tactic:
rw [Set.indicator_of_notMem]

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
b : ι
h_1 : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
h₁ : ¬(↑i : WithTop ι) = (↑b : WithTop ι)
⊢ ω ∉ {ω : Ω | τ ω = (↑b : WithTop ι)}

Tactic:
rw [Set.mem_setOf, ← hi]

Premises used: Set.mem_setOf
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
b : ι
h_1 : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
⊢ ¬(↑i : WithTop ι) = (↑b : WithTop ι)

Tactic:
mod_cast hneq.symm

Premises used: congrArg, cast, Ne.symm, WithTop.coe_inj._simp_1, Eq.symm, Not
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)
b : ι
h_1 : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
⊢ ¬(↑i : WithTop ι) = (↑b : WithTop ι)

Tactic:
exact mod_cast hneq.symm

Premises used: Ne.symm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
simp : ∃ x < n, (↑x : WithTop ι) = τ ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)

Tactic:
simp only [Finset.coe_Iio, Set.mem_image, Set.mem_Iio]

Premises used: Set.mem_Iio, Set.mem_image, Finset.coe_Iio
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_contra : τ ω = ⊤
⊢ False

Tactic:
simp [h_contra] at h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ τ ω ≠ ⊤

Tactic:
have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ τ ω ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
lift :
  ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (h : (↑i : WithTop ι) < (↑n : WithTop ι)),
    ∃ x < n, (↑x : WithTop ι) = (↑i : WithTop ι)
⊢ ∃ x < n, (↑x : WithTop ι) = τ ω

Tactic:
lift τ ω to ι using h_top with i hi
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
⊢ ∃ x < n, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
⟨i, mod_cast h, rfl⟩

Premises used: cast, WithTop.coe_lt_coe._simp_1, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
⊢ ∃ x < n, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
exact ⟨i, mod_cast h, rfl⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
⊢ ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)

Tactic:
have h_mem : ∀ ω, τ ω < n → τ ω ∈ WithTop.some '' (Finset.Iio n) := by
    intro ω h
    simp only [Finset.coe_Iio, Set.mem_image, Set.mem_Iio]
    have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
    lift τ ω to ι using h_top with i hi
    exact ⟨i, mod_cast h, rfl⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)
rw :
  Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)

Tactic:
rw [stoppedProcess_eq_of_mem_finset n h_mem]

Premises used: MeasureTheory.stoppedProcess_eq_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)
e_a : ∀ (i : ι), i ∈ {i ∈ Finset.Iio n | i < n} ↔ i ∈ Finset.Iio n
⊢ Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)

Tactic:
congr with i
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)
i : ι
⊢ i ∈ {i ∈ Finset.Iio n | i < n} ↔ i ∈ Finset.Iio n

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
rw : MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ
⊢ MemLp (stoppedValue u τ) p μ

Tactic:
rw [stoppedValue_eq_of_mem_finset hbdd]

Premises used: MeasureTheory.stoppedValue_eq_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ

Tactic:
memLp_finsetSum' _ fun i _ => MemLp.indicator ?_ (hu i)

Premises used: MeasureTheory.memLp_finsetSum', MeasureTheory.MemLp.indicator
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
refine : ∀ i ∈ s, MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
⊢ MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ

Tactic:
refine memLp_finsetSum' _ fun i _ => MemLp.indicator ?_ (hu i)

Premises used: MeasureTheory.memLp_finsetSum', MeasureTheory.MemLp.indicator
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq_of_countable_range ?_ i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, setOf, WithTop.some, MeasureTheory.Filtration.le, Eq
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
refine : (Set.range τ).Countable
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
refine ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq_of_countable_range ?_ i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, setOf, WithTop.some, MeasureTheory.Filtration.le, Eq
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
y : Ω
⊢ τ y ∈ WithTop.some '' (↑s : Set ι)

Tactic:
hbdd y
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
y : Ω
⊢ τ y ∈ WithTop.some '' (↑s : Set ι)

Tactic:
exact hbdd y