awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet.{u_1} (α := Ω) Set.univ

Tactic:
exacts [MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩,
      MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩), measurableSet_empty _]

Premises used: MeasurableSpace.measurableSet_empty, MeasurableSet.univ
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_4
inst_1 : Zero E
inst_2 : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
pos :
  ∀ (h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))),
    StronglyMeasurable
      (Classical.choose (p := fun (x : Ω → E) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h)
neg :
  ∀ (h : ¬∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))),
    StronglyMeasurable.{u_1, u_4} (α := Ω) (β := E) 0
⊢ StronglyMeasurable.{u_1, u_4} (α := Ω) (β := E)
    (if h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω)) then
      Classical.choose (p := fun (x : Ω → E) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h
    else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_4
inst_1 : Zero E
inst_2 : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable
    (Classical.choose (p := fun (x : Ω → E) ↦
      StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h)

Tactic:
(Classical.choose_spec h).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_4
inst_1 : Zero E
inst_2 : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ¬∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable.{u_1, u_4} (α := Ω) (β := E) 0

Tactic:
stronglyMeasurable_zero

Premises used: MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_4
inst_1 : Zero E
inst_2 : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable
    (Classical.choose (p := fun (x : Ω → E) ↦
      StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h)

Tactic:
exacts [(Classical.choose_spec h).1, stronglyMeasurable_zero]

Premises used: Classical.choose_spec, And.left, MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_4
inst_1 : Zero E
inst_2 : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable (limitProcess f ℱ μ)

Tactic:
stronglyMeasurable_limitProcess.mono (sSup_le fun _ ⟨_, hn⟩ => hn ▸ ℱ.le _)

Premises used: Eq.rec, _private.0.MeasureTheory.Filtration.stronglyMeasurable_limit_process'.match_1, LE.le, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.le, sSup_le, MeasureTheory.Filtration.stronglyMeasurable_limitProcess
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
pos :
  ∀ (h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))),
    MemLp
      (Classical.choose (p := fun (x : Ω → F) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h)
      p μ
neg :
  ∀ (h : ¬∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))),
    MemLp.{u_1, u_5} (ε := F) 0 p μ
⊢ MemLp.{u_1, u_5} (ε := F)
    (if h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω)) then
      Classical.choose (p := fun (x : Ω → F) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h
    else 0)
    p μ

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ MemLp
    (Classical.choose (p := fun (x : Ω → F) ↦
      StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h)
    p μ

Tactic:
⟨StronglyMeasurable.aestronglyMeasurable
      ((Classical.choose_spec h).1.mono (sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _)),
      lt_of_le_of_lt (Lp.eLpNorm_lim_le_liminf_eLpNorm hfm _ (Classical.choose_spec h).2)
        (lt_of_le_of_lt ?_ (ENNReal.coe_lt_top : ↑R < ∞))⟩

Premises used: lt_of_le_of_lt, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Eq.rec, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, MeasureTheory.MemLp, LE.le, Classical.choose_spec, And.right, And.left, MeasureTheory.StronglyMeasurable.mono, And.intro, MeasureTheory.Filtration.le, _private.0.MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd.match_1, sSup_le, ENNReal.coe_lt_top
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
pos : liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop ≤ (↑R : ℝ≥0∞)
⊢ MemLp
    (Classical.choose (p := fun (x : Ω → F) ↦
      StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h)
    p μ

Tactic:
refine ⟨StronglyMeasurable.aestronglyMeasurable
      ((Classical.choose_spec h).1.mono (sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _)),
      lt_of_le_of_lt (Lp.eLpNorm_lim_le_liminf_eLpNorm hfm _ (Classical.choose_spec h).2)
        (lt_of_le_of_lt ?_ (ENNReal.coe_lt_top : ↑R < ∞))⟩
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
pos : sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ eLpNorm (f b) p μ} ≤ (↑R : ℝ≥0∞)
⊢ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop ≤ (↑R : ℝ≥0∞)

Tactic:
simp_rw [liminf_eq, eventually_atTop]

Premises used: Filter.liminf_eq, Filter.eventually_atTop
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ eLpNorm (f b) p μ} ≤ (↑R : ℝ≥0∞)

Tactic:
sSup_le fun b ⟨a, ha⟩ => (ha a le_rfl).trans (hbdd _)

Premises used: ENNReal.ofNNReal, le_rfl, LE.le, _private.0.MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd.match_2, LE.le.trans, sSup_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ eLpNorm (f b) p μ} ≤ (↑R : ℝ≥0∞)

Tactic:
exact sSup_le fun b ⟨a, ha⟩ => (ha a le_rfl).trans (hbdd _)
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ¬∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ MemLp.{u_1, u_5} (ε := F) 0 p μ

Tactic:
MemLp.zero

Premises used: MeasureTheory.MemLp.zero
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ¬∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ MemLp.{u_1, u_5} (ε := F) 0 p μ

Tactic:
exact MemLp.zero

Premises used: MeasureTheory.MemLp.zero
-- 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 ι
X : ι → Type u_4
inst_4 : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
rw :
  LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (restrictLe (π := X) j)
      (MeasurableSpace.comap (restrictLe₂ (π := X) hij)
        (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι)))))
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic j) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) j)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic j) : Type u_2)) ↦ X (↑a : ι))))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι))))
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic j) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) j)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic j) : Type u_2)) ↦ X (↑a : ι))))

Tactic:
rw [← restrictLe₂_comp_restrictLe hij, ← comap_comp]

Premises used: MeasurableSpace.comap_comp, Preorder.restrictLe₂_comp_restrictLe
-- 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 ι
X : ι → Type u_4
inst_4 : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (restrictLe (π := X) j)
      (MeasurableSpace.comap (restrictLe₂ (π := X) hij)
        (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι)))))
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic j) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) j)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic j) : Type u_2)) ↦ X (↑a : ι))))

Tactic:
comap_mono (measurable_restrictLe₂ _).comap_le

Premises used: MeasurableSpace.comap_mono, Measurable.comap_le, Preorder.measurable_restrictLe₂
-- 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 ι
X : ι → Type u_4
inst_4 : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (restrictLe (π := X) j)
      (MeasurableSpace.comap (restrictLe₂ (π := X) hij)
        (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι)))))
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic j) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) j)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic j) : Type u_2)) ↦ X (↑a : ι))))

Tactic:
exact comap_mono (measurable_restrictLe₂ _).comap_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
a :
  LE.le (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
a₁ :
  LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
    ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
⊢ Eq (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
a :
  LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β :=
      (a : ↥(Finset.Iic i)) → X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) a) : ι))
      (frestrictLe (π := X) i)
      (MeasurableSpace.comap (β := (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))
        (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (δ := ↥(Finset.Iic i))
                (fun (i_1 : (↑(Set.Iic i) : Type u_2)) ↦ X (↑i_1 : ι)) (Equiv.IicFinsetSet i) :
              ((b : ↥(Finset.Iic i)) →
                  X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) ≃ᵐ
                ((a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))) :
          (a :
              (b : ↥(Finset.Iic i)) →
                X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) →
            (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))
        (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι)))))
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))

Tactic:
simp_rw [piLE, ← piCongrLeft_comp_frestrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]

Premises used: MeasurableSpace.comap_comp, MeasureTheory.Filtration.piLE, MeasurableEquiv.coe_piCongrLeft, Preorder.piCongrLeft_comp_frestrictLe
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
⊢ Measurable (α :=
    (a : ↥(Finset.Iic i)) → X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) a) : ι))
    (β := (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))
    (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (δ := ↥(Finset.Iic i))
            (fun (i_1 : (↑(Set.Iic i) : Type u_2)) ↦ X (↑i_1 : ι)) (Equiv.IicFinsetSet i) :
          ((b : ↥(Finset.Iic i)) →
              X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) ≃ᵐ
            ((a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))) :
      (a :
          (b : ↥(Finset.Iic i)) →
            X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) →
        (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β :=
      (a : ↥(Finset.Iic i)) → X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) a) : ι))
      (frestrictLe (π := X) i)
      (MeasurableSpace.comap (β := (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))
        (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (δ := ↥(Finset.Iic i))
                (fun (i_1 : (↑(Set.Iic i) : Type u_2)) ↦ X (↑i_1 : ι)) (Equiv.IicFinsetSet i) :
              ((b : ↥(Finset.Iic i)) →
                  X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) ≃ᵐ
                ((a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))) :
          (a :
              (b : ↥(Finset.Iic i)) →
                X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) →
            (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))
        (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι)))))
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))

Tactic:
exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)

Premises used: MeasurableSpace.comap_mono, Measurable.comap_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
a :
  LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β :=
      (a : (↑(Set.Iic i) : Type u_2)) →
        X (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) a) : ι))
      (restrictLe (π := X) i)
      (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι))
        (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (fun (i_1 : ↥(Finset.Iic i)) ↦ X (↑i_1 : ι))
                (Equiv.symm (Equiv.IicFinsetSet i)) :
              ((b : (↑(Set.Iic i) : Type u_2)) →
                  X
                    (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) :
                      ι)) ≃ᵐ
                ((a : ↥(Finset.Iic i)) → X (↑a : ι))) :
          (a :
              (b : (↑(Set.Iic i) : Type u_2)) →
                X (↑(((Equiv.IicFinsetSet i).symm : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) : ι)) →
            (a : ↥(Finset.Iic i)) → X (↑a : ι))
        (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι)))))
    ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
    ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)

Tactic:
rw [← piCongrLeft_comp_restrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]

Premises used: MeasurableSpace.comap_comp, MeasurableEquiv.coe_piCongrLeft, Preorder.piCongrLeft_comp_restrictLe
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
⊢ Measurable (α :=
    (a : (↑(Set.Iic i) : Type u_2)) →
      X (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) a) : ι))
    (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι))
    (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (fun (i_1 : ↥(Finset.Iic i)) ↦ X (↑i_1 : ι))
            (Equiv.symm (Equiv.IicFinsetSet i)) :
          ((b : (↑(Set.Iic i) : Type u_2)) →
              X (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) : ι)) ≃ᵐ
            ((a : ↥(Finset.Iic i)) → X (↑a : ι))) :
      (a :
          (b : (↑(Set.Iic i) : Type u_2)) →
            X (↑(((Equiv.IicFinsetSet i).symm : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) : ι)) →
        (a : ↥(Finset.Iic i)) → X (↑a : ι))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β :=
      (a : (↑(Set.Iic i) : Type u_2)) →
        X (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) a) : ι))
      (restrictLe (π := X) i)
      (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι))
        (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (fun (i_1 : ↥(Finset.Iic i)) ↦ X (↑i_1 : ι))
                (Equiv.symm (Equiv.IicFinsetSet i)) :
              ((b : (↑(Set.Iic i) : Type u_2)) →
                  X
                    (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) :
                      ι)) ≃ᵐ
                ((a : ↥(Finset.Iic i)) → X (↑a : ι))) :
          (a :
              (b : (↑(Set.Iic i) : Type u_2)) →
                X (↑(((Equiv.IicFinsetSet i).symm : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) : ι)) →
            (a : ↥(Finset.Iic i)) → X (↑a : ι))
        (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι)))))
    ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)

Tactic:
exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)

Premises used: MeasurableSpace.comap_mono, Measurable.comap_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι_1 : Type u_2
m : MeasurableSpace Ω
β : ι_1 → Type u_3
inst : (i : ι_1) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι_1), MetrizableSpace.{u_3} (β i)
mβ : (i : ι_1) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι_1), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι_1
ι : Type u_4
X : ι → Type u_5
inst_4 : (i : ι) → MeasurableSpace (X i)
s t : Finset ι
hst : s ≤ t
rw :
  LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (t.restrict (π := X))
      (MeasurableSpace.comap (restrict₂ (π := X) hst) (MeasurableSpace.pi (X := fun (a : ↥s) ↦ X (↑a : ι)))))
    (MeasurableSpace.comap (t.restrict (π := X)) (MeasurableSpace.pi (X := fun (a : ↥t) ↦ X (↑a : ι))))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (s.restrict (π := X)) (MeasurableSpace.pi (X := fun (a : ↥s) ↦ X (↑a : ι))))
    (MeasurableSpace.comap (t.restrict (π := X)) (MeasurableSpace.pi (X := fun (a : ↥t) ↦ X (↑a : ι))))

Tactic:
rw [← restrict₂_comp_restrict hst, ← comap_comp]

Premises used: MeasurableSpace.comap_comp, Finset.restrict₂_comp_restrict