awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h_1 : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i : WithTop ι
hi : i ∈ Set.range τ
h : i = ⊤
⊢ ∃ (y : Ω), τ y = ⊤

Tactic:
simp only [h, Set.mem_range] at hi

Premises used: Set.mem_range
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h_1 : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i : WithTop ι
h : i = ⊤
hi : ∃ (y : Ω), τ y = ⊤
obtain : ∀ (ω : Ω) (hω : τ ω = ⊤), False
⊢ False

Tactic:
obtain ⟨ω, hω⟩ := hi
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h_1 : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i : WithTop ι
h : i = ⊤
ω : Ω
hω : τ ω = ⊤
⊢ τ ω ≤ (↑n : WithTop ι)

Tactic:
specialize hτ_le ω
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h_1 : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le_1 : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i : WithTop ι
h : i = ⊤
ω : Ω
hω : τ ω = ⊤
hτ_le : τ ω ≤ (↑n : WithTop ι)
⊢ False

Tactic:
simp [hω] at hτ_le
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i : WithTop ι
hi : i ∈ Set.range τ
⊢ i ≠ ⊤

Tactic:
have h_top : i ≠ ⊤ := fun h ↦ by
    simp only [h, Set.mem_range] at hi
    obtain ⟨ω, hω⟩ := hi
    specialize hτ_le ω
    simp [hω] at hτ_le
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i : WithTop ι
hi : i ∈ Set.range τ
h_top : i ≠ ⊤
⊢ i ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i : WithTop ι
hi : i ∈ Set.range τ
h_top : i ≠ ⊤
lift :
  ∀ (i : ι) (hi : (↑i : WithTop ι) ∈ Set.range τ),
    stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | hτ.measurableSpace]
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = i})] μ[f n | hτ.measurableSpace]

Tactic:
lift i to ι using h_top with i
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i_1 : WithTop ι
i : ι
hi : (↑i : WithTop ι) ∈ Set.range τ
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | hτ.measurableSpace]

Tactic:
stoppedValue_ae_eq_restrict_eq h _ hτ_le i

Premises used: MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
i_1 : WithTop ι
i : ι
hi : (↑i : WithTop ι) ∈ Set.range τ
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | hτ.measurableSpace]

Tactic:
exact stoppedValue_ae_eq_restrict_eq h _ hτ_le i

Premises used: MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
ℱ : Filtration ι m
inst_6 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_7 : Nonempty ι
inst_8 : Countable ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
⊢ stoppedValue f τ =ᶠ[ae μ] μ[f n | hτ.measurableSpace]

Tactic:
h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hτ hτ_le (Set.to_countable _)

Premises used: Set.to_countable, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
have : SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le)) :=
    sigmaFiniteTrim_mono _ (IsStoppingTime.measurableSpace_mono hσ hτ hσ_le_τ)
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]

Tactic:
have : μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ]
      μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace] := condExp_congr_ae
    (h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hτ hτ_le hτ_countable_range)
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this_1 : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
(Filter.EventuallyEq.trans ?_
    (condExp_condExp_of_le ?_ (hτ.measurableSpace_le_of_le hτ_le)).symm).trans this.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_condExp_of_le, Filter.EventuallyEq.symm, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this_1 : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
refine_1 : stoppedValue f σ =ᶠ[ae μ] μ[f n | hσ.measurableSpace]
refine_2 : hσ.measurableSpace ≤ hτ.measurableSpace
⊢ stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
refine (Filter.EventuallyEq.trans ?_
    (condExp_condExp_of_le ?_ (hτ.measurableSpace_le_of_le hτ_le)).symm).trans this.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_condExp_of_le, Filter.EventuallyEq.symm, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this_1 : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ stoppedValue f σ =ᶠ[ae μ] μ[f n | hσ.measurableSpace]

Tactic:
h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hσ
      (fun x => (hσ_le_τ x).trans (hτ_le x)) hσ_countable_range

Premises used: LE.le.trans, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this_1 : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ stoppedValue f σ =ᶠ[ae μ] μ[f n | hσ.measurableSpace]

Tactic:
exact h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hσ
      (fun x => (hσ_le_τ x).trans (hτ_le x)) hσ_countable_range

Premises used: LE.le.trans, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this_1 : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ hσ.measurableSpace ≤ hτ.measurableSpace

Tactic:
hσ.measurableSpace_mono hτ hσ_le_τ

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_mono
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this_1 : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ hσ.measurableSpace ≤ hτ.measurableSpace

Tactic:
exact hσ.measurableSpace_mono hτ hσ_le_τ

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_mono
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
ℱ : Filtration ι m
inst_6 : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_7 : Nonempty ι
inst_8 : Countable ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
⊢ stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
h.stoppedValue_ae_eq_condExp_of_le_of_countable_range hτ hσ hσ_le_τ hτ_le (Set.to_countable _)
    (Set.to_countable _)

Premises used: MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range, Set.to_countable
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
rw :
  Set.indicator {ω : Ω | τ ω ≤ σ ω} μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ]
    Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)
⊢ μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] stoppedValue f τ

Tactic:
rw [ae_eq_restrict_iff_indicator_ae_eq
    (hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ))]

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.IsStoppingTime.measurableSpace_le, ae_eq_restrict_iff_indicator_ae_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
⊢ Set.indicator {ω : Ω | τ ω ≤ σ ω} μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ]
    Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)

Tactic:
(condExp_indicator (integrable_stoppedValue ι hτ h.integrable hτ_le)
    (hτ.measurableSet_stopping_time_le hσ)).symm.trans ?_

Premises used: MeasureTheory.integrable_stoppedValue, Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.condExp_indicator, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
refine :
  μ[Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ) | hσ.measurableSpace] =ᶠ[ae μ]
    Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)
⊢ Set.indicator {ω : Ω | τ ω ≤ σ ω} μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ]
    Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)

Tactic:
refine (condExp_indicator (integrable_stoppedValue ι hτ h.integrable hτ_le)
    (hτ.measurableSet_stopping_time_le hσ)).symm.trans ?_

Premises used: MeasureTheory.integrable_stoppedValue, Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.condExp_indicator, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
⊢ Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ

Tactic:
(integrable_stoppedValue ι hτ h.integrable hτ_le).indicator ?_

Premises used: MeasureTheory.integrable_stoppedValue, MeasureTheory.Martingale.integrable, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ σ ω}
⊢ Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ

Tactic:
refine (integrable_stoppedValue ι hτ h.integrable hτ_le).indicator ?_

Premises used: MeasureTheory.integrable_stoppedValue, MeasureTheory.Martingale.integrable, MeasureTheory.Integrable.indicator