awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
h : Countable.{u_1 + 1} (↑I : Type u_1)
a : α
ha :
  ∀ (i : (↑I : Type u_1)),
    ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), Eq (α := 𝓧 (↑i : S)) (X (↑i : S) ω) (X' (↑i : S) ω)
⊢ (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : (↑I : Type u_1)) → 𝓧 (↑i : S))
    (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω | (fun (a : Ω) ↦ ∀ (i : (↑I : Type u_1)), Eq (α := 𝓧 (↑i : S)) (X (↑i : S) a) (X' (↑i : S) a)) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq (α := (i : (↑I : Type u_1)) → 𝓧 (↑i : S))
                  ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ (X (↑i : S) ω : 𝓧 (↑i : S))) x)
                  ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ (X' (↑i : S) ω : 𝓧 (↑i : S))) x))
              x}
          x}
    a
Tactic: filter_upwards [ae_all_iff.2 ha] with ω hω using by simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
h_1 : Countable.{u_1 + 1} (↑I : Type u_1)
a : α
ha :
  ∀ (i : (↑I : Type u_1)),
    ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), Eq (α := 𝓧 (↑i : S)) (X (↑i : S) ω) (X' (↑i : S) ω)
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω | (fun (a : Ω) ↦ ∀ (i : (↑I : Type u_1)), Eq (α := 𝓧 (↑i : S)) (X (↑i : S) a) (X' (↑i : S) a)) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq (α := (i : (↑I : Type u_1)) → 𝓧 (↑i : S))
                    ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ (X (↑i : S) ω : 𝓧 (↑i : S))) x)
                    ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ (X' (↑i : S) ω : 𝓧 (↑i : S))) x))
                x}
            x}
      a
⊢ (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : (↑I : Type u_1)) → 𝓧 (↑i : S))
    (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω
have h₁ : ∀ (a : Ω),
  (∀ (i : (↑I : Type u_1)), Eq (α := 𝓧 (↑i : S)) (X (↑i : S) a) (X' (↑i : S) a)) →
    Eq (α := (i : (↑I : Type u_1)) → 𝓧 (↑i : S)) (fun (i : (↑I : Type u_1)) ↦ X (↑i : S) a) fun (i : (↑I : Type u_1)) ↦
      X' (↑i : S) a
Tactic: filter_upwards [ae_all_iff.2 ha] with ω hω using by simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
h : Countable.{u_1 + 1} (↑I : Type u_1)
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
have h : ∀ᵐ (a : α) ∂P,
  (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : (↑I : Type u_1)) → 𝓧 (↑i : S))
    (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω
Tactic: have h : ∀ᵐ a ∂P, (fun ω (i : I) ↦ X i ω) =ᵐ[κ a] (fun ω (i : I) ↦ X' i ω) := by
    filter_upwards [ae_all_iff.2 fun (i : I) ↦ h2 i] with
      a (ha : ∀ (i : I), ∀ᵐ ω ∂κ a, X i ω = X' i ω)
    filter_upwards [ae_all_iff.2 ha] with ω hω using by simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
h_1 : Countable.{u_1 + 1} (↑I : Type u_1)
h :
  ∀ᵐ (a : α) ∂P,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β :=
      (i : (↑I : Type u_1)) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω)
      fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω
a : α
ha1 :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
      ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
        ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
ha2 :
  (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : (↑I : Type u_1)) → 𝓧 (↑i : S))
    (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
        ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω) ⁻¹' u) :
        ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
have h₁ : Eq (α := ENNReal)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
      ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
    ENNReal)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
      ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω) ⁻¹' u) :
    ENNReal)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
have πX_pi : IsPiSystem πX
Tactic: have πX_pi : IsPiSystem πX :=
    IsPiSystem.comap (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp)) _
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
⊢ MeasurableSpace.comap (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (MeasurableSpace.pi (X := 𝓧)) =
    generateFrom πX
have rw : generateFrom
    (image (α := Set ((i : S) → 𝓧 i)) (preimage fun (ω : Ω) (i : S) ↦ X i ω)
      (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s})) =
  generateFrom πX
Tactic: rw [generateFrom_squareCylinders.symm, MeasurableSpace.comap_generateFrom]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
have πX_gen : MeasurableSpace.comap (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (MeasurableSpace.pi (X := 𝓧)) = generateFrom πX
Tactic: have πX_gen : (MeasurableSpace.pi.comap fun ω i ↦ X i ω) = generateFrom πX := by
    rw [generateFrom_squareCylinders.symm, MeasurableSpace.comap_generateFrom]
    rfl
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen :
  MeasurableSpace.comap (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (MeasurableSpace.pi (X := 𝓧)) =
    generateFrom πX
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
have refine : IndepSets πX {s : Set Ω | MeasurableSet s} κ P
Tactic: refine IndepSets.indep (measurable_pi_iff.2 hX).comap_le hY.comap_le
    πX_pi (@isPiSystem_measurableSet Ω (.comap Y inferInstance)) πX_gen
    (@generateFrom_measurableSet Ω (.comap Y inferInstance)).symm ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen :
  MeasurableSpace.comap (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (MeasurableSpace.pi (X := 𝓧)) =
    generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
hs :
  Membership.mem (γ := Set ((i : S) → Set (𝓧 i)))
    (Set.pi (α := fun (i : S) ↦ Set (𝓧 i)) univ fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) s
t : Set 𝓨
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
have hs₁ : ∀ (i : S), MeasurableSet (s i)
Tactic: simp only [Set.mem_pi, Set.mem_univ, Set.mem_setOf_eq, forall_const] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen :
  MeasurableSpace.comap (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (MeasurableSpace.pi (X := 𝓧)) =
    generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
⊢ Eq.{u_3 + 1} (α := Set Ω) ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s)
    (preimage (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      ((↑Finset.univ : Set ↥I).pi (α := fun (i : ↥I) ↦ 𝓧 (↑i : S)) fun (i : ↥I) ↦ s (↑i : S)))
have h₁ : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s) x ↔
    Membership.mem (γ := Set Ω)
      (preimage (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
        ((↑Finset.univ : Set ↥I).pi (α := fun (i : ↥I) ↦ 𝓧 (↑i : S)) fun (i : ↥I) ↦ s (↑i : S)))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen :
  MeasurableSpace.comap (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (MeasurableSpace.pi (X := 𝓧)) =
    generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
have this : Eq.{u_3 + 1} (α := Set Ω) ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s)
  (preimage (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    ((↑Finset.univ : Set ↥I).pi (α := fun (i : ↥I) ↦ 𝓧 (↑i : S)) fun (i : ↥I) ↦ s (↑i : S)))
Tactic: have : (fun ω i ↦ X i ω) ⁻¹' .pi I s =
      (fun ω (i : I) ↦ X i ω) ⁻¹' .pi (SetLike.coe Finset.univ) (fun i ↦ s i)
       := by
    ext; simp
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) :=
  {s : Set Ω |
    ∃ (t : Set ((i : S) → 𝓧 i)),
      Membership.mem (γ := Set (Set ((i : S) → 𝓧 i)))
          (squareCylinders (α := 𝓧) fun (i : S) ↦ {s : Set (𝓧 i) | MeasurableSet s}) t ∧
        (fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen :
  MeasurableSpace.comap (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (MeasurableSpace.pi (X := 𝓧)) =
    generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
this :
  Eq.{u_3 + 1} (α := Set Ω) ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s)
    (preimage (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      ((↑Finset.univ : Set ↥I).pi (α := fun (i : ↥I) ↦ 𝓧 (↑i : S)) fun (i : ↥I) ↦ s (↑i : S)))
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
have h1 : MeasurableSet (α := (i : ↥I) → 𝓧 (↑i : S))
  ((↑Finset.univ : Set ↥I).pi (α := fun (i : ↥I) ↦ 𝓧 (↑i : S)) fun (i : ↥I) ↦ s (↑i : S))
Tactic: have h1 : MeasurableSet <| .pi (SetLike.coe Finset.univ) (fun (i : I) ↦ s i) :=
    .pi (Finset.countable_toSet _) (fun _ _ ↦ hs _)
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : AEMeasurable (_m := mΩ) Y ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
have refine : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (AEMeasurable.mk Y hY) κ P
Tactic: refine .congr' ?_ (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk.symm)
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : AEMeasurable (_m := mΩ) Y ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (AEMeasurable.mk Y hY) κ P
have h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) sorry ω) (AEMeasurable.mk Y hY) κ P
Tactic: apply process_congr_left (X := fun i ↦ (hX i).mk (X i))