awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι m
i : ι
inst_3 : (𝓝[>] i).NeBot
rw :
  (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) =
    ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)
    (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
rw [rightCont_apply, if_pos ‹(𝓝[>] i).NeBot›]

Premises used: MeasureTheory.Filtration.rightCont_apply, if_pos
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this : TopologicalSpace ι := Preorder.topology ι
⊢ OrderTopology ι

Tactic:
haveI : OrderTopology ι := ⟨rfl⟩
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ (𝓝[>] i).NeBot

Tactic:
have : (𝓝[>] i).NeBot := nhdsGT_neBot_of_exists_gt (not_isMax_iff.mp hi)
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this_1 : TopologicalSpace ι := Preorder.topology ι
this_2 : OrderTopology ι
this : (𝓝[>] i).NeBot
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
rightCont_eq_of_neBot_nhdsGT _ _

Premises used: MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this_1 : TopologicalSpace ι := Preorder.topology ι
this_2 : OrderTopology ι
this : (𝓝[>] i).NeBot
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
exact rightCont_eq_of_neBot_nhdsGT _ _

Premises used: MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : DenselyOrdered ι
inst_2 : NoMaxOrder ι
𝓕 : Filtration ι m
i : ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
𝓕.rightCont_eq_of_not_isMax (not_isMax i)

Premises used: not_isMax, MeasureTheory.Filtration.rightCont_eq_of_not_isMax
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
⊢ OrderTopology ι

Tactic:
haveI : OrderTopology ι := ⟨rfl⟩
-- Module: Mathlib.Probability.Process.Filtration
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
neg : ∀ (hne : ¬(𝓝[>] i).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i

Tactic:
by_cases hne : (𝓝[>] i).NeBot

Premises used: Set.Ioi, Filter.NeBot, nhdsWithin
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
pos : (↑𝓕 : ι → MeasurableSpace Ω) i ≤ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i

Tactic:
rw [rightCont_eq_of_neBot_nhdsGT]

Premises used: MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT
-- Module: Mathlib.Probability.Process.Filtration
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 ≤ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
le_iInf₂ fun _ he => 𝓕.mono he.le

Premises used: LT.lt.le, le_iInf₂, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Filtration
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 ≤ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
exact le_iInf₂ fun _ he => 𝓕.mono he.le

Premises used: le_iInf₂, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Filtration
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
neg₁ neg₂ : (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕 : ι → MeasurableSpace Ω) i
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i

Tactic:
rw [rightCont_apply, if_neg hne]

Premises used: MeasureTheory.Filtration.rightCont_apply, if_neg
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
apply : 𝓕₊₊ ≤ 𝓕₊
⊢ 𝓕₊₊ = 𝓕₊

Tactic:
apply le_antisymm _ 𝓕₊.le_rightCont

Premises used: MeasureTheory.Filtration.rightCont, le_antisymm, MeasureTheory.Filtration.le_rightCont
-- Module: Mathlib.Probability.Process.Filtration
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
neg : ∀ (hne : ¬(𝓝[>] i).NeBot), (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i

Tactic:
by_cases hne : (𝓝[>] i).NeBot

Premises used: Set.Ioi, Filter.NeBot, nhdsWithin
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
apply :
  ∀ (u : ι) (hu : u > i), ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j)
    (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)

Tactic:
apply le_iInf₂ fun u hu => ?_

Premises used: le_iInf₂
-- Module: Mathlib.Probability.Process.Filtration
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
rw : ∃ u_1 ∈ 𝓝 i, u_1 ∩ Set.Ioi i ⊆ Set.Ioo i u
⊢ Set.Ioo i u ∈ 𝓝[>] i

Tactic:
rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]

Premises used: mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Probability.Process.Filtration
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
⊢ ∃ u_1 ∈ 𝓝 i, u_1 ∩ Set.Ioi i ⊆ Set.Ioo i u

Tactic:
⟨Set.Iio u, (isOpen_Iio' u).mem_nhds hu, fun _ hx ↦ ⟨hx.2, hx.1⟩⟩

Premises used: isOpen_Iio', And.right, And.left, And.intro, IsOpen.mem_nhds, Exists.intro, Set.Iio
-- Module: Mathlib.Probability.Process.Filtration
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
⊢ ∃ u_1 ∈ 𝓝 i, u_1 ∩ Set.Ioi i ⊆ Set.Ioo i u

Tactic:
exact ⟨Set.Iio u, (isOpen_Iio' u).mem_nhds hu, fun _ hx ↦ ⟨hx.2, hx.1⟩⟩
-- Module: Mathlib.Probability.Process.Filtration
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

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⟩⟩
-- Module: Mathlib.Probability.Process.Filtration
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
obtain :
  ∀ (v : ι) (hv : v ∈ Set.Ioo i u),
    ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u

Tactic:
obtain ⟨v, hv⟩ := hne.nonempty_of_mem hiou

Premises used: Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Probability.Process.Filtration
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 Ω) v

Tactic:
have hle₁ : (⨅ j > i, 𝓕₊ j) ≤ 𝓕₊ v := iInf₂_le_of_le v hv.1 le_rfl
-- Module: Mathlib.Probability.Process.Filtration
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
neg : ∀ (hnv : ¬(𝓝[>] v).NeBot), (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u

Tactic:
by_cases hnv : (𝓝[>] v).NeBot

Premises used: Set.Ioi, Filter.NeBot, nhdsWithin
-- Module: Mathlib.Probability.Process.Filtration
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
hnv : (𝓝[>] v).NeBot
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u

Tactic:
simpa [rightCont_eq_of_neBot_nhdsGT] using iInf₂_le_of_le u hv.2 le_rfl

Premises used: le_rfl, iInf₂_le_of_le, And.right, MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT
-- Module: Mathlib.Probability.Process.Filtration
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
hnv : ¬(𝓝[>] v).NeBot
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u

Tactic:
simpa [rightCont_apply, hnv] using 𝓕.mono hv.2.le

Premises used: LT.lt.le, MeasureTheory.Filtration.rightCont_apply, And.right, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Filtration
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

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
-- Module: Mathlib.Probability.Process.Filtration
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
hle₂ : (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u

Tactic:
hle₁.trans hle₂

Premises used: LE.le.trans
-- Module: Mathlib.Probability.Process.Filtration
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
hle₂ : (↑𝓕₊ : ι → MeasurableSpace Ω) v ≤ (↑𝓕 : ι → MeasurableSpace Ω) u
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) u

Tactic:
exact hle₁.trans hle₂

Premises used: LE.le.trans
-- Module: Mathlib.Probability.Process.Filtration
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)

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₂
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
hineq :
  LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕₊ : ι → MeasurableSpace Ω) j)
    (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i

Tactic:
simpa [rightCont_eq_of_neBot_nhdsGT] using hineq

Premises used: MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT
-- Module: Mathlib.Probability.Process.Filtration
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
neg₁ neg₂ : (↑𝓕₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i
⊢ (↑𝓕₊₊ : ι → MeasurableSpace Ω) i ≤ (↑𝓕₊ : ι → MeasurableSpace Ω) i

Tactic:
rw [rightCont_apply, if_neg hne]

Premises used: MeasureTheory.Filtration.rightCont_apply, if_neg
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
h : 𝓕.IsRightContinuous
⊢ 𝓕₊ = 𝓕

Tactic:
(le_antisymm 𝓕.le_rightCont h.RC).symm

Premises used: le_antisymm, MeasureTheory.Filtration.le_rightCont, MeasureTheory.Filtration.IsRightContinuous.RC, Eq.symm
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
⊢ 𝓕₊.IsRightContinuous

Tactic:
⟨(rightCont_self 𝓕).le⟩

Premises used: Eq.le, MeasureTheory.Filtration.rightCont_self, MeasureTheory.Filtration.IsRightContinuous.mk
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
inst_1 : 𝓕.IsRightContinuous
i : ι
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
IsRightContinuous.eq (𝓕 := 𝓕) ▸ hs

Premises used: Eq.rec, MeasureTheory.Filtration.IsRightContinuous.eq
-- Module: Mathlib.Probability.Process.Filtration
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

Tactic:
iSup₂_le ?_

Premises used: iSup₂_le
-- Module: Mathlib.Probability.Process.Filtration
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 : ι
refine : ∀ (i_1 : ι) (j : i_1 ≤ i), MeasurableSpace.comap (u i_1) (mβ i_1) ≤ m
⊢ ⨆ (j : ι), ⨆ (_ : j ≤ i), MeasurableSpace.comap (u j) (mβ j) ≤ m

Tactic:
refine iSup₂_le ?_

Premises used: iSup₂_le
-- Module: Mathlib.Probability.Process.Filtration
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_1 : j ≤ i
t : Set (β j)
ht : MeasurableSet t
⊢ MeasurableSet (u j ⁻¹' t)

Tactic:
(hum j).measurable ht

Premises used: MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.Probability.Process.Filtration
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_1 : j ≤ i
t : Set (β j)
ht : MeasurableSet t
⊢ MeasurableSet (u j ⁻¹' t)

Tactic:
exact (hum j).measurable ht

Premises used: MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.Probability.Process.Filtration
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 : ι
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)
⊢ (↑(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

Tactic:
simp_rw [natural, MeasurableSpace.comap_process_pi, iSup_subtype']

Premises used: MeasureTheory.Filtration.natural, iSup_subtype', MeasurableSpace.comap_process_pi
-- Module: Mathlib.Probability.Process.Filtration
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 : ι
⊢ 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:
rfl
-- Module: Mathlib.Probability.Process.Filtration
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)
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}
⊢ Eq (α := Filtration ι m) (filtrationOfSet (s := s) hsm)
    (natural (β := β) (fun (i : ι) ↦ (s i).indicator fun (x : Ω) ↦ 1) ⋯)

Tactic:
simp only [filtrationOfSet, natural, measurableSpace_iSup_eq, exists_prop, mk.injEq]

Premises used: MeasureTheory.Filtration.natural, MeasurableSpace.measurableSpace_iSup_eq, exists_prop, MeasureTheory.filtrationOfSet, MeasureTheory.Filtration.mk.injEq
-- Module: Mathlib.Probability.Process.Filtration
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)
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})
⊢ 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:
ext1 i
-- Module: Mathlib.Probability.Process.Filtration
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})

Tactic:
le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le