awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
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 ∩ {ω : Ω | τ ω = ⊤}
refine_2 : MeasurableSet.{u_1} (α := Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Stopping
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 ∩ {ω : Ω | τ ω = ⊤})

Tactic:
MeasurableSet.inter (ht.preimage ?_) hτ.measurableSet_eq_top

Premises used: MeasurableSet.preimage, MeasureTheory.IsStoppingTime.measurableSet_eq_top, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
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 ∩ {ω : Ω | τ ω = ⊤}
refine_2 : Measurable.{u_1, u_2} (β := β) fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω
⊢ MeasurableSet.{u_1} (α := Ω) ((fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω : Ω | τ ω = ⊤})

Tactic:
refine MeasurableSet.inter (ht.preimage ?_) hτ.measurableSet_eq_top

Premises used: MeasurableSet.preimage, MeasureTheory.IsStoppingTime.measurableSet_eq_top, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
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 ∩ {ω : Ω | τ ω = ⊤}
⊢ Measurable.{u_1, u_2} (β := β) fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω

Tactic:
(hf_prog.stronglyAdapted (Classical.arbitrary ι)).measurable.mono
      (f.le (Classical.arbitrary ι)) le_rfl

Premises used: le_rfl, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.IsStronglyProgressive.stronglyAdapted, Classical.arbitrary, MeasureTheory.Filtration.le, Measurable.mono
-- Module: Mathlib.Probability.Process.Stopping
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 ∩ {ω : Ω | τ ω = ⊤}
⊢ Measurable.{u_1, u_2} (β := β) fun (ω : Ω) ↦ u (Classical.arbitrary ι) ω

Tactic:
exact (hf_prog.stronglyAdapted (Classical.arbitrary ι)).measurable.mono
      (f.le (Classical.arbitrary ι)) le_rfl

Premises used: le_rfl, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.IsStronglyProgressive.stronglyAdapted, Classical.arbitrary, MeasureTheory.Filtration.le, Measurable.mono
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
h : ∀ (y : Ω), stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y
⊢ stoppedValue u τ = ∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)

Tactic:
ext y
-- Module: Mathlib.Probability.Process.Stopping
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 with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y
⊢ stoppedValue u τ y = (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) y

Tactic:
rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]

Premises used: MeasureTheory.stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter
-- Module: Mathlib.Probability.Process.Stopping
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
rw₁ rw₂ : u (τ y).untopA y = u (τ y).untopA y
⊢ u (τ y).untopA y = ∑ i ∈ s with Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y, u i y

Tactic:
rw [this, Finset.sum_singleton]

Premises used: Finset.sum_singleton
-- Module: Mathlib.Probability.Process.Stopping
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 : {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

Tactic:
suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
-- Module: Mathlib.Probability.Process.Stopping
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 :
  ∀ (ω : ι),
    ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
      Membership.mem (γ := Finset ι) {(τ y).untopA} ω
⊢ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} = {(τ y).untopA}

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
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
⊢ ω ∈ {i ∈ s | Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} y} ↔
    Membership.mem (γ := Finset ι) {(τ y).untopA} ω

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

Premises used: Finset.mem_singleton, Set.mem_setOf_eq, 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 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
ω : ι
h : ω ∈ s ∧ τ y = (↑ω : WithTop ι) → ω = (τ y).untopA
h₁ : ω = (τ y).untopA → ω ∈ s ∧ τ y = (↑ω : WithTop ι)
⊢ ω ∈ s ∧ τ y = (↑ω : WithTop ι) ↔ ω = (τ y).untopA

Tactic:
constructor
-- Module: Mathlib.Probability.Process.Stopping
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

Tactic:
simp [h.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 : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
y : Ω
ω : ι
h : ω = (τ y).untopA
h₁ : (τ y).untopA ∈ s ∧ τ y = (↑(τ y).untopA : WithTop ι)
⊢ ω ∈ s ∧ τ y = (↑ω : WithTop ι)

Tactic:
simp only [h]
-- Module: Mathlib.Probability.Process.Stopping
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 ∈ WithTop.some '' (↑s : Set ι)

Tactic:
specialize hbdd y
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
h_contra : τ y = ⊤
⊢ False

Tactic:
simp [h_contra] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
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 ≠ ⊤

Tactic:
have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
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 ≠ ⊤

Tactic:
this
-- Module: Mathlib.Probability.Process.Stopping
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 ≠ ⊤
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 ι)
⊢ (τ y).untopA ∈ s ∧ τ y = (↑(τ y).untopA : WithTop ι)

Tactic:
lift τ y to ι using this 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 : AddCommMonoid E
s : Finset ι
y : Ω
ω 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:
simpa using hbdd
-- Module: Mathlib.Probability.Process.Stopping
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
h₉ h₁₀ : ∀ (ω : ι) (h : ω = (τ y).untopA), ω ∈ s ∧ τ y = (↑ω : WithTop ι)
⊢ stoppedValue u τ 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

Premises used: Finset.mem_singleton, MeasureTheory.stoppedValue, Finset.sum_apply, Set.mem_setOf_eq, Finset.sum_indicator_eq_sum_filter, 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 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
⊢ stoppedValue u τ = ∑ i ∈ Finset.Iic N, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)

Tactic:
stoppedValue_eq_of_mem_finset fun ω ↦ ?_

Premises used: MeasureTheory.stoppedValue_eq_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
⊢ stoppedValue u τ = ∑ i ∈ Finset.Iic N, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)

Tactic:
refine stoppedValue_eq_of_mem_finset fun ω ↦ ?_

Premises used: MeasureTheory.stoppedValue_eq_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
simp : ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = τ ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)

Tactic:
simp only [Finset.coe_Iic, Set.mem_image]

Premises used: Finset.coe_Iic, Set.mem_image
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
ω : Ω
⊢ τ ω ≤ (↑N : WithTop ι)

Tactic:
specialize hbdd ω
-- Module: Mathlib.Probability.Process.Stopping
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_contra : τ ω = ⊤
⊢ False

Tactic:
simp [h_contra] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
⊢ τ ω ≠ ⊤

Tactic:
have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
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 : τ ω ≠ ⊤
⊢ τ ω ≠ ⊤

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 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
h_top : τ ω ≠ ⊤
lift :
  ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)),
    ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = (↑i : WithTop ι)
⊢ ∃ x ∈ Set.Iic 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 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)
⊢ ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
⟨i, mod_cast hbdd, rfl⟩

Premises used: WithTop.coe_le_coe._simp_1, cast, 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 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
N : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)
⊢ ∃ x ∈ Set.Iic N, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
exact ⟨i, mod_cast hbdd, 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 : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
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)) ω
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)

Tactic:
ext ω
-- 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 :
  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 ω =
    HAdd.hAdd (β := (x : Ω) → E) (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n))
      (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) ω

Tactic:
rw [Pi.add_apply, Finset.sum_apply]

Premises used: Finset.sum_apply, Pi.add_apply
-- 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 :
  ∀ (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) ω
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) ω

Tactic:
rcases le_or_gt (n : WithTop ι) (τ ω) with h | h

Premises used: WithTop.some, le_or_gt
-- 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₁ : ∀ x ∈ {i ∈ s | i < n}, Set.indicator {ω : Ω | τ ω = (↑x : WithTop ι)} (u x) ω = 0
h₂ : Membership.mem (γ := Set Ω) {a : Ω | (↑n : WithTop ι) ≤ τ a} ω
⊢ 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_le h, Set.indicator_of_mem, Finset.sum_eq_zero, add_zero]

Premises used: Finset.sum_eq_zero, MeasureTheory.stoppedProcess_eq_of_le, Set.indicator_of_mem, add_zero
-- 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 ∈ {i ∈ s | i < n}
⊢ Set.indicator {ω : Ω | τ ω = (↑m : WithTop ι)} (u m) ω = 0

Tactic:
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 : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
m : ι
hm : m ∈ {i ∈ s | i < n}
h₁ : ω ∉ {ω : Ω | τ ω = (↑m : WithTop ι)}
⊢ Set.indicator {ω : Ω | τ ω = (↑m : WithTop ι)} (u m) ω = 0

Tactic:
refine 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 : ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
ω : Ω
h : (↑n : WithTop ι) ≤ τ ω
m : ι
hm : m ∈ {i ∈ s | i < n}
⊢ m ∈ s ∧ m < n

Tactic:
rw [Finset.mem_filter] at hm

Premises used: Finset.mem_filter