awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
⊢ 𝓕 ≤ 𝓕₊
have this₁ : OrderTopology ι
Tactic: haveI : OrderTopology ι := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have pos : ∀ (hne : (𝓝[>] i).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
Tactic: by_cases hne : (𝓝[>] i).NeBot
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
pos : ∀ (hne : (𝓝[>] i).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have neg : ∀ (hne : ¬(𝓝[>] i).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
Tactic: by_cases hne : (𝓝[>] i).NeBot
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have pos : (↑𝓕 : ι → MeasurableSpace Ω) i ≤ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
Tactic: rw [rightCont_eq_of_neBot_nhdsGT]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : ¬(𝓝[>] i).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have neg : (↑𝓕 : ι → MeasurableSpace Ω) i ≤
  if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j else (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, if_neg hne]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : ¬(𝓝[>] i).NeBot
neg :
  (↑𝓕 : ι → MeasurableSpace Ω) i ≤
    if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j else (↑𝓕 : ι → MeasurableSpace Ω) i
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have neg₁ : (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, if_neg hne]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
⊢ 𝓕₊₊ = 𝓕₊
have this₁ : OrderTopology ι
Tactic: haveI : OrderTopology ι := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ 𝓕₊₊ = 𝓕₊
have apply : 𝓕₊₊ ≤ 𝓕₊
Tactic: apply le_antisymm _ 𝓕₊.le_rightCont
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have pos : ∀ (hne : (𝓝[>] i).NeBot), (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
Tactic: by_cases hne : (𝓝[>] i).NeBot
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
pos : ∀ (hne : (𝓝[>] i).NeBot), (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have neg : ∀ (hne : ¬(𝓝[>] i).NeBot), (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
Tactic: by_cases hne : (𝓝[>] i).NeBot
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j)
    (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)
have apply : ∀ (u : ι) (hu : u > i), ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
Tactic: apply le_iInf₂ fun u hu => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
⊢ Set.Ioo i u ∈ 𝓝[>] i
have rw : ∃ u_1 ∈ 𝓝 i, u_1 ∩ Set.Ioi i ⊆ Set.Ioo i u
Tactic: rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
have hiou : Set.Ioo i u ∈ 𝓝[>] i
Tactic: have hiou : Set.Ioo i u ∈ 𝓝[>] i := by
        rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]
        exact ⟨Set.Iio u, (isOpen_Iio' u).mem_nhds hu, fun _ hx ↦ ⟨hx.2, hx.1⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
have obtain : ∀ (v : ι) (hv : v ∈ Set.Ioo i u),
  ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
Tactic: obtain ⟨v, hv⟩ := hne.nonempty_of_mem hiou
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
have hle₁ : ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) v
Tactic: have hle₁ : (⨅ j > i, 𝓕₊ j) ≤ 𝓕₊ v := iInf₂_le_of_le v hv.1 le_rfl
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
hle₁ : ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) v
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
have pos : ∀ (hnv : (𝓝[>] v).NeBot), (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
Tactic: by_cases hnv : (𝓝[>] v).NeBot
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
hle₁ : ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) v
pos : ∀ (hnv : (𝓝[>] v).NeBot), (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
have neg : ∀ (hnv : ¬(𝓝[>] v).NeBot), (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
Tactic: by_cases hnv : (𝓝[>] v).NeBot
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
hle₁ : ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) v
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
have hle₂ : (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
Tactic: have hle₂ : 𝓕₊ v ≤ 𝓕 u := by
        by_cases hnv : (𝓝[>] v).NeBot
        · simpa [rightCont_eq_of_neBot_nhdsGT] using iInf₂_le_of_le u hv.2 le_rfl
        · simpa [rightCont_apply, hnv] using 𝓕.mono hv.2.le
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have hineq : LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j)
  (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)
Tactic: have hineq : (⨅ j > i, 𝓕₊ j) ≤ ⨅ j > i, 𝓕 j := by
      apply le_iInf₂ fun u hu => ?_
      have hiou : Set.Ioo i u ∈ 𝓝[>] i := by
        rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]
        exact ⟨Set.Iio u, (isOpen_Iio' u).mem_nhds hu, fun _ hx ↦ ⟨hx.2, hx.1⟩⟩
      obtain ⟨v, hv⟩ := hne.nonempty_of_mem hiou
      have hle₁ : (⨅ j > i, 𝓕₊ j) ≤ 𝓕₊ v := iInf₂_le_of_le v hv.1 le_rfl
      have hle₂ : 𝓕₊ v ≤ 𝓕 u := by
        by_cases hnv : (𝓝[>] v).NeBot
        · simpa [rightCont_eq_of_neBot_nhdsGT] using iInf₂_le_of_le u hv.2 le_rfl
        · simpa [rightCont_apply, hnv] using 𝓕.mono hv.2.le
      exact hle₁.trans hle₂
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : ¬(𝓝[>] i).NeBot
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have neg : (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j
  else (↑𝓕₊ : ι → MeasurableSpace Ω) i) ≤
  (↑𝓕₊ : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, if_neg hne]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : ¬(𝓝[>] i).NeBot
neg :
  (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j
    else (↑𝓕₊ : ι → MeasurableSpace Ω) i) ≤
    (↑𝓕₊ : ι → MeasurableSpace Ω) i
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
have neg₁ : (↑𝓕₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, if_neg hne]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ⨆ (j : ι), ⨆ (_ : j ≤ i), MeasurableSpace.comap (u j) (mβ j) ≤ m
have refine : ∀ (i_1 : ι) (j : i_1 ≤ i), MeasurableSpace.comap (u i_1) (mβ i_1) ≤ m
Tactic: refine iSup₂_le ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ (↑(natural (β := β) u hum) : ι → MeasurableSpace Ω) i =
    MeasurableSpace.comap (β := (j : (↑(Set.Iic i) : Type u_2)) → β (↑j : ι))
      (fun (ω : Ω) (j : (↑(Set.Iic i) : Type u_2)) ↦ u (↑j : ι) ω) inferInstance
have simp_rw : Eq.{u_1 + 1} (α := MeasurableSpace Ω)
  (⨆ (x : { i_1 : ι // i_1 ≤ i }), MeasurableSpace.comap (β := β (↑x : ι)) (u (↑x : ι)) (mβ (↑x : ι)))
  (⨆ (a : (↑(Set.Iic i) : Type u_2)), MeasurableSpace.comap (β := β (↑a : ι)) (u (↑a : ι)) inferInstance)
Tactic: simp_rw [natural, MeasurableSpace.comap_process_pi, iSup_subtype']
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := Filtration ι m) (filtrationOfSet (s := s) hsm)
    (natural (β := β) (fun (i : ι) ↦ (s i).indicator fun (x : Ω) ↦ 1) ⋯)
have simp : Eq (α := ι → MeasurableSpace Ω) (fun (i : ι) ↦ MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
  fun (i : ι) ↦ MeasurableSpace.generateFrom {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1}
Tactic: simp only [filtrationOfSet, natural, measurableSpace_iSup_eq, exists_prop, mk.injEq]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ι → MeasurableSpace Ω) (fun (i : ι) ↦ MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
    fun (i : ι) ↦ MeasurableSpace.generateFrom {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1}
have h : ∀ (i : ι),
  Eq.{u_1 + 1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
    (MeasurableSpace.generateFrom {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1})
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ Eq.{u_1 + 1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
    (MeasurableSpace.generateFrom {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1})
have h : ∀ (t : Set Ω), Membership.mem (γ := Set (Set Ω)) {t : Set Ω | ∃ j ≤ i, s j = t} t → MeasurableSet t
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
h : ∀ (t : Set Ω), Membership.mem (γ := Set (Set Ω)) {t : Set Ω | ∃ j ≤ i, s j = t} t → MeasurableSet t
⊢ Eq.{u_1 + 1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
    (MeasurableSpace.generateFrom {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1})
have h₁ : ∀ (t : Set Ω), Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1} t → MeasurableSet t
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
have h : MeasurableSet (s j)
Tactic: refine measurableSet_generateFrom ⟨j, measurableSet_generateFrom ⟨hij, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
have h : MeasurableSet (s j)
Tactic: rw [comap_eq_generateFrom]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
have h : Set.preimage (β := β j) ((s j).indicator fun (x : Ω) ↦ 1) {1} = s j
Tactic: refine measurableSet_generateFrom ⟨{1}, measurableSet_singleton 1, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ Set.preimage (β := β j) ((s j).indicator fun (x : Ω) ↦ 1) {1} = s j
have h : ∀ (x : Ω), x ∈ Set.preimage (β := β j) ((s j).indicator fun (x : Ω) ↦ 1) {1} ↔ x ∈ s j
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSet t
have h : LE.le.{u_1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | n ≤ i ∧ MeasurableSet t})
  (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
Tactic: suffices MeasurableSpace.generateFrom {t | n ≤ i ∧
      MeasurableSet[MeasurableSpace.comap ((s n).indicator (fun _ => 1 : Ω → β n)) (mβ n)] t} ≤
        MeasurableSpace.generateFrom {t | ∃ (j : ι), j ≤ i ∧ s j = t} by
      exact this _ ht
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | n ≤ i ∧ MeasurableSet t})
    (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
have h : ∀ (t : Set Ω), Membership.mem (γ := Set (Set Ω)) {t : Set Ω | n ≤ i ∧ MeasurableSet t} t → MeasurableSet t
Tactic: refine generateFrom_le ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
⊢ MeasurableSet t
have h : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ), MeasurableSet t
Tactic: obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β n)
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
h : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ), MeasurableSet t
⊢ MeasurableSet t
have h₁ : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n), MeasurableSet t
Tactic: obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β n)
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
h : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ), MeasurableSet t
h₁ : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n), MeasurableSet t
⊢ MeasurableSet t
have h₂ : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ), MeasurableSet t
Tactic: obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β n)