awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
h : u (τ y).untopA y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
h₁ : u (τ y).untopA y = ∑ c ∈ s, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) y
h₂ h₃ h₄ : u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
h₅ : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h₆ : ∀ (ω : ι),
  ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
    Membership.mem (γ := Finset ι) {(τ y).untopA} ω
Tactic: classical
  rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
  suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
  ext1 ω
  simp only [Set.mem_setOf_eq, Finset.mem_filter, Finset.mem_singleton]
  constructor <;> intro h
  · simp [h.2]
  · simp only [h]
    specialize hbdd y
    have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
    lift τ y to ι using this with i hi
    simpa using hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
h : u (τ y).untopA y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
h₁ : u (τ y).untopA y = ∑ c ∈ s, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) y
h₂ h₃ h₄ : u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
h₅ : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
h₆ :
  ∀ (ω : ι),
    ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
      Membership.mem (γ := Finset ι) {(τ y).untopA} ω
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h₇ : ∀ (ω : ι), ω ∈ s ∧ τ y = (↑ω : WithTop ι) ↔ ω = (τ y).untopA
Tactic: classical
  rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
  suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
  ext1 ω
  simp only [Set.mem_setOf_eq, Finset.mem_filter, Finset.mem_singleton]
  constructor <;> intro h
  · simp [h.2]
  · simp only [h]
    specialize hbdd y
    have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
    lift τ y to ι using this with i hi
    simpa using hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
h : u (τ y).untopA y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
h₁ : u (τ y).untopA y = ∑ c ∈ s, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) y
h₂ h₃ h₄ : u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
h₅ : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
h₆ :
  ∀ (ω : ι),
    ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
      Membership.mem (γ := Finset ι) {(τ y).untopA} ω
h₇ : ∀ (ω : ι), ω ∈ s ∧ τ y = (↑ω : WithTop ι) ↔ ω = (τ y).untopA
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h₈ : ∀ (ω : ι) (h : ω ∈ s ∧ τ y = (↑ω : WithTop ι)), ω = (τ y).untopA
Tactic: classical
  rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
  suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
  ext1 ω
  simp only [Set.mem_setOf_eq, Finset.mem_filter, Finset.mem_singleton]
  constructor <;> intro h
  · simp [h.2]
  · simp only [h]
    specialize hbdd y
    have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
    lift τ y to ι using this with i hi
    simpa using hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
h : u (τ y).untopA y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
h₁ : u (τ y).untopA y = ∑ c ∈ s, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) y
h₂ h₃ h₄ : u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
h₅ : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
h₆ :
  ∀ (ω : ι),
    ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
      Membership.mem (γ := Finset ι) {(τ y).untopA} ω
h₇ : ∀ (ω : ι), ω ∈ s ∧ τ y = (↑ω : WithTop ι) ↔ ω = (τ y).untopA
h₈ : ∀ (ω : ι) (h : ω ∈ s ∧ τ y = (↑ω : WithTop ι)), ω = (τ y).untopA
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h₉ : ∀ (ω : ι) (h : ω = (τ y).untopA), ω ∈ s ∧ τ y = (↑ω : WithTop ι)
Tactic: classical
  rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
  suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
  ext1 ω
  simp only [Set.mem_setOf_eq, Finset.mem_filter, Finset.mem_singleton]
  constructor <;> intro h
  · simp [h.2]
  · simp only [h]
    specialize hbdd y
    have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
    lift τ y to ι using this with i hi
    simpa using hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
⊢ stoppedValue u τ = ∑ i ∈ Finset.Iic N, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
have refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
Tactic: refine stoppedValue_eq_of_mem_finset fun ω ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
have simp : ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = τ ω
Tactic: simp only [Finset.coe_Iic, Set.mem_image]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = τ ω
have hbdd₁ : τ ω ≤ (↑N : WithTop ι)
Tactic: specialize hbdd ω
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
⊢ ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = τ ω
have h_top : τ ω ≠ ⊤
Tactic: have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = τ ω
have lift : ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)),
  ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = (↑i : WithTop ι)
Tactic: lift τ ω to ι using h_top with i hi
Cleared hypotheses: hbdd, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
have h : ∀ (ω : Ω),
  stoppedProcess u τ n ω =
    HAdd.hAdd (β := (x : Ω) → E) (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n))
      (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
ω : Ω
⊢ stoppedProcess u τ n ω =
    HAdd.hAdd (β := (x : Ω) → E) (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n))
      (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) ω
have h : stoppedProcess u τ n ω =
  Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
    ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
Tactic: rw [Pi.add_apply, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
ω : Ω
⊢ stoppedProcess u τ n ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h : ∀ (h : (↑n : WithTop ι) ≤ τ ω),
  stoppedProcess u τ n ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
Tactic: rcases le_or_gt (n : WithTop ι) (τ ω) with h | h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 :
  ∀ (h : (↑n : WithTop ι) ≤ τ ω),
    stoppedProcess u τ n ω =
      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) ω
have h₁ : ∀ (h : τ ω < (↑n : WithTop ι)),
  stoppedProcess u τ n ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
Tactic: rcases le_or_gt (n : WithTop ι) (τ ω) with h | h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι) ≤ τ ω
⊢ stoppedProcess u τ n ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h₁ : ∀ x ∈ {i ∈ s | i < n}, Set.indicator {ω : Ω | τ ω = (↑x : WithTop ι)} (u x) ω = 0
Tactic: rw [stoppedProcess_eq_of_le h, Set.indicator_of_mem, Finset.sum_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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₁ : ∀ x ∈ {i ∈ s | i < n}, Set.indicator {ω : Ω | τ ω = (↑x : WithTop ι)} (u x) ω = 0
⊢ stoppedProcess u τ n ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h₂ : Membership.mem (γ := Set Ω) {a : Ω | (↑n : WithTop ι) ≤ τ a} ω
Tactic: rw [stoppedProcess_eq_of_le h, Set.indicator_of_mem, Finset.sum_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ∈ {i ∈ s | i < n}
⊢ Set.indicator {ω : Ω | τ ω = (↑m : WithTop ι)} (u m) ω = 0
have h₁ : ω ∉ {ω : Ω | τ ω = (↑m : WithTop ι)}
Tactic: refine Set.indicator_of_notMem ?_ _
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ∈ {i ∈ s | i < n}
⊢ ω ∉ {ω : Ω | τ ω = (↑m : WithTop ι)}
have hm₁ : m ∈ s ∧ m < n
Tactic: rw [Finset.mem_filter] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
have h₁ : (↑m : WithTop ι) < (↑n : WithTop ι)
Tactic: refine (lt_of_lt_of_le ?_ h).ne'
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ stoppedProcess u τ n ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h₁ : u (τ ω).untopA ω =
  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)]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ι)
⊢ u (τ ω).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h_top : τ ω ≠ ⊤
Tactic: have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 : τ ω ≠ ⊤
⊢ u (τ ω).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have hbdd₁ : τ ω ∈ WithTop.some '' (↑s : Set ι)
Tactic: specialize hbdd ω h
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ u (τ ω).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have 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) ω
Tactic: lift τ ω to ι using h_top with i hi
Cleared hypotheses: h, h_top, hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ u (↑i : WithTop ι).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h₁ : u (↑i : WithTop ι).untopA ω =
  Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω
Tactic: rw [Finset.sum_eq_single_of_mem i]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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) ω
⊢ u (↑i : WithTop ι).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h₂ : i ∈ {i ∈ s | i < n}
Tactic: rw [Finset.sum_eq_single_of_mem i]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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}
⊢ u (↑i : WithTop ι).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω +
      ∑ c ∈ s with c < n, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) ω
have h₃ : ∀ b ∈ {i ∈ s | i < n}, b ≠ i → Set.indicator {ω : Ω | τ ω = (↑b : WithTop ι)} (u b) ω = 0
Tactic: rw [Finset.sum_eq_single_of_mem i]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ u (↑i : WithTop ι).untopA ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω
have h₁ : u i ω = Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω
Tactic: simp only [untopD_coe]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ u i ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω
have h₁ : Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} ω
Tactic: rw [Set.indicator_of_notMem, zero_add, Set.indicator_of_mem]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)} ω
⊢ u i ω =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) ω + Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) ω
have h₂ : ω ∉ {a : Ω | (↑n : WithTop ι) ≤ τ a}
Tactic: rw [Set.indicator_of_notMem, zero_add, Set.indicator_of_mem]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι) ≤ τ ω
have h₁ : ¬(↑n : WithTop ι) ≤ (↑i : WithTop ι)
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ∈ {i ∈ s | i < n}
have h₁ : i ∈ s ∧ i < n
Tactic: rw [Finset.mem_filter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ∧ i < n
have hbdd₁ : i ∈ s
Tactic: simp only [Set.mem_image, Finset.mem_coe, coe_eq_coe, exists_eq_right] at hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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
⊢ Set.indicator {ω : Ω | τ ω = (↑b : WithTop ι)} (u b) ω = 0
have h₁ : ω ∉ {ω : Ω | τ ω = (↑b : WithTop ι)}
Tactic: rw [Set.indicator_of_notMem]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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
⊢ ω ∉ {ω : Ω | τ ω = (↑b : WithTop ι)}
have h₁ : ¬(↑i : WithTop ι) = (↑b : WithTop ι)
Tactic: rw [Set.mem_setOf, ← hi]