awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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ω : τ ω = ⊤
⊢ False
have hτ_le₁ : τ ω ≤ (↑n : WithTop ι)
Tactic: specialize hτ_le ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 τ
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = i})] μ[f n | hτ.measurableSpace]
have h_top : 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
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ≠ ⊤
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = i})] μ[f n | hτ.measurableSpace]
have lift : ∀ (i : ι) (hi : (↑i : WithTop ι) ∈ Set.range τ),
  stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | hτ.measurableSpace]
Tactic: lift i to ι using h_top with i
Cleared hypotheses: hi, h_top
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 ⋯)
⊢ stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
have this : SigmaFinite (μ.trim sorry)
Tactic: have : SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le)) :=
    sigmaFiniteTrim_mono _ (IsStoppingTime.measurableSpace_mono hσ hτ hσ_le_τ)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 σ =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
have this₁ : μ[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)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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]
have refine_1 : stoppedValue f σ =ᶠ[ae μ] μ[f n | hσ.measurableSpace]
Tactic: refine (Filter.EventuallyEq.trans ?_
    (condExp_condExp_of_le ?_ (hτ.measurableSpace_le_of_le hτ_le)).symm).trans this.symm
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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]
⊢ stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
have refine_2 : hσ.measurableSpace ≤ hτ.measurableSpace
Tactic: refine (Filter.EventuallyEq.trans ?_
    (condExp_condExp_of_le ?_ (hτ.measurableSpace_le_of_le hτ_le)).symm).trans this.symm
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
⊢ μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] stoppedValue f τ
have rw : Set.indicator {ω : Ω | τ ω ≤ σ ω} μ[stoppedValue f τ | hσ.measurableSpace] =ᶠ[ae μ]
  Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)
Tactic: rw [ae_eq_restrict_iff_indicator_ae_eq
    (hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ))]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 τ)
have refine : μ[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 ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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) τ)) μ
have refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ σ ω}
Tactic: refine (integrable_stoppedValue ι hτ h.integrable hτ_le).indicator ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 τ)
have h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
Tactic: have h_int :
      Integrable ({ω : Ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n : ι => f n) τ)) μ := by
    refine (integrable_stoppedValue ι hτ h.integrable hτ_le).indicator ?_
    exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
have refine : StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
Tactic: refine StronglyMeasurable.aestronglyMeasurable ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
have refine_1 : ∀ (t : Set Ω), MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) → MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
Tactic: refine StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
refine_1 : ∀ (t : Set Ω), MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) → MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
have refine_2 : StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
Tactic: refine StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
refine_1 : ∀ (t : Set Ω), MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) → MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
refine_2 :
  StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
have refine_3 : ∀ x ∉ {ω : Ω | τ ω ≤ σ ω},
  Eq.{u_2 + 1} (α := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ) x) 0
Tactic: refine StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
⊢ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
have refine_1 : ∀ (ht : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})), MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
Tactic: rw [Set.inter_comm _ t] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
have ht₁ : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ∧ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
Tactic: rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
have refine_2 : StronglyMeasurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)
Tactic: refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)
have refine_2 : Measurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)
Tactic: refine Measurable.stronglyMeasurable ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ μ[Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ) | hσ.measurableSpace] =ᶠ[ae μ]
    Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)
have h_meas : AEStronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
Tactic: have h_meas : AEStronglyMeasurable[hσ.measurableSpace]
      ({ω : Ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n : ι => f n) τ)) μ := by
    refine StronglyMeasurable.aestronglyMeasurable ?_
    refine StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_
    · intro t ht
      rw [Set.inter_comm _ t] at ht ⊢
      rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht
      exact ht.2
    · refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)
      refine Measurable.stronglyMeasurable ?_
      exact measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
    · intro x hx
      simp only [hx, Set.indicator_of_notMem, not_false_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ (stoppedValue f fun (x : Ω) ↦ min (σ x) (τ x)) =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
have hτ₁ : μ[stoppedValue f τ | sorry.measurableSpace] =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
Tactic: refine
    (h.stoppedValue_ae_eq_condExp_of_le hτ (hσ.min hτ) (fun x => min_le_right _ _) hτ_le).trans ?_