awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
refine_2 : ∀ i ∈ {i ∈ s | i < n}, MeasurableSet.{u_1} (α := Ω) {a : Ω | τ a = (↑i : WithTop ι)}
⊢ MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ

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

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

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

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

Tactic:
exact ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq i)

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_eq, WithTop.some, MeasureTheory.Filtration.le, Eq
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
⊢ MemLp (stoppedProcess u τ n) p μ

Tactic:
memLp_stoppedProcess_of_mem_finset hτ hu n (s := Finset.Iic n) fun ω h => ?_

Premises used: MeasureTheory.memLp_stoppedProcess_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
refine : ∀ (ω : Ω) (h : τ ω < (↑n : WithTop ι)), τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)
⊢ MemLp (stoppedProcess u τ n) p μ

Tactic:
refine memLp_stoppedProcess_of_mem_finset hτ hu n (s := Finset.Iic n) fun ω h => ?_

Premises used: MeasureTheory.memLp_stoppedProcess_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
simp : ∃ x ≤ n, (↑x : WithTop ι) = τ ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)

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

Premises used: Finset.coe_Iic, Set.mem_image, Set.mem_Iic
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_contra : τ ω = ⊤
⊢ False

Tactic:
simp [h_contra] at h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
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 : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ τ ω ≠ ⊤

Tactic:
have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
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 : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ τ ω ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
lift :
  ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (h : (↑i : WithTop ι) < (↑n : WithTop ι)),
    ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = τ ω

Tactic:
lift τ ω to ι using h_top with i hi
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
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 : ι), MemLp (u n) p μ
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
⟨i, mod_cast h.le, rfl⟩

Premises used: WithTop.coe_le_coe._simp_1, cast, LT.lt.le, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
exact ⟨i, mod_cast h.le, rfl⟩
-- Module: Mathlib.Probability.Process.Stopping
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
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
simp_rw : ∀ (hu : ∀ (n : ι), MemLp (u n) 1 μ), MemLp (stoppedProcess u τ n) 1 μ
⊢ Integrable (stoppedProcess u τ n) μ

Tactic:
simp_rw [← memLp_one_iff_integrable] at hu ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.Process.Stopping
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
hτ : IsStoppingTime ℱ τ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedProcess u τ n) 1 μ

Tactic:
memLp_stoppedProcess_of_mem_finset hτ hu n hbdd

Premises used: MeasureTheory.memLp_stoppedProcess_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedProcess u τ n) 1 μ

Tactic:
exact memLp_stoppedProcess_of_mem_finset hτ hu n hbdd

Premises used: MeasureTheory.memLp_stoppedProcess_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
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 : ι
⊢ Integrable (stoppedProcess u τ n) μ

Tactic:
integrable_stoppedProcess_of_mem_finset hτ hu n (s := Finset.Iic n) fun ω h => ?_

Premises used: MeasureTheory.integrable_stoppedProcess_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
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 : ι
refine : ∀ (ω : Ω) (h : τ ω < (↑n : WithTop ι)), τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)
⊢ Integrable (stoppedProcess u τ n) μ

Tactic:
refine integrable_stoppedProcess_of_mem_finset hτ hu n (s := Finset.Iic n) fun ω h => ?_

Premises used: MeasureTheory.integrable_stoppedProcess_of_mem_finset
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
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 ι)
simp : ∃ x ≤ n, (↑x : WithTop ι) = τ ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)

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

Premises used: Finset.coe_Iic, Set.mem_image, Set.mem_Iic
-- Module: Mathlib.Probability.Process.Stopping
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_contra : τ ω = ⊤
⊢ False

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

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

Tactic:
h_top
-- Module: Mathlib.Probability.Process.Stopping
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 : τ ω ≠ ⊤
lift :
  ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (h : (↑i : WithTop ι) < (↑n : WithTop ι)),
    ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = τ ω

Tactic:
lift τ ω to ι using h_top with i hi
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
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 : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
⟨i, mod_cast h.le, rfl⟩

Premises used: WithTop.coe_le_coe._simp_1, cast, LT.lt.le, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Process.Stopping
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 : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
h : (↑i : WithTop ι) < (↑n : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
exact ⟨i, mod_cast h.le, rfl⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : Nonempty ι
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : SecondCountableTopology ι
inst_6 : OrderTopology ι
inst_7 : MeasurableSpace ι
inst_8 : BorelSpace ι
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
inst_9 : MetrizableSpace ι
hu : StronglyAdapted (β := fun (i : ι) ↦ β) f u
hu_cont : ∀ (ω : Ω), Continuous[inst_4, inst] fun (i : ι) ↦ u i ω
hτ : IsStoppingTime f τ
⊢ StronglyAdapted (β := fun (a : ι) ↦ β) f (MeasureTheory.stoppedProcess u τ)

Tactic:
((hu.isStronglyProgressive_of_continuous hu_cont).stoppedProcess hτ).stronglyAdapted

Premises used: MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous, MeasureTheory.IsStronglyProgressive.stronglyAdapted, MeasureTheory.IsStronglyProgressive.stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : Nonempty ι
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : SecondCountableTopology ι
inst_6 : OrderTopology ι
inst_7 : MeasurableSpace ι
inst_8 : BorelSpace ι
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
inst_9 : DiscreteTopology ι
hu : StronglyAdapted (β := fun (i : ι) ↦ β) f u
hτ : IsStoppingTime f τ
⊢ StronglyAdapted (β := fun (a : ι) ↦ β) f (MeasureTheory.stoppedProcess u τ)

Tactic:
(hu.isStronglyProgressive_of_discrete.stoppedProcess hτ).stronglyAdapted

Premises used: MeasureTheory.IsStronglyProgressive.stronglyAdapted, MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete, MeasureTheory.IsStronglyProgressive.stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : Nonempty ι
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : SecondCountableTopology ι
inst_6 : OrderTopology ι
inst_7 : MeasurableSpace ι
inst_8 : BorelSpace ι
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
inst_9 : MetrizableSpace ι
hu : StronglyAdapted (β := fun (i : ι) ↦ β) f u
hu_cont : ∀ (ω : Ω), Continuous[inst_4, inst] fun (i : ι) ↦ u i ω
hτ : IsStoppingTime f τ
n : ι
⊢ StronglyMeasurable (MeasureTheory.stoppedProcess u τ n)

Tactic:
(hu.isStronglyProgressive_of_continuous hu_cont).stronglyMeasurable_stoppedProcess hτ n

Premises used: MeasureTheory.IsStronglyProgressive.stronglyMeasurable_stoppedProcess, MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : Nonempty ι
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : SecondCountableTopology ι
inst_6 : OrderTopology ι
inst_7 : MeasurableSpace ι
inst_8 : BorelSpace ι
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
inst_9 : DiscreteTopology ι
hu : StronglyAdapted (β := fun (i : ι) ↦ β) f u
hτ : IsStoppingTime f τ
n : ι
⊢ StronglyMeasurable (MeasureTheory.stoppedProcess u τ n)

Tactic:
hu.isStronglyProgressive_of_discrete.stronglyMeasurable_stoppedProcess hτ n

Premises used: MeasureTheory.IsStronglyProgressive.stronglyMeasurable_stoppedProcess, MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
h :
  ∀ (ω : Ω),
    (stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω
⊢ stoppedValue u π - stoppedValue u τ = fun (ω : Ω) ↦
    (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
ω : Ω
⊢ untopA (τ ω) ≤ untopA (π ω)

Tactic:
have h_le' : (τ ω).untopA ≤ (π ω).untopA := untopA_mono (mod_cast hπ ω) (hle ω)
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
ω : Ω
h_le' : untopA (τ ω) ≤ untopA (π ω)
h : (stoppedValue u π - stoppedValue u τ) ω = (u (untopA (π ω)) - u 0 - (u (untopA (τ ω)) - u 0)) ω
⊢ (stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω

Tactic:
rw [Finset.sum_Ico_eq_sub _ h_le', Finset.sum_range_sub, Finset.sum_range_sub]

Premises used: Finset.sum_Ico_eq_sub, Finset.sum_range_sub
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
ω : Ω
h_le' : untopA (τ ω) ≤ untopA (π ω)
⊢ (stoppedValue u π - stoppedValue u τ) ω = (u (untopA (π ω)) - u 0 - (u (untopA (τ ω)) - u 0)) ω

Tactic:
simp [stoppedValue]

Premises used: MeasureTheory.stoppedValue
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
ω : Ω
h : π ω = ⊤
⊢ π ω ≤ (↑N : ℕ∞)

Tactic:
specialize hbdd ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
ω : Ω
h : π ω = ⊤
hbdd : π ω ≤ (↑N : ℕ∞)
⊢ False

Tactic:
simp [h] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ ∀ (ω : Ω), π ω ≠ ⊤

Tactic:
have hπ_top ω : π ω ≠ ⊤ := fun h ↦ by specialize hbdd ω; simp [h] at hbdd
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
⊢ ∀ (ω : Ω), τ ω ≠ ⊤

Tactic:
have hτ_top ω : τ ω ≠ ⊤ := ne_top_of_le_ne_top (hπ_top ω) (mod_cast hle ω)
-- Module: Mathlib.Probability.Process.Stopping
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)) ω
rw₁ : ∀ (ω : Ω), (↑(π ω) : ℝ≥0∞) ≠ ∞
⊢ stoppedValue u π - stoppedValue u τ = fun (ω : Ω) ↦
    (∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (u (i + 1) - u i)) ω

Tactic:
rw [stoppedValue_sub_eq_sum hle]

Premises used: MeasureTheory.stoppedValue_sub_eq_sum
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
⊢ (↑(π ω) : ℝ≥0∞) ≠ ∞

Tactic:
mod_cast hπ_top ω

Premises used: ENat.toENNReal_eq_top._simp_1, congrArg, cast, Eq.symm, Not
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
⊢ (↑(π ω) : ℝ≥0∞) ≠ ∞

Tactic:
exact mod_cast hπ_top ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
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)) ω)
⊢ 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:
ext ω