awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
h :
  Eq.{u_2 + 1} (α := Measure β)
    (Measure.withDensity (Measure.withDensity ((κ : (a : α) → Measure β) a) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞))
      fun (x : β) ↦ g a x)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
⊢ Eq (α := Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a)
      (HMul.hMul (α := (x : β) → ℝ≥0∞) (fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)) fun (x : β) ↦ g a x))
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
have h₁ : Measurable (β := ℝ≥0∞) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)
Tactic: rw [withDensity_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
h :
  Eq.{u_2 + 1} (α := Measure β)
    (Measure.withDensity (Measure.withDensity ((κ : (a : α) → Measure β) a) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞))
      fun (x : β) ↦ g a x)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
h₁ : Measurable (β := ℝ≥0∞) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)
⊢ Eq (α := Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a)
      (HMul.hMul (α := (x : β) → ℝ≥0∞) (fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)) fun (x : β) ↦ g a x))
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
have h₂ : Measurable (β := ℝ≥0∞) fun (x : β) ↦ g a x
Tactic: rw [withDensity_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.withDensity (Measure.withDensity ((κ : (a : α) → Measure β) a) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞))
      fun (x : β) ↦ g a x)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
have h : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞))
Tactic: rw [Kernel.withDensity_apply _ hg, Kernel.withDensity_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
x : E
i j : ι
h : i ≤ j
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) μ[(fun (x_1 : ι) (x_2 : Ω) ↦ x) j | (↑ℱ : ι → MeasurableSpace Ω) i]
    ((fun (x_1 : ι) (x_2 : Ω) ↦ x) i)
have rw : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (fun (x_1 : Ω) ↦ x) fun (x_1 : Ω) ↦ x
Tactic: rw [condExp_const (ℱ.le _)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst_4 : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
⊢ Martingale.{u_1, u_2, u_3} (E := E) (fun (x : ι) ↦ f) ℱ μ
have refine : ∀ (i j : ι),
  i ≤ j →
    EventuallyEq.{u_1, u_2} (β := E) (ae μ) μ[(fun (x : ι) ↦ f) j | (↑ℱ : ι → MeasurableSpace Ω) i]
      ((fun (x : ι) ↦ f) i)
Tactic: refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst_4 : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
i j : ι
h : i ≤ j
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) μ[(fun (x : ι) ↦ f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ((fun (x : ι) ↦ f) i)
have rw : f =ᶠ[ae μ] f
Tactic: rw [condExp_of_stronglyMeasurable (ℱ.le _) (hf.mono <| ℱ.mono bot_le) hfint]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have rw : Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ)
Tactic: rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ)
have refine : ∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x
Tactic: refine setIntegral_congr_ae (ℱ.le i s hs) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x = f i x) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω | (fun (x : Ω) ↦ x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x) x} x}
    a
Tactic: filter_upwards [hf.2 i j hij] with _ heq _ using heq.symm
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x = f i x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω | (fun (x : Ω) ↦ x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x) x} x}
      a
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x
have h₁ : ∀ (a : Ω), μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a = f i a → a ∈ s → f i a = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
Tactic: filter_upwards [hf.2 i j hij] with _ heq _ using heq.symm
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
⊢ Martingale g ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] g i
Tactic: refine ⟨hg, fun i j hij ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + g) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (f + g) i
Tactic: refine ⟨hf.stronglyAdapted.add hg.stronglyAdapted, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f - g) ℱ μ
have rw : Martingale (f + -g) ℱ μ
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
c : ℝ
hf : Martingale f ℱ μ
⊢ Martingale (c • f) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (c • f) i
Tactic: refine ⟨hf.stronglyAdapted.smul c, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (c • f) i
have refine : ∀ (x : Ω) (hx : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x = f i x),
  (c • μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) x = (c • f) i x
Tactic: refine (condExp_smul ..).trans ((hf.2 i j hij).mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ LE.le.{u_2} (α := E) (∫ (ω : Ω) in s, f j ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
have rw : LE.le.{u_2} (α := E) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
Tactic: rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ LE.le.{u_2} (α := E) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
have refine : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
Tactic: refine setIntegral_mono_ae integrable_condExp.integrableOn (hf.integrable i).integrableOn ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ≤ f i x) x} x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ≤ f i x) x} x}
    a
Tactic: filter_upwards [hf.2.1 i j hij] with _ heq using heq
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ≤ f i x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ≤ f i x) x} x}
      a
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
have h₁ : ∀ (a : Ω), μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a → μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
Tactic: filter_upwards [hf.2.1 i j hij] with _ heq using heq
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
⊢ Supermartingale g ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] g i
Tactic: refine ⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
⊢ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] g i
have h : ∀ (ω : Ω) (h_le : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ f i ω)
  (hcond : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω = μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω)
  (h_eq : f i ω = g i ω), μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ g i ω
Tactic: filter_upwards [condExp_ae_le hf hij, condExp_congr_ae (h_eq j), h_eq i] with ω h_le hcond h_eq
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq_1 : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
ω : Ω
h_le : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ f i ω
hcond : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω = μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω
h_eq : f i ω = g i ω
⊢ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ g i ω
have h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ g i ω
Tactic: rwa [← hcond, ← h_eq]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Supermartingale (f + g) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i
Tactic: refine ⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i
have refine : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i
Tactic: refine (condExp_add (hf.integrable j) (hg.integrable j) _).le.trans ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i
have h : ∀ (a : Ω),
  μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a →
    μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a →
      (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (f + g) i a
Tactic: filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
⊢ Submartingale (-f) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), (-f) i ≤ᶠ[ae μ] μ[(-f) j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine ⟨hf.1.neg, fun i j hij => ?_, fun i => (hf.2.2 i).neg⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ (-f) i ≤ᶠ[ae μ] μ[(-f) j | (↑ℱ : ι → MeasurableSpace Ω) i]
have refine : (-f) i ≤ᶠ[ae μ] -μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine EventuallyLE.trans ?_ (condExp_neg ..).symm.le
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ (-f) i ≤ᶠ[ae μ] -μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
have h : ∀ (a : Ω), μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a → (-f) i a ≤ (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a
Tactic: filter_upwards [hf.2.1 i j hij] with _ _
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Submartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
⊢ Submartingale g ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), g i ≤ᶠ[ae μ] μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine ⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Submartingale (f + g) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), (f + g) i ≤ᶠ[ae μ] μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine ⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ (f + g) i ≤ᶠ[ae μ] μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
have refine : (f + g) i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine EventuallyLE.trans ?_ (condExp_add (hf.integrable j) (hg.integrable j) _).symm.le
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ (f + g) i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]
have h : ∀ (a : Ω),
  f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a →
    g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a →
      (f + g) i a ≤ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]) a
Tactic: filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
⊢ Supermartingale (-f) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), -μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (-f) i
Tactic: refine ⟨hf.1.neg, fun i j hij => (condExp_neg ..).le.trans ?_, fun i => (hf.2.2 i).neg⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ -μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (-f) i
have h : ∀ (a : Ω), f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a → (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (-f) i a
Tactic: filter_upwards [hf.2.1 i j hij] with _ _
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ LE.le.{u_2} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have rw : LE.le.{u_2} (α := E) (∫ (a : Ω) in s, -f j a ∂μ) (∫ (a : Ω) in s, -f i a ∂μ)
Tactic: rw [← neg_le_neg_iff, ← integral_neg, ← integral_neg]