awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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 : ι))))

Tactic:
comap_mono (measurable_restrict₂ hst).comap_le

Premises used: MeasurableSpace.comap_mono, Finset.measurable_restrict₂, 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
⊢ 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 : ι))))

Tactic:
exact comap_mono (measurable_restrict₂ hst).comap_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → MeasurableSpace (X i)
s : Finset ι
⊢ Eq (α := MeasurableSpace ((i : ι) → X i)) ((↑(piFinset (X := X)) : Finset ι → MeasurableSpace ((i : ι) → X i)) s)
    (MeasurableSpace.comap ((↑s : Set ι).restrict (π := X))
      (MeasurableSpace.pi (X := fun (a : (↑(↑s : Set ι) : Type u_4)) ↦ X (↑a : ι))))

Tactic:
rfl

Premises used: Finset.restrict, Set.restrict, rfl
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
rw :
  Eq (α := Measure ((j : ↥J) → 𝓧 (↑j : T)))
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      J)
    (Measure.map (Finset.restrict₂ (π := 𝓧) hJI ∘ fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
rw₁ : AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P
⊢ Eq (α := Measure ((j : ↥J) → 𝓧 (↑j : T)))
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      J)
    (Measure.map (Finset.restrict₂ (π := 𝓧) hJI)
      ((fun (I : Finset T) ↦
          (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
        I))

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict₂ _).aemeasurable]

Premises used: Measurable.aemeasurable, Finset.measurable_restrict₂, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ Eq (α := Measure ((j : ↥J) → 𝓧 (↑j : T)))
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      J)
    (Measure.map (Finset.restrict₂ (π := 𝓧) hJI ∘ fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)

Tactic:
simp [Finset.restrict_def, Finset.restrict₂_def, Function.comp_def]

Premises used: Function.comp_def, Finset.restrict₂_def, Finset.restrict_def
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P

Tactic:
aemeasurable_pi_lambda _ fun _ ↦ hX _

Premises used: aemeasurable_pi_lambda, Subtype.val
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P

Tactic:
exact aemeasurable_pi_lambda _ fun _ ↦ hX _

Premises used: aemeasurable_pi_lambda
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
I : Finset T
rw :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (I.restrict (π := 𝓧) ∘ fun (ω : Ω) (x : T) ↦ X x ω) P)
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      I)
rw₁ rw₂ :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (x : Ω) ↦ I.restrict (π := 𝓧) fun (x_1 : T) ↦ X x_1 x) P)
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      I)
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T)))
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      I)

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict _).aemeasurable hX,
    Function.comp_def]

Premises used: Measurable.aemeasurable, Finset.measurable_restrict, Function.comp_def, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P) ↔
    ∀ (I : Finset T),
      Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)

Tactic:
⟨fun h I ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
refine_1 :
  ∀
    (h :
      Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
        (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P))
    (I : Finset T),
    Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
refine_2 :
  ∀
    (h :
      ∀ (I : Finset T),
        Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T)))
          (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
          (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)),
    Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P) ↔
    ∀ (I : Finset T),
      Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)

Tactic:
refine ⟨fun h I ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
I : Finset T
⊢ AEMeasurable (α := (x : T) → 𝓧 x) (_m := MeasurableSpace.pi (X := 𝓧)) (I.restrict (π := 𝓧))
    (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
I : Finset T
rw :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (I.restrict (π := 𝓧) ∘ fun (ω : Ω) (x : T) ↦ X x ω) P)
rw₁ rw₂ :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (fun (x : Ω) ↦ I.restrict (π := 𝓧) fun (x_1 : T) ↦ X x_1 x) P)
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX, Function.comp_def]

Premises used: Function.comp_def, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
I : Finset T
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))

Tactic:
have hX' : P.map (fun ω ↦ I.restrict (X · ω)) = (P.map (fun ω ↦ (X · ω))).map I.restrict := by
      rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX, Function.comp_def]
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
I : Finset T
hX' :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))
⊢ AEMeasurable (α := (x : T) → 𝓧 x) (_m := MeasurableSpace.pi (X := 𝓧)) (I.restrict (π := 𝓧))
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
I : Finset T
hX' :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))
rw :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
    (Measure.map (I.restrict (π := 𝓧) ∘ fun (ω : Ω) (x : T) ↦ Y x ω) P)
rw₁ rw₂ :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
    (Measure.map (fun (x : Ω) ↦ I.restrict (π := 𝓧) fun (x_1 : T) ↦ Y x_1 x) P)
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P))

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hY, Function.comp_def]

Premises used: Function.comp_def, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
I : Finset T
hX' :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P))

Tactic:
have hY' : P.map (fun ω ↦ I.restrict (Y · ω)) = (P.map (fun ω ↦ (Y · ω))).map I.restrict := by
      rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hY, Function.comp_def]
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
I : Finset T
hX' :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))
hY' :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P))
refine_1 :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T)))
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
refine_1₁ :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T)))
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P))
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P))
refine_1₂ refine_1₃ :
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T)))
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P))
    (Measure.map (I.restrict (π := 𝓧)) (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P))
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)

Tactic:
rw [hX', hY', h]
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  ∀ (I : Finset T),
    Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
⊢ IsProjectiveLimit (α := 𝓧) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P) fun (I : Finset T) ↦
    Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P

Tactic:
have hX' := isProjectiveLimit_map hX
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  ∀ (I : Finset T),
    Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
hX' :
  IsProjectiveLimit (α := 𝓧) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P) fun (I : Finset T) ↦
    Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P
⊢ IsProjectiveLimit (α := 𝓧) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P) fun (I : Finset T) ↦
    Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P

Tactic:
simp_rw [h] at hX'
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  ∀ (I : Finset T),
    Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
hX' :
  IsProjectiveLimit (α := 𝓧) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P) fun (I : Finset T) ↦
    Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)

Tactic:
hX'.unique (isProjectiveLimit_map hY)

Premises used: ProbabilityTheory.isProjectiveLimit_map, MeasureTheory.IsProjectiveLimit.unique
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h :
  ∀ (I : Finset T),
    Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
hX' :
  IsProjectiveLimit (α := 𝓧) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P) fun (I : Finset T) ↦
    Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)

Tactic:
exact hX'.unique (isProjectiveLimit_map hY)

Premises used: ProbabilityTheory.isProjectiveLimit_map, MeasureTheory.IsProjectiveLimit.unique
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
⊢ IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P ↔
    ∀ (I : Finset T),
      IdentDistrib (γ := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω)
        (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P P

Tactic:
⟨fun h I ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨hX, hY, ?_⟩⟩

Premises used: Iff.intro, ProbabilityTheory.IdentDistrib.mk
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
refine_1 :
  ∀ (h : IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P)
    (I : Finset T), AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P
refine_2 :
  ∀ (h : IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P)
    (I : Finset T), AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P
refine_3 :
  ∀ (h : IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P)
    (I : Finset T),
    Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
refine_4 :
  ∀
    (h :
      ∀ (I : Finset T),
        IdentDistrib (γ := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω)
          (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P P),
    Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
⊢ IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P ↔
    ∀ (I : Finset T),
      IdentDistrib (γ := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω)
        (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P P

Tactic:
refine ⟨fun h I ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨hX, hY, ?_⟩⟩
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h : IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P
I : Finset T
⊢ AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P

Tactic:
(Finset.measurable_restrict _).comp_aemeasurable hX

Premises used: Finset.measurable_restrict, Finset.restrict, Measurable.comp_aemeasurable