awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
⊢ Eq (α := ℝ≥0∞)
    (if b ∈ s then
      ∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
    else 0)
    (∑' (a : α),
      if b ∈ s then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
      else 0)
have pos : ∀ (hbs : b ∈ s),
  Eq (α := ℝ≥0∞)
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
          ℝ≥0∞))
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
          ℝ≥0∞))
Tactic: split_ifs with hbs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
pos :
  ∀ (hbs : b ∈ s),
    Eq (α := ℝ≥0∞)
      (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞))
      (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞)
    (if b ∈ s then
      ∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
    else 0)
    (∑' (a : α),
      if b ∈ s then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
      else 0)
have neg : ∀ (hbs : b ∉ s), Eq (α := ℝ≥0∞) 0 (∑' (a : α), 0)
Tactic: split_ifs with hbs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β),
          if b ∈ s then
            if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b
          else 0 :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else ∑' (b : β), if b ∈ s then (f a h : (a : β) → ℝ≥0∞) b else 0 :
        ℝ≥0∞)
have pos : ∀ (ha : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (b : β), if b ∈ s then 0 else 0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
pos :
  ∀ (ha : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (b : β), if b ∈ s then 0 else 0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β),
          if b ∈ s then
            if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b
          else 0 :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else ∑' (b : β), if b ∈ s then (f a h : (a : β) → ℝ≥0∞) b else 0 :
        ℝ≥0∞)
have neg : ∀ (ha : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β), if b ∈ s then (f a ha : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β), if b ∈ s then (f a ha : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞)
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_3 : ∀ (i : ι), BorelSpace.{u_3} (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)
have refine : StronglyMeasurable (u i)
Tactic: refine StronglyMeasurable.mono ?_ (le_iSup₂_of_le i (le_refl i) le_rfl)
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_3 : ∀ (i : ι), BorelSpace.{u_3} (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)
have rw : Measurable (u i) ∧ IsSeparable (Set.range (u i))
Tactic: rw [stronglyMeasurable_iff_measurable_separable]
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
⊢ Measurable (u i)
have this : u i =
  (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i sorry, x)
Tactic: have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
    rfl
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
⊢ Measurable (u i)
have rw : Measurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
  ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i sorry, x))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
⊢ Measurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (fun (i : ι) (ω : Ω) ↦ u (t i ω) ω) (↑p.1 : ι) p.2
have this : Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
  (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
  ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
    fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) sorry, p.2))
Tactic: have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
    (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
      (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) := rfl
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ Measurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (fun (i : ι) (ω : Ω) ↦ u (t i ω) ω) (↑p.1 : ι) p.2
have rw : Measurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
  ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
    fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) sorry, p.2))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
⊢ StronglyMeasurable (u i)
have this : u i =
  (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i sorry, x)
Tactic: have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
    rfl
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
⊢ StronglyMeasurable (u i)
have rw : StronglyMeasurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
  ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i sorry, x))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
t : ι → Ω → ι
inst_3 : TopologicalSpace ι
inst_4 : BorelSpace ι
inst_5 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (fun (i : ι) (ω : Ω) ↦ u (t i ω) ω) (↑p.1 : ι) p.2
have this : Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
  (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
  ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
    fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) sorry, p.2))
Tactic: have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
    (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
      (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) := rfl
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
t : ι → Ω → ι
inst_3 : TopologicalSpace ι
inst_4 : BorelSpace ι
inst_5 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (fun (i : ι) (ω : Ω) ↦ u (t i ω) ω) (↑p.1 : ι) p.2
have rw : StronglyMeasurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
  ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
    fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) sorry, p.2))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
γ : Type u_4
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (a : Ω) ↦ ∏ c ∈ s, U c i a
have h₁ : Eq (α := ι → Ω → β) (fun (i : ι) (a : Ω) ↦ ∏ c ∈ s, U c i a) (∏ c ∈ s, U c)
Tactic: convert! IsStronglyProgressive.finsetProd' h using 1
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
γ : Type u_4
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ Eq (α := ι → Ω → β) (fun (i : ι) (a : Ω) ↦ ∏ c ∈ s, U c i a) (∏ c ∈ s, U c)
have h₁ : ∀ (i : ι) (a : Ω), Eq.{u_3 + 1} (α := β) (∏ c ∈ s, U c i a) ((∏ c ∈ s, U c) i a)
Tactic: ext (i a)
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst_2 : MeasurableSpace ι
inst_3 : PseudoMetrizableSpace β
fltr : Filter γ
inst_4 : fltr.NeBot
inst_5 : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2
have apply : Tendsto (β := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω → β)
  (fun (l : γ) (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ U l (↑p.1 : ι) p.2) fltr
  (𝓝 fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2)
Tactic: apply @stronglyMeasurable_of_tendsto (Set.Iic i × Ω) β γ
    (MeasurableSpace.prod _ (f i)) _ _ fltr _ _ _ _ fun l => h l i
-- Lean 4 proof step from Mathlib.Probability.Process.Adapted (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst_2 : MeasurableSpace ι
inst_3 : PseudoMetrizableSpace β
fltr : Filter γ
inst_4 : fltr.NeBot
inst_5 : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ Tendsto (β := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω → β)
    (fun (l : γ) (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ U l (↑p.1 : ι) p.2) fltr
    (𝓝 fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2)
have rw : ∀ (h_tendsto : ∀ (x : ι), Tendsto (fun (i : γ) ↦ U i x) fltr (𝓝 (u x))) (i : ι)
  (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω),
  Tendsto (fun (i_1 : γ) ↦ U i_1 (↑x.1 : ι) x.2) fltr (𝓝 (u (↑x.1 : ι) x.2))
Tactic: rw [tendsto_pi_nhds] at h_tendsto ⊢
Cleared hypotheses: h_tendsto, i
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f g : Filtration ι m
h : (↑f : ι → MeasurableSpace Ω) = (↑g : ι → MeasurableSpace Ω)
⊢ f = g
have mk : ∀ (seq : ι → MeasurableSpace Ω) (mono' : Monotone seq) (le' : ∀ (i : ι), seq i ≤ m)
  (h :
    (↑{ seq := seq, mono' := mono', le' := le' : Filtration ι m } : ι → MeasurableSpace Ω) =
      (↑g : ι → MeasurableSpace Ω)),
  { seq := seq, mono' := mono', le' := le' : Filtration ι m } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
g : Filtration ι m
seq : ι → MeasurableSpace Ω
mono' : Monotone seq
le' : ∀ (i : ι), seq i ≤ m
h :
  (↑{ seq := seq, mono' := mono', le' := le' : Filtration ι m } : ι → MeasurableSpace Ω) = (↑g : ι → MeasurableSpace Ω)
⊢ { seq := seq, mono' := mono', le' := le' : Filtration ι m } = g
have mk : ∀ (seq_1 : ι → MeasurableSpace Ω) (mono'_1 : Monotone seq_1) (le'_1 : ∀ (i : ι), seq_1 i ≤ m)
  (h :
    (↑{ seq := seq, mono' := mono', le' := le' : Filtration ι m } : ι → MeasurableSpace Ω) =
      (↑{ seq := seq_1, mono' := mono'_1, le' := le'_1 : Filtration ι m } : ι → MeasurableSpace Ω)),
  { seq := seq, mono' := mono', le' := le' : Filtration ι m } = { seq := seq_1, mono' := mono'_1, le' := le'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) i)
    ((fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j)
have refine : ∀ (m' : MeasurableSpace Ω)
  (hm' :
    Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s)
      m'),
  m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
Tactic: refine sSup_le fun m' hm' => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) m'
⊢ m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
have hm'₁ : ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'
Tactic: rw [Set.mem_image] at hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'
⊢ m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
have obtain : ∀ (f : Filtration ι m) (hf_mem : f ∈ s) (hfm' : (↑f : ι → MeasurableSpace Ω) i = m'),
  m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
Tactic: obtain ⟨f, hf_mem, hfm'⟩ := hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
have rw : (↑f : ι → MeasurableSpace Ω) i ≤
  (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
Tactic: rw [← hfm']
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ (↑f : ι → MeasurableSpace Ω) i ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
have refine : (↑f : ι → MeasurableSpace Ω) j ≤
  (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
Tactic: refine (f.mono hij).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ (↑f : ι → MeasurableSpace Ω) j ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
have hfj_mem : Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) j) '' s)
  ((↑f : ι → MeasurableSpace Ω) j)
Tactic: have hfj_mem : f j ∈ (fun g : Filtration ι m => g j) '' s := ⟨f, hf_mem, rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m
have refine : ∀ (m' : MeasurableSpace Ω)
  (hm' :
    Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s)
      m'),
  m' ≤ m
Tactic: refine sSup_le fun m' hm' => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) m'
⊢ m' ≤ m
have hm'₁ : ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'
Tactic: rw [Set.mem_image] at hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'
⊢ m' ≤ m
have obtain : ∀ f ∈ s, ∀ (hfm' : (↑f : ι → MeasurableSpace Ω) i = m'), m' ≤ m
Tactic: obtain ⟨f, _, hfm'⟩ := hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ m' ≤ m
have rw : (↑f : ι → MeasurableSpace Ω) i ≤ m
Tactic: rw [← hfm']
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      i)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      j)
have pos : ∀ (h_nonempty : s.Nonempty),
  LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      i)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      j)
Tactic: by_cases h_nonempty : Set.Nonempty s