awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t_1 : Set β
ht : MeasurableSet t_1
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
h : stoppedValue u τ ω ∈ t_1
t : ι
⊢ ∃ (x : ℕ), t ≤ seq x
have neg : ∀ (h_seq_tendsto : ∀ (b : ι), ∀ᶠ (a : ℕ) in atTop, b ≤ seq a) (ω : Ω),
  stoppedValue u τ ω ∈ t_1 → ∀ (t : ι), ∃ (x : ℕ), t ≤ seq x
Tactic: rw [tendsto_atTop] at h_seq_tendsto
Cleared hypotheses: h_seq_tendsto, ω, h, t
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)
have this : stoppedValue u τ ⁻¹' t =
  (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
    stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
Tactic: have : stoppedValue u τ ⁻¹' t
      = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ seq n})
        ∪ (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}) := by
    ext1 ω
    simp only [Set.mem_preimage, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq,
      exists_and_left]
    rw [← and_or_left, iff_self_and]
    intro _
    by_cases h : τ ω = ⊤
    · exact .inr h
    · lift τ ω to ι using h with t
      simp only [coe_le_coe, coe_ne_top, or_false]
      rw [tendsto_atTop] at h_seq_tendsto
      exact (h_seq_tendsto t).exists
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)
have rw : MeasurableSet
  ((⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
    stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet
    ((⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
have refine_1 : MeasurableSet.{u_1} (α := Ω) (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)})
Tactic: refine MeasurableSet.union ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
refine_1 : MeasurableSet.{u_1} (α := Ω) (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)})
⊢ MeasurableSet
    ((⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
have refine_2 : MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
Tactic: refine MeasurableSet.union ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} = (fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
have h : ∀ (ω : Ω),
  ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} ↔
    Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
ω : Ω
⊢ ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} ↔
    Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}) ω
have h : τ ω = ⊤ → (u (untopD (Classical.arbitrary ι) (τ ω)) ω ∈ t ↔ u (Classical.arbitrary ι) ω ∈ t)
Tactic: simp only [Set.mem_inter_iff, Set.mem_preimage, stoppedValue, untopA,
        Set.mem_setOf_eq, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
have this₁ : stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} = (fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
Tactic: have : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
       = (fun ω ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω | τ ω = ⊤} := by
      ext ω
      simp only [Set.mem_inter_iff, Set.mem_preimage, stoppedValue, untopA,
        Set.mem_setOf_eq, and_congr_left_iff]
      intro h
      simp [h]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this_1 :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
this :
  stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} = (fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
have refine_2 : MeasurableSet.{u_1} (α := Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
inst_7 : TopologicalSpace β
f : Filtration ι m
inst_8 : PseudoMetrizableSpace β
inst_9 : MeasurableSpace β
inst_10 : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι))
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this_1 :
  stoppedValue u τ ⁻¹' t =
    (⋃ (n : ℕ), stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ (↑(seq n) : WithTop ι)}) ∪
      stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
this :
  stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤} = (fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤}
⊢ MeasurableSet.{u_1} (α := Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
have refine_2 : Measurable.{u_1, u_2} (β := β) fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω
Tactic: refine MeasurableSet.inter (ht.preimage ?_) hτ.measurableSet_eq_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 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ stoppedValue u τ = ∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
have h : ∀ (y : Ω), stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
Tactic: ext y
-- 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 : Ω
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h : u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
Tactic: rw [stoppedValue, 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_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
this : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
⊢ u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
have rw : u (τ y).untopA y = ∑ i ∈ {(τ y).untopA}, u i y
Tactic: rw [this, Finset.sum_singleton]
-- 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 : Ω
this : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
rw : u (τ y).untopA y = ∑ i ∈ {(τ y).untopA}, u i y
⊢ u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
have rw₁ : u (τ y).untopA y = u (τ y).untopA y
Tactic: rw [this, Finset.sum_singleton]
-- 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 : Ω
⊢ u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
have h : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
Tactic: suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
-- 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 : Ω
⊢ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}
have h : ∀ (ω : ι),
  ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
    Membership.mem (γ := Finset ι) {(τ y).untopA} ω
Tactic: ext1 ω
-- 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 : Ω
ω : ι
⊢ ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
    Membership.mem (γ := Finset ι) {(τ y).untopA} ω
have h : ω ∈ s ∧ τ y = (↑ω : WithTop ι) ↔ ω = (τ y).untopA
Tactic: simp only [Set.mem_setOf_eq, Finset.mem_filter, Finset.mem_singleton]
-- 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 : Ω
ω : ι
⊢ ω ∈ s ∧ τ y = (↑ω : WithTop ι) ↔ ω = (τ y).untopA
have h : ω ∈ s ∧ τ y = (↑ω : WithTop ι) → ω = (τ y).untopA
Tactic: constructor
-- 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 : ω ∈ s ∧ τ y = (↑ω : WithTop ι) → ω = (τ y).untopA
⊢ ω ∈ s ∧ τ y = (↑ω : WithTop ι) ↔ ω = (τ y).untopA
have h₁ : ω = (τ y).untopA → ω ∈ s ∧ τ y = (↑ω : WithTop ι)
Tactic: constructor
-- 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 : ω = (τ y).untopA
⊢ ω ∈ s ∧ τ y = (↑ω : WithTop ι)
have h₁ : (τ y).untopA ∈ s ∧ τ y = (↑(τ y).untopA : WithTop ι)
Tactic: simp only [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 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
ω : ι
h : ω = (τ y).untopA
⊢ (τ y).untopA ∈ s ∧ τ y = (↑(τ y).untopA : WithTop ι)
have hbdd₁ : τ y ∈ WithTop.some '' (↑s : Set ι)
Tactic: specialize hbdd y
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 : AddCommMonoid E
s : Finset ι
y : Ω
ω : ι
h : ω = (τ y).untopA
hbdd : τ y ∈ WithTop.some '' (↑s : Set ι)
⊢ (τ y).untopA ∈ s ∧ τ y = (↑(τ y).untopA : WithTop ι)
have this : τ y ≠ ⊤
Tactic: have : τ y ≠ ⊤ := 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 : AddCommMonoid E
s : Finset ι
y : Ω
ω : ι
h : ω = (τ y).untopA
hbdd : τ y ∈ WithTop.some '' (↑s : Set ι)
this : τ y ≠ ⊤
⊢ (τ y).untopA ∈ s ∧ τ y = (↑(τ y).untopA : WithTop ι)
have h₁ : ∀ (i : ι) (hi : (↑i : WithTop ι) = τ y) (h : ω = (↑i : WithTop ι).untopA)
  (hbdd : (↑i : WithTop ι) ∈ WithTop.some '' (↑s : Set ι)),
  (↑i : WithTop ι).untopA ∈ s ∧ (↑i : WithTop ι) = (↑(↑i : WithTop ι).untopA : WithTop ι)
Tactic: lift τ y to ι using this with i hi
Cleared hypotheses: h, hbdd, this
-- 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 : Ω
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h : u (τ y).untopA y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
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
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h₁ : u (τ y).untopA y = ∑ c ∈ s, Set.indicator {ω : Ω | τ ω = (↑c : WithTop ι)} (u c) y
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
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h₂ : u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
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
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
have h₅ : {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ 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