awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ ∃ x ≤ n, (↑x : WithTop ι) = τ ω
have lift : ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (h : (↑i : WithTop ι) < (↑n : WithTop ι)),
  ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)
Tactic: lift τ ω to ι using h_top with i hi
Cleared hypotheses: h, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
⊢ stoppedValue u π - stoppedValue u τ = fun (ω : Ω) ↦
    (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω
have h : ∀ (ω : Ω),
  (stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
ω : Ω
⊢ (stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω
have h_le' : untopA (τ ω) ≤ untopA (π ω)
Tactic: have h_le' : (τ ω).untopA ≤ (π ω).untopA := untopA_mono (mod_cast hπ ω) (hle ω)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
ω : Ω
h_le' : untopA (τ ω) ≤ untopA (π ω)
⊢ (stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω
have h : (stoppedValue u π - stoppedValue u τ) ω = (u (untopA (π ω)) - u 0 - (u (untopA (τ ω)) - u 0)) ω
Tactic: rw [Finset.sum_Ico_eq_sub _ h_le', Finset.sum_range_sub, Finset.sum_range_sub]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
ω : Ω
h : π ω = ⊤
⊢ False
have hbdd₁ : π ω ≤ (↑N : ℕ∞)
Tactic: specialize hbdd ω
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ stoppedValue u π - stoppedValue u τ = fun (ω : Ω) ↦
    (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω
have hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
Tactic: have hπ_top ω : π ω ≠ ⊤ := fun h ↦ by specialize hbdd ω; simp [h] at hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
⊢ stoppedValue u π - stoppedValue u τ = fun (ω : Ω) ↦
    (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω
have hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
Tactic: have hτ_top ω : τ ω ≠ ⊤ := ne_top_of_le_ne_top (hπ_top ω) (mod_cast hle ω)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ stoppedValue u π - stoppedValue u τ = fun (ω : Ω) ↦
    (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω
have rw : Eq (α := Ω → β) (fun (ω : Ω) ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) fun (ω : Ω) ↦
  (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω
Tactic: rw [stoppedValue_sub_eq_sum hle]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
rw :
  Eq (α := Ω → β) (fun (ω : Ω) ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) fun (ω : Ω) ↦
    (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω
⊢ stoppedValue u π - stoppedValue u τ = fun (ω : Ω) ↦
    (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω
have rw₁ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
Tactic: rw [stoppedValue_sub_eq_sum hle]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ Eq (α := Ω → β) (fun (ω : Ω) ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) fun (ω : Ω) ↦
    (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω
have h : ∀ (ω : Ω),
  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: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
⊢ 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)) ω)
have 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) ω)
Tactic: simp only [Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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) ω)
have h : Finset.Ico (untopA (τ ω)) (untopA (π ω)) =
  {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}
Tactic: refine Finset.sum_congr ?_ fun _ _ => rfl
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
⊢ Finset.Ico (untopA (τ ω)) (untopA (π ω)) =
    {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}
have h : ∀ (i : ℕ),
  i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)) ↔
    i ∈ {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}
Tactic: ext i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
⊢ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)) ↔
    i ∈ {i ∈ Finset.range (N + 1) | Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} ω}
have h : untopA (τ ω) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω
Tactic: simp only [Finset.mem_filter, Set.mem_setOf_eq, Finset.mem_range, Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
⊢ untopA (τ ω) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω
have hbdd₁ : π ω ≤ (↑N : ℕ∞)
Tactic: specialize hbdd ω
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
hbdd : π ω ≤ (↑N : ℕ∞)
⊢ untopA (τ ω) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω
have h : ∀ (t : ℕ) (ht : (↑t : ℕ∞) = τ ω),
  untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω
Tactic: lift τ ω to ℕ using hτ_top ω with t ht
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i : ℕ
hbdd : π ω ≤ (↑N : ℕ∞)
t : ℕ
ht : (↑t : ℕ∞) = τ ω
⊢ untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (π ω) ↔ i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω
have 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 : ℕ∞)
Tactic: lift π ω to ℕ using hπ_top ω with b hb
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 : ℕ∞)
⊢ untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (↑b : ℕ∞) ↔
    i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑b : ℕ∞)
have hbdd₁ : b ≤ N
Tactic: simp only [Nat.cast_le] at hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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
⊢ untopA (↑t : ℕ∞) ≤ i ∧ i < untopA (↑b : ℕ∞) ↔
    i < N + 1 ∧ LE.le (α := ℕ∞) (↑t : ℕ∞) (↑i : ℕ∞) ∧ LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑b : ℕ∞)
have h : t ≤ i → i < b → i ≤ N
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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
have refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
Tactic: refine stoppedValue_eq_of_mem_finset fun ω ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : ℕ∞)
ω : Ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
have hbdd₁ : τ ω ≤ (↑N : ℕ∞)
Tactic: specialize hbdd ω
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
hbdd : τ ω ≤ (↑N : ℕ∞)
⊢ τ ω ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
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_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
hbdd : τ ω ≤ (↑N : ℕ∞)
h_top : τ ω ≠ ⊤
⊢ τ ω ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
have lift : ∀ (t : ℕ) (ht : (↑t : ℕ∞) = τ ω) (hbdd : LE.le (α := ℕ∞) (↑t : ℕ∞) (↑N : ℕ∞)),
  (↑t : ℕ∞) ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
Tactic: lift τ ω to ℕ using h_top with t ht
Cleared hypotheses: hbdd, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : (↑t : ℕ∞) = τ ω
hbdd : LE.le (α := ℕ∞) (↑t : ℕ∞) (↑N : ℕ∞)
⊢ (↑t : ℕ∞) ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
have hbdd₁ : t ≤ N
Tactic: simp only [Nat.cast_le] at hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : (↑t : ℕ∞) = τ ω
hbdd : t ≤ N
⊢ (↑t : ℕ∞) ∈ WithTop.some '' (↑(Finset.range (N + 1)) : Set ℕ)
have simp : t < N + 1
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]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i)
have 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)
Tactic: rw [stoppedProcess_eq'' n]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
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)
have e_a : ∀ (i : ℕ), i ∈ Finset.Iio n ↔ i ∈ Finset.range n
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n i : ℕ
⊢ i ∈ Finset.Iio n ↔ i ∈ Finset.range n
have e_a : i < n ↔ i ∈ Finset.range n
Tactic: rw [Finset.mem_Iio, Finset.mem_range]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n i : ℕ
e_a : i < n ↔ i ∈ Finset.range n
⊢ i ∈ Finset.Iio n ↔ i ∈ Finset.range n
have e_a₁ : i < n ↔ i < n
Tactic: rw [Finset.mem_Iio, Finset.mem_range]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
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
have h : Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) x =
  Set.indicator ({a : Ω | τ a = (↑n : ℕ∞)} ∪ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}) (u n) x
Tactic: rw [add_comm, Pi.add_apply, ← Set.indicator_union_of_notMem_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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
⊢ 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
have h₁ : x ∉ {a : Ω | τ a = (↑n : ℕ∞)} ∩ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}
Tactic: rw [add_comm, Pi.add_apply, ← Set.indicator_union_of_notMem_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
⊢ Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) x =
    Set.indicator ({a : Ω | τ a = (↑n : ℕ∞)} ∪ {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a}) (u n) x
have 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
Tactic: simp_rw [@eq_comm _ _ (n : WithTop ℕ), @le_iff_eq_or_lt _ _ (n : WithTop ℕ)]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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}
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} ω ↔
    Membership.mem (γ := Set Ω) {a : Ω | (↑n : ℕ∞) < τ a} ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x ω : Ω
t : ℕ
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑t : ℕ∞) ↔ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑t : ℕ∞)
have h : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑t : ℕ∞) ↔ n < t
Tactic: simp only [Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x ω : Ω
t : ℕ
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑t : ℕ∞) ↔ n < t
have h : n + 1 ≤ t ↔ n < t
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x ω : Ω
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ ω ↔ (↑n : ℕ∞) < τ ω
have h : ∀ (x : ℕ∞), HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ x ↔ (↑n : ℕ∞) < x
Tactic: cases τ ω with
        | top => simp
        | coe t =>
          simp only [Nat.cast_lt]
          norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
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
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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}
⊢ 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
have 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
Tactic: rw [this, Set.setOf_or]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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
⊢ 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
have 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
Tactic: rw [this, Set.setOf_or]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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
⊢ False
have h₃ : τ x = (↑n : ℕ∞)
Tactic: rw [Set.mem_setOf] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 : ℕ∞)
⊢ False
have h₄ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ x
Tactic: rw [Set.mem_setOf] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = (↑n : ℕ∞)
h₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ x
⊢ False
have h₃ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑n : ℕ∞)
Tactic: rw [h₁] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = (↑n : ℕ∞)
h₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ (↑n : ℕ∞)
⊢ False
have h₃ : n + 1 ≤ n
Tactic: norm_cast at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
⊢ 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)
have 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)
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