awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_3 : ∀ (i : ι), BorelSpace.{u_3} (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ Measurable (u i) ∧ IsSeparable (Set.range (u i))

Tactic:
⟨measurable_iff_comap_le.2 le_rfl, (hum i).isSeparable_range⟩

Premises used: Iff.mpr, le_rfl, MeasureTheory.StronglyMeasurable.isSeparable_range, measurable_iff_comap_le, And.intro
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_3 : ∀ (i : ι), BorelSpace.{u_3} (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ Measurable (u i) ∧ IsSeparable (Set.range (u i))

Tactic:
exact ⟨measurable_iff_comap_le.2 le_rfl, (hum i).isSeparable_range⟩
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : Type u_3
mi : MeasurableSpace ι
mβ : MeasurableSpace β
f : Filtration ι m
b : β
x : ι
⊢ Measurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic x) : Type u_2) Ω) ↦ (fun (x : ι) (x_1 : Ω) ↦ b) (↑p.1 : ι) p.2

Tactic:
measurable_const

Premises used: measurable_const
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : Type u_3
mi : MeasurableSpace ι
mβ : MeasurableSpace β
f : Filtration ι m
b : β
x : ι
⊢ Measurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic x) : Type u_2) Ω) ↦ (fun (x : ι) (x_1 : Ω) ↦ b) (↑p.1 : ι) p.2

Tactic:
exact measurable_const

Premises used: measurable_const
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
⊢ u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)

Tactic:
have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
    rfl
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
rw :
  Measurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x))
⊢ Measurable (u i)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
⊢ Measurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x))

Tactic:
(h i).comp measurable_prodMk_left

Premises used: Measurable.comp, measurable_prodMk_left
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
⊢ Measurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x))

Tactic:
exact (h i).comp measurable_prodMk_left

Premises used: Measurable.comp, measurable_prodMk_left
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
⊢ Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))

Tactic:
have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
    (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
      (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) := rfl
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
rw :
  Measurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ Measurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (fun (i : ι) (ω : Ω) ↦ u (t i ω) ω) (↑p.1 : ι) p.2

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ Measurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))

Tactic:
(h i).comp ((ht i).subtype_mk.prodMk measurable_snd)

Premises used: Measurable.comp, Measurable.subtype_mk, Measurable.prodMk, measurable_snd
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ Measurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))

Tactic:
exact (h i).comp ((ht i).subtype_mk.prodMk measurable_snd)

Premises used: Measurable.comp, Measurable.subtype_mk, Measurable.prodMk, measurable_snd
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u v : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst_1 : Mul β
inst_2 : MeasurableMul₂ β
hu : IsProgressive f u
hv : IsProgressive f v
⊢ IsProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (ω : Ω) ↦ u i ω * v i ω

Tactic:
fun i ↦ Measurable.mul (hu i) (hv i)

Premises used: Measurable.mul, MeasureTheory.IsProgressive
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
mi : MeasurableSpace ι
mβ : MeasurableSpace β
γ : Type u_4
inst_1 : CommMonoid β
inst_2 : MeasurableMul₂ β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsProgressive f (U c)
⊢ IsProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (ω : Ω) ↦ ∏ c ∈ s, U c i ω

Tactic:
fun i ↦ s.measurable_prod fun c hc ↦ h c hc i

Premises used: Finset.measurable_prod, MeasureTheory.IsProgressive
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst_1 : Group β
inst_2 : MeasurableInv β
hu : IsProgressive f u
⊢ IsProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (ω : Ω) ↦ (u i ω)⁻¹

Tactic:
fun i ↦ (hu i).inv

Premises used: MeasureTheory.IsProgressive, Measurable.inv
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u v : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst_1 : Group β
inst_2 : MeasurableDiv₂ β
hu : IsProgressive f u
hv : IsProgressive f v
⊢ IsProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (ω : Ω) ↦ u i ω / v i ω

Tactic:
fun i ↦ Measurable.div (hu i) (hv i)

Premises used: Measurable.div, MeasureTheory.IsProgressive
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst_1 : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst_2 : NormedAddCommGroup β
inst_3 : OpensMeasurableSpace β
hu : IsProgressive f u
i : ι
inst : OpensMeasurableSpace β
⊢ Measurable (β := ℝ) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (fun (t : ι) (ω : Ω) ↦ ‖u t ω‖) (↑p.1 : ι) p.2

Tactic:
apply @(hu i).norm

Premises used: Measurable.norm
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : OpensMeasurableSpace β
hu : IsProgressive f u
i : ι
⊢ OpensMeasurableSpace β

Tactic:
infer_instance
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
f : Filtration ι m
b : β
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f fun (x : ι) (x_1 : Ω) ↦ b

Tactic:
fun i =>
  @stronglyMeasurable_const _ _ (Subtype.instMeasurableSpace.prod (f i)) _ _

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.IsStronglyProgressive
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
⊢ u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)

Tactic:
have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
    rfl
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
rw :
  StronglyMeasurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x))
⊢ StronglyMeasurable (u i)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
⊢ StronglyMeasurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x))

Tactic:
(h i).comp_measurable measurable_prodMk_left

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_prodMk_left
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this :
  u i =
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x)
⊢ StronglyMeasurable.{u_1, u_3} (α := Ω) (β := (fun (i : ι) ↦ β) i)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘ fun (x : Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) i ⋯, x))

Tactic:
exact (h i).comp_measurable measurable_prodMk_left

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_prodMk_left
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
t : ι → Ω → ι
inst_3 : TopologicalSpace ι
inst_4 : BorelSpace ι
inst_5 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
⊢ Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))

Tactic:
have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
    (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
      (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) := rfl
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
t : ι → Ω → ι
inst_3 : TopologicalSpace ι
inst_4 : BorelSpace ι
inst_5 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
rw :
  StronglyMeasurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (fun (i : ι) (ω : Ω) ↦ u (t i ω) ω) (↑p.1 : ι) p.2

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
t : ι → Ω → ι
inst_3 : TopologicalSpace ι
inst_4 : BorelSpace ι
inst_5 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ StronglyMeasurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))

Tactic:
(h i).comp_measurable ((ht i).measurable.subtype_mk.prodMk measurable_snd)

Premises used: Measurable.subtype_mk, MeasureTheory.StronglyMeasurable.measurable, Measurable.prodMk, MeasureTheory.StronglyMeasurable.comp_measurable, measurable_snd
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
t : ι → Ω → ι
inst_3 : TopologicalSpace ι
inst_4 : BorelSpace ι
inst_5 : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  Eq (α := (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → β)
    (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (t (↑p.1 : ι) p.2) p.2)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))
⊢ StronglyMeasurable (α := Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) (β := β)
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) ∘
      fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) (t (↑p.1 : ι) p.2) ⋯, p.2))

Tactic:
exact (h i).comp_measurable ((ht i).measurable.subtype_mk.prodMk measurable_snd)

Premises used: Measurable.subtype_mk, MeasureTheory.StronglyMeasurable.measurable, Measurable.prodMk, MeasureTheory.StronglyMeasurable.comp_measurable, measurable_snd
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u v : ι → Ω → β
inst_2 : MeasurableSpace ι
inst_3 : Mul β
inst_4 : ContinuousMul β
hu : IsStronglyProgressive f u
hv : IsStronglyProgressive f v
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (ω : Ω) ↦ u i ω * v i ω

Tactic:
fun i =>
  (hu i).mul (hv i)

Premises used: MeasureTheory.IsStronglyProgressive, MeasureTheory.StronglyMeasurable.mul
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
γ : Type u_4
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f (∏ c ∈ s, U c)

Tactic:
Finset.prod_induction U (IsStronglyProgressive f) (fun _ _ => .mul)
    (isStronglyProgressive_const _ 1) h

Premises used: MeasureTheory.isStronglyProgressive_const, MeasureTheory.IsStronglyProgressive, Finset.prod_induction, MeasureTheory.IsStronglyProgressive.mul, OfNat.ofNat
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
γ : Type u_4
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f (∏ c ∈ s, U c)

Tactic:
IsStronglyProgressive.finsetProd' h

Premises used: MeasureTheory.IsStronglyProgressive.finsetProd'
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
γ : Type u_4
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
h₁ : Eq (α := ι → Ω → β) (fun (i : ι) (a : Ω) ↦ ∏ c ∈ s, U c i a) (∏ c ∈ s, U c)
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (a : Ω) ↦ ∏ c ∈ s, U c i a

Tactic:
convert! IsStronglyProgressive.finsetProd' h using 1

Premises used: MeasureTheory.IsStronglyProgressive.finsetProd'
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
γ : Type u_4
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
h₁ : ∀ (i : ι) (a : Ω), Eq.{u_3 + 1} (α := β) (∏ c ∈ s, U c i a) ((∏ c ∈ s, U c) i a)
⊢ Eq (α := ι → Ω → β) (fun (i : ι) (a : Ω) ↦ ∏ c ∈ s, U c i a) (∏ c ∈ s, U c)

Tactic:
ext (i a)
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : MeasurableSpace ι
γ : Type u_4
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
i : ι
a : Ω
⊢ Eq.{u_3 + 1} (α := β) (∏ c ∈ s, U c i a) ((∏ c ∈ s, U c) i a)

Tactic:
simp only [Finset.prod_apply]

Premises used: Finset.prod_apply
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
inst_3 : Group β
inst_4 : ContinuousInv β
hu : IsStronglyProgressive f u
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (ω : Ω) ↦ (u i ω)⁻¹

Tactic:
fun i => (hu i).inv

Premises used: MeasureTheory.StronglyMeasurable.inv, MeasureTheory.IsStronglyProgressive