awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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
⊢ 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)
have 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)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict _).aemeasurable hX,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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)
⊢ 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)
have 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)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict _).aemeasurable hX,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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)
have 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)
Tactic: refine ⟨fun h I ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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)
⊢ 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)
have 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)
Tactic: refine ⟨fun h I ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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))
have 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)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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)
⊢ 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))
have 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)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (hypothesis)
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 (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
have 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))
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]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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))
have 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)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hY, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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)
⊢ 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))
have 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)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hY, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (hypothesis)
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) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
have 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))
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]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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))
⊢ 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)
have 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)
Tactic: rw [hX', hY', h]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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)
⊢ 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)
have 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))
Tactic: rw [hX', hY', h]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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))
⊢ 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)
have 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))
Tactic: rw [hX', hY', h]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (hypothesis)
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)
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
have 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
Tactic: have hX' := isProjectiveLimit_map hX
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (hypothesis)
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
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
have 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
Tactic: simp_rw [h] at hX'
Cleared hypotheses: hX'
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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
have 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
Tactic: refine ⟨fun h I ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨hX, hY, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h I ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨hX, hY, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
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
⊢ 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
have 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)
Tactic: refine ⟨fun h I ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨hX, hY, ?_⟩⟩