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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
⊢ Set.range τ ⊆ WithTop.some '' (↑s : Set ι)

Tactic:
have : Set.range τ ⊆ WithTop.some '' s := by
    rintro x ⟨y, rfl⟩
    exact hbdd y
-- 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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
this : Set.range τ ⊆ WithTop.some '' (↑s : Set ι)
⊢ (Set.range τ).Countable

Tactic:
((Finset.finite_toSet s).image _).subset this |>.countable

Premises used: Set.Finite.subset, Set.Finite.image, Finset.finite_toSet, Set.Finite.countable
-- 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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
this : Set.range τ ⊆ WithTop.some '' (↑s : Set ι)
⊢ (Set.range τ).Countable

Tactic:
exact ((Finset.finite_toSet s).image _).subset this |>.countable

Premises used: Set.Finite.subset, Set.Finite.image, Finset.finite_toSet, Set.Finite.countable
-- 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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
⊢ MemLp (stoppedValue u τ) p μ

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

Premises used: MeasureTheory.memLp_stoppedValue_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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
⊢ MemLp (stoppedValue u τ) p μ

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

Premises used: MeasureTheory.memLp_stoppedValue_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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ τ ω ≤ (↑N : WithTop ι)

Tactic:
specialize hbdd ω
-- 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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
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
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
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
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
h_top : τ ω ≠ ⊤
lift :
  ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (hbdd : (↑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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)
⊢ ∃ x ≤ 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
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)
⊢ ∃ x ≤ N, (↑x : WithTop ι) = (↑i : WithTop ι)

Tactic:
exact ⟨i, mod_cast hbdd, 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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
simp_rw : ∀ (hu : ∀ (n : ι), MemLp (u n) 1 μ), MemLp (stoppedValue u τ) 1 μ
⊢ Integrable (stoppedValue u τ) μ

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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedValue u τ) 1 μ

Tactic:
memLp_stoppedValue_of_mem_finset hτ hu hbdd

Premises used: MeasureTheory.memLp_stoppedValue_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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedValue u τ) 1 μ

Tactic:
exact memLp_stoppedValue_of_mem_finset hτ hu hbdd

Premises used: MeasureTheory.memLp_stoppedValue_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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
⊢ Integrable (stoppedValue u τ) μ

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

Premises used: MeasureTheory.integrable_stoppedValue_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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
⊢ Integrable (stoppedValue u τ) μ

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

Premises used: MeasureTheory.integrable_stoppedValue_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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ τ ω ≤ (↑N : WithTop ι)

Tactic:
specialize hbdd ω
-- 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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
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
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
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
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
h_top : τ ω ≠ ⊤
lift :
  ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (hbdd : (↑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 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)
⊢ ∃ x ≤ 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
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
ω : Ω
i : ι
hi : (↑i : WithTop ι) = τ ω
hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)
⊢ ∃ x ≤ N, (↑x : WithTop ι) = (↑i : WithTop ι)

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

Tactic:
rw [stoppedProcess_eq_of_mem_finset n hbdd]

Premises used: MeasureTheory.stoppedProcess_eq_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
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp
    (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i))
    p μ

Tactic:
MemLp.add ?_ ?_

Premises used: MeasureTheory.MemLp.add
-- 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_1 : MemLp (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n)) p μ
refine_2 : MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ
⊢ MemLp
    (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i))
    p μ

Tactic:
refine MemLp.add ?_ ?_

Premises used: MeasureTheory.MemLp.add
-- 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 ι)
⊢ MemLp (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n)) p μ

Tactic:
MemLp.indicator (ℱ.le n {a : Ω | n ≤ τ a} (hτ.measurableSet_ge n)) (hu n)

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_ge, LE.le, WithTop.some, MeasureTheory.Filtration.le, 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 ι)
⊢ MemLp (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n)) p μ

Tactic:
exact MemLp.indicator (ℱ.le n {a : Ω | n ≤ τ a} (hτ.measurableSet_ge n)) (hu n)

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_ge, LE.le, WithTop.some, MeasureTheory.Filtration.le, 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 ι)
this :
  MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
⊢ MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ

Tactic:
this
-- 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 ι)
this :
  MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
h :
  Eq (α := Ω → E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) fun (ω : Ω) ↦
    ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω
⊢ MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ

Tactic:
convert! this using 1
-- 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 ι)
this :
  MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
h :
  ∀ (ω : Ω),
    Eq.{u_4 + 1} (α := E) ((∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) ω)
      (∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω)
⊢ Eq (α := Ω → E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) fun (ω : Ω) ↦
    ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω

Tactic:
ext1 ω
-- 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 ι)
this :
  MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
ω : Ω
⊢ Eq.{u_4 + 1} (α := E) ((∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) ω)
    (∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω)

Tactic:
simp only [Finset.sum_apply]

Premises used: Finset.sum_apply
-- 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 :
  MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
⊢ MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ

Tactic:
suffices MemLp (fun ω => ∑ i ∈ s with i < n, {a : Ω | τ a = i}.indicator (u i) ω) p μ by
      convert! this using 1; ext1 ω; simp only [Finset.sum_apply]
-- 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 ι)
⊢ MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ

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

Premises used: MeasureTheory.memLp_finsetSum, MeasureTheory.MemLp.indicator