awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
f : Filtration ι m
hf_mem : f ∈ s
hfi_mem :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) i) '' s)
    ((↑f : ι → MeasurableSpace Ω) i)
⊢ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑f : ι → MeasurableSpace Ω) i

Tactic:
exact sInf_le hfi_mem

Premises used: sInf_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
pos :
  ∀ (h_nonempty : s.Nonempty),
    (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m
neg :
  ∀ (h_nonempty : ¬s.Nonempty),
    (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m
⊢ (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m

Tactic:
by_cases h_nonempty : Set.Nonempty s

Premises used: Set.Nonempty
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬s.Nonempty
⊢ (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m

Tactic:
simp only [h_nonempty, if_false, le_refl]

Premises used: le_refl, if_false
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : s.Nonempty
pos : sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m
⊢ (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m

Tactic:
simp only [h_nonempty, if_true]

Premises used: if_true
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : s.Nonempty
pos :
  ∀ (f : Filtration ι m) (hf_mem : f ∈ s), sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m
⊢ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m

Tactic:
obtain ⟨f, hf_mem⟩ := h_nonempty
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m

Tactic:
le_trans (sInf_le ⟨f, hf_mem, rfl⟩) (f.le i)

Premises used: sInf_le, And.intro, Exists.intro, MeasureTheory.Filtration.le, rfl, le_trans
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m

Tactic:
exact le_trans (sInf_le ⟨f, hf_mem, rfl⟩) (f.le i)
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ (↑(sInf s) : ι → MeasurableSpace Ω) i =
    if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
⊢ IsLUB (seq '' x) (↑(sSup x) : ι → MeasurableSpace Ω)

Tactic:
simpa only [isLUB_pi, Set.image_image] using fun _ ↦ isLUB_sSup _

Premises used: Set.image_image, isLUB_sSup, isLUB_pi
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
pos :
  ∀ (hn : x.Nonempty),
    IsGLB x
      { seq := fun (i : ι) ↦ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x), mono' := ⋯,
        le' := ⋯ }
neg : ∀ (hn : ¬x.Nonempty), IsGLB x { seq := fun (i : ι) ↦ m, mono' := ⋯, le' := ⋯ }
⊢ IsGLB x
    {
      seq := fun (i : ι) ↦
        if x.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x) else m,
      mono' := ⋯, le' := ⋯ }

Tactic:
split_ifs with hn
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
hn : x.Nonempty
⊢ IsGLB x
    { seq := fun (i : ι) ↦ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x), mono' := ⋯,
      le' := ⋯ }

Tactic:
.of_image (f := seq) .rfl ?_

Premises used: IsGLB.of_image, Iff.rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
hn : x.Nonempty
pos :
  IsGLB (seq '' x)
    (↑{ seq := fun (i : ι) ↦ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x), mono' := ⋯,
          le' := ⋯ } :
      ι → MeasurableSpace Ω)
⊢ IsGLB x
    { seq := fun (i : ι) ↦ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x), mono' := ⋯,
      le' := ⋯ }

Tactic:
refine .of_image (f := seq) .rfl ?_
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
hn : x.Nonempty
⊢ IsGLB (seq '' x)
    (↑{ seq := fun (i : ι) ↦ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x), mono' := ⋯,
          le' := ⋯ } :
      ι → MeasurableSpace Ω)

Tactic:
simpa only [isGLB_pi, Set.image_image] using fun _ ↦ isGLB_sInf _

Premises used: Set.image_image, isGLB_pi, isGLB_sInf
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
hn : ¬x.Nonempty
⊢ x = ∅

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at hn

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
hn_1 : ¬x.Nonempty
hn : x = ∅
⊢ IsGLB x { seq := fun (i : ι) ↦ m, mono' := ⋯, le' := ⋯ }

Tactic:
simpa [hn] using Filtration.le

Premises used: MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
s : Set Ω
i : ι
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
f.le i s hs

Premises used: MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
μ : Measure Ω
f : Filtration ι m
hf : SigmaFiniteFiltration μ f
i : ι
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
hf.SigmaFinite _

Premises used: MeasureTheory.SigmaFiniteFiltration.SigmaFinite
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
μ : Measure Ω
f : Filtration ι m
inst_1 : IsFiniteMeasure μ
n : ι
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Filtration ι m
g : Ω → ℝ
hg : Integrable g μ
⊢ UniformIntegrable (β := ℝ) (fun (i : ι) ↦ μ[g | (↑f : ι → MeasurableSpace Ω) i]) 1 μ

Tactic:
hg.uniformIntegrable_condExp f.le

Premises used: MeasureTheory.Filtration.le, MeasureTheory.Integrable.uniformIntegrable_condExp
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
μ : Measure Ω
ℱ : Filtration ι m
i j : ι
hij : i ≤ j
inst_4 : SigmaFinite (μ.trim ⋯)
⊢ μ[μ[f | (↑ℱ : ι → MeasurableSpace Ω) j] | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
condExp_condExp_of_le (ℱ.mono hij) (ℱ.le j)

Premises used: MeasureTheory.condExp_condExp_of_le, MeasureTheory.Filtration.mono, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hj : j ≤ i
⊢ MeasurableSet (s j)

Tactic:
MeasurableSpace.measurableSet_generateFrom ⟨j, hj, rfl⟩

Premises used: MeasurableSpace.measurableSet_generateFrom, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
i : ι
⊢ MeasurableSet (s i)

Tactic:
measurableSet_filtrationOfSet hsm i le_rfl

Premises used: le_rfl, MeasureTheory.measurableSet_filtrationOfSet
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
simp :
  (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) ≤
    if (𝓝[>] j).NeBot then ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1
    else (↑𝓕 : ι → MeasurableSpace Ω) j
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦
        if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
        else (↑𝓕 : ι → MeasurableSpace Ω) i)
      i)
    ((fun (i : ι) ↦
        if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
        else (↑𝓕 : ι → MeasurableSpace Ω) i)
      j)

Tactic:
simp only [gt_iff_lt]

Premises used: gt_iff_lt
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
pos :
  ∀ (hi : (𝓝[>] i).NeBot) (hj : (𝓝[>] j).NeBot),
    LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j)
      (⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1)
neg :
  ∀ (hi : (𝓝[>] i).NeBot) (hj : ¬(𝓝[>] j).NeBot),
    ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
pos₁ :
  ∀ (hi : ¬(𝓝[>] i).NeBot) (hj : (𝓝[>] j).NeBot),
    (↑𝓕 : ι → MeasurableSpace Ω) i ≤ ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1
neg₁ : ∀ (hi : ¬(𝓝[>] i).NeBot) (hj : ¬(𝓝[>] j).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
⊢ (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) ≤
    if (𝓝[>] j).NeBot then ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1
    else (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
split_ifs with hi hj hj
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j)
    (⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1)

Tactic:
le_iInf₂ fun k hkj ↦ iInf₂_le k (hij.trans_lt hkj)

Premises used: iInf₂_le, le_iInf₂, LE.le.trans_lt
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j)
    (⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1)

Tactic:
exact le_iInf₂ fun k hkj ↦ iInf₂_le k (hij.trans_lt hkj)

Premises used: iInf₂_le, le_iInf₂, LE.le.trans_lt
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
neg :
  ∀ (hij : j ≤ j) (hi : (𝓝[>] j).NeBot),
    ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1 ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
neg₁ : ∀ (hj : j ≠ i), ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
⊢ ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
obtain rfl | hj := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
j : ι
hj : ¬(𝓝[>] j).NeBot
hij : j ≤ j
hi : (𝓝[>] j).NeBot
⊢ ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1 ≤ (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
contradiction
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj_1 : ¬(𝓝[>] j).NeBot
hj : j ≠ i
⊢ ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
iInf₂_le j (lt_of_le_of_ne hij hj.symm)

Premises used: iInf₂_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj_1 : ¬(𝓝[>] j).NeBot
hj : j ≠ i
⊢ ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
exact iInf₂_le j (lt_of_le_of_ne hij hj.symm)

Premises used: iInf₂_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1

Tactic:
le_iInf₂ fun k hk ↦ 𝓕.mono (hij.trans hk.le)

Premises used: LT.lt.le, le_iInf₂, MeasureTheory.Filtration.mono, LE.le.trans
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1

Tactic:
exact le_iInf₂ fun k hk ↦ 𝓕.mono (hij.trans hk.le)

Premises used: le_iInf₂, MeasureTheory.Filtration.mono, LE.le.trans
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
𝓕.mono hij

Premises used: MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕 : ι → MeasurableSpace Ω) j

Tactic:
exact 𝓕.mono hij

Premises used: MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
pos : ∀ (hi : (𝓝[>] i).NeBot), ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m
neg : ∀ (hi : ¬(𝓝[>] i).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ m
⊢ (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) ≤
    m

Tactic:
split_ifs with hi
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : (𝓝[>] i).NeBot
pos : ∀ (j : ι) (hj : i < j), ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m

Tactic:
obtain ⟨j, hj⟩ := (frequently_gt_nhds i).exists

Premises used: frequently_gt_nhds, Filter.Frequently.exists
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : (𝓝[>] i).NeBot
j : ι
hj : i < j
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m

Tactic:
iInf₂_le_of_le j hj (𝓕.le j)

Premises used: iInf₂_le_of_le, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : (𝓝[>] i).NeBot
j : ι
hj : i < j
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m

Tactic:
exact iInf₂_le_of_le j hj (𝓕.le j)

Premises used: iInf₂_le_of_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : ¬(𝓝[>] i).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ m

Tactic:
𝓕.le i

Premises used: MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : ¬(𝓝[>] i).NeBot
⊢ (↑𝓕 : ι → MeasurableSpace Ω) i ≤ m

Tactic:
exact 𝓕.le i

Premises used: MeasureTheory.Filtration.le
-- 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 : ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i =
    if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j else (↑𝓕 : ι → MeasurableSpace Ω) i

Tactic:
simp +instances only [rightCont, OrderTopology.topology_eq_generate_intervals]

Premises used: MeasureTheory.Filtration.rightCont, OrderTopology.topology_eq_generate_intervals
-- 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 : ι
hi : 𝓝[>] i = ⊥
rw :
  (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) =
    (↑𝓕 : ι → MeasurableSpace Ω) i
rw₁ :
  (if NeBot.{u_2} (α := ι) ⊥ then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) =
    (↑𝓕 : ι → MeasurableSpace Ω) i
rw₂ :
  (if Ne.{u_2 + 1} (α := Filter ι) ⊥ ⊥ then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) =
    (↑𝓕 : ι → MeasurableSpace Ω) i
rw₃ :
  (if False then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j else (↑𝓕 : ι → MeasurableSpace Ω) i) =
    (↑𝓕 : ι → MeasurableSpace Ω) i
rw₄ rw₅ : (↑𝓕 : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i

Tactic:
rw [rightCont_apply, hi, neBot_iff, ne_self_iff_false, if_false]

Premises used: ne_self_iff_false, if_false, Filter.neBot_iff, MeasureTheory.Filtration.rightCont_apply
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : SuccOrder ι
𝓕 : 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 : LinearOrder ι
inst_1 : SuccOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
h : ∀ (x : ι) (s : Set Ω), MeasurableSet s ↔ MeasurableSet s
⊢ 𝓕₊ = 𝓕

Tactic:
ext _
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : SuccOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
x : ι
s : Set Ω
h h₁ : MeasurableSet s ↔ MeasurableSet s
⊢ MeasurableSet s ↔ MeasurableSet s

Tactic:
rw [rightCont_eq_of_nhdsGT_eq_bot _ SuccOrder.nhdsGT]

Premises used: MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot, SuccOrder.nhdsGT
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : 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 : PartialOrder ι
𝓕 : Filtration ι m
i : ι
hi : IsMax i
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i

Tactic:
rightCont_eq_of_nhdsGT_eq_bot _ (hi.Ioi_eq ▸ nhdsWithin_empty i)

Premises used: MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
i : ι
hi : IsMax i
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i

Tactic:
exact rightCont_eq_of_nhdsGT_eq_bot _ (hi.Ioi_eq ▸ nhdsWithin_empty i)

Premises used: MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
𝓕 : Filtration ι m
i : ι
hi : ∃ j > i, Set.Ioo i j = ∅
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 ι
𝓕 : Filtration ι m
i : ι
hi : ∃ j > i, Set.Ioo i j = ∅
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
obtain :
  ∀ (j : ι) (hij : j > i) (hIoo : Set.Ioo i j = ∅), (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i

Tactic:
obtain ⟨j, hij, hIoo⟩ := hi
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
𝓕 : Filtration ι m
i : ι
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
j : ι
hij : j > i
hIoo : Set.Ioo i j = ∅
⊢ i ⋖ j

Tactic:
have hcov : i ⋖ j := covBy_iff_Ioo_eq.mpr ⟨hij, hIoo⟩
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
𝓕 : Filtration ι m
i : ι
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
j : ι
hij : j > i
hIoo : Set.Ioo i j = ∅
hcov : i ⋖ j
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i

Tactic:
rightCont_eq_of_nhdsGT_eq_bot _ <| CovBy.nhdsGT hcov

Premises used: MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot, CovBy.nhdsGT
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
𝓕 : Filtration ι m
i : ι
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
j : ι
hij : j > i
hIoo : Set.Ioo i j = ∅
hcov : i ⋖ j
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i

Tactic:
exact rightCont_eq_of_nhdsGT_eq_bot _ <| CovBy.nhdsGT hcov

Premises used: MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot, CovBy.nhdsGT