awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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 neg : ∀ (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
-- 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
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)
have pos : ∀ a ∈ s, sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑a : ι → MeasurableSpace Ω) j
Tactic: simp only [h_nonempty, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp,
          forall_apply_eq_imp_iff₂]
-- 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
h_nonempty : s.Nonempty
⊢ ∀ a ∈ s, sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑a : ι → MeasurableSpace Ω) j
have pos : ∀ (f : Filtration ι m) (hf_mem : f ∈ s),
  sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑f : ι → MeasurableSpace Ω) i
Tactic: refine fun f hf_mem => le_trans ?_ (f.mono hij)
-- 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
h_nonempty : s.Nonempty
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑f : ι → MeasurableSpace Ω) i
have hfi_mem : Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) i) '' s)
  ((↑f : ι → MeasurableSpace Ω) i)
Tactic: have hfi_mem : f i ∈ (fun g : Filtration ι m => g i) '' 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 : ι
⊢ (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m
have pos : ∀ (h_nonempty : s.Nonempty),
  (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m
Tactic: by_cases h_nonempty : Set.Nonempty s
-- 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 : ι
pos :
  ∀ (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
have neg : ∀ (h_nonempty : ¬s.Nonempty),
  (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m
Tactic: by_cases h_nonempty : Set.Nonempty s
-- 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 : ι
h_nonempty : s.Nonempty
⊢ (if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m) ≤ m
have pos : sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m
Tactic: simp only [h_nonempty, if_true]
-- 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 : ι
h_nonempty : s.Nonempty
⊢ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m
have pos : ∀ (f : Filtration ι m) (hf_mem : f ∈ s), sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m
Tactic: obtain ⟨f, hf_mem⟩ := h_nonempty
Cleared hypotheses: h_nonempty
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
⊢ IsGLB x
    {
      seq := fun (i : ι) ↦
        if x.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x) else m,
      mono' := ⋯, le' := ⋯ }
have pos : ∀ (hn : x.Nonempty),
  IsGLB x
    { seq := fun (i : ι) ↦ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x), mono' := sorry,
      le' := sorry }
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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' := ⋯ }
⊢ IsGLB x
    {
      seq := fun (i : ι) ↦
        if x.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x) else m,
      mono' := ⋯, le' := ⋯ }
have neg : ∀ (hn : ¬x.Nonempty), IsGLB x { seq := fun (i : ι) ↦ m, mono' := sorry, le' := sorry }
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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' := ⋯ }
have pos : IsGLB (seq '' x)
  (↑{ seq := fun (i : ι) ↦ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' x), mono' := sorry,
        le' := sorry } :
    ι → MeasurableSpace Ω)
Tactic: refine .of_image (f := seq) .rfl ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
x : Set (Filtration ι m)
hn : ¬x.Nonempty
⊢ IsGLB x { seq := fun (i : ι) ↦ m, mono' := ⋯, le' := ⋯ }
have hn₁ : x = ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty] at hn
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ 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)
have 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
Tactic: simp only [gt_iff_lt]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ 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
have 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)
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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)
⊢ (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
have neg : ∀ (hi : (𝓝[>] i).NeBot) (hj : ¬(𝓝[>] j).NeBot),
  ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (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
have pos₁ : ∀ (hi : ¬(𝓝[>] i).NeBot) (hj : (𝓝[>] j).NeBot),
  (↑𝓕 : ι → MeasurableSpace Ω) i ≤ ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (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
have neg₁ : ∀ (hi : ¬(𝓝[>] i).NeBot) (hj : ¬(𝓝[>] j).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
have neg : ∀ (hij : j ≤ j) (hi : (𝓝[>] j).NeBot),
  ⨅ (j_1 : ι), ⨅ (_ : j < j_1), (↑𝓕 : ι → MeasurableSpace Ω) j_1 ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
Tactic: obtain rfl | hj := eq_or_ne j i
Cleared hypotheses: i, hij, hi
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
have neg₁ : ∀ (hj : j ≠ i), ⨅ (j : ι), ⨅ (_ : i < j), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ (↑𝓕 : ι → MeasurableSpace Ω) j
Tactic: obtain rfl | hj := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
⊢ (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) ≤
    m
have pos : ∀ (hi : (𝓝[>] i).NeBot), ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
    else (↑𝓕 : ι → MeasurableSpace Ω) i) ≤
    m
have neg : ∀ (hi : ¬(𝓝[>] i).NeBot), (↑𝓕 : ι → MeasurableSpace Ω) i ≤ m
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : (𝓝[>] i).NeBot
⊢ ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m
have pos : ∀ (j : ι) (hj : i < j), ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j ≤ m
Tactic: obtain ⟨j, hj⟩ := (frequently_gt_nhds i).exists
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι m
i : ι
hi : 𝓝[>] i = ⊥
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have rw : (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j else (↑𝓕 : ι → MeasurableSpace Ω) i) =
  (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, hi, neBot_iff, ne_self_iff_false, if_false]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have rw₁ : (if NeBot.{u_2} (α := ι) ⊥ then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
  else (↑𝓕 : ι → MeasurableSpace Ω) i) =
  (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, hi, neBot_iff, ne_self_iff_false, if_false]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have rw₂ : (if Ne.{u_2 + 1} (α := Filter ι) ⊥ ⊥ then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
  else (↑𝓕 : ι → MeasurableSpace Ω) i) =
  (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, hi, neBot_iff, ne_self_iff_false, if_false]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have rw₃ : (if False then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j else (↑𝓕 : ι → MeasurableSpace Ω) i) =
  (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, hi, neBot_iff, ne_self_iff_false, if_false]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have rw₄ : (↑𝓕 : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: rw [rightCont_apply, hi, neBot_iff, ne_self_iff_false, if_false]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : SuccOrder ι
𝓕 : 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 : LinearOrder ι
inst_1 : SuccOrder ι
𝓕 : Filtration ι m
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ 𝓕₊ = 𝓕
have h : ∀ (x : ι) (s : Set Ω), MeasurableSet s ↔ MeasurableSet s
Tactic: ext _
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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 Ω
⊢ MeasurableSet s ↔ MeasurableSet s
have h : MeasurableSet s ↔ MeasurableSet s
Tactic: rw [rightCont_eq_of_nhdsGT_eq_bot _ SuccOrder.nhdsGT]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
𝓕 : Filtration ι m
i : ι
hi : IsMax i
this : TopologicalSpace ι := Preorder.topology ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have this₁ : OrderTopology ι
Tactic: haveI : OrderTopology ι := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
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 ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
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 : LinearOrder ι
𝓕 : Filtration ι m
i : ι
hi : ∃ j > i, Set.Ioo i j = ∅
this_1 : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have obtain : ∀ (j : ι) (hij : j > i) (hIoo : Set.Ioo i j = ∅), (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
Tactic: obtain ⟨j, hij, hIoo⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
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 = ∅
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = (↑𝓕 : ι → MeasurableSpace Ω) i
have hcov : i ⋖ j
Tactic: have hcov : i ⋖ j := covBy_iff_Ioo_eq.mpr ⟨hij, hIoo⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : PartialOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι m
i : ι
inst_3 : (𝓝[>] i).NeBot
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
have rw : (if (𝓝[>] i).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j else (↑𝓕 : ι → MeasurableSpace Ω) i) =
  ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
Tactic: rw [rightCont_apply, if_pos ‹(𝓝[>] i).NeBot›]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
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
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
have rw₁ : Eq.{u_1 + 1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)
  (⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j)
Tactic: rw [rightCont_apply, if_pos ‹(𝓝[>] i).NeBot›]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this : TopologicalSpace ι := Preorder.topology ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
have this₁ : OrderTopology ι
Tactic: haveI : OrderTopology ι := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
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 ι
⊢ (↑𝓕₊ : ι → MeasurableSpace Ω) i = ⨅ (j : ι), ⨅ (_ : j > i), (↑𝓕 : ι → MeasurableSpace Ω) j
have this₁ : (𝓝[>] i).NeBot
Tactic: have : (𝓝[>] i).NeBot := nhdsGT_neBot_of_exists_gt (not_isMax_iff.mp hi)