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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i j
s : Finset S
f_1 : S → Set Ω
g : (i : S) → Set ((fun (i : S) ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i = f_1 i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f_1 i) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i)
h3' :
  ∀ (a : α),
    Eq (α := ENNReal) (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f_1 i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i))
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : (↑(I i) : Type u_5)) → 𝓧 i (↑a : T i))
hI : ∀ (i : S) (hi : i ∈ s), (I i).Countable
hu : ∀ (i : S) (hi : i ∈ s), g i = (I i).restrict (π := 𝓧 i) ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i)
      (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
a : α
f : (i : S) → (j : T i) → Ω → 𝓧 i j
i : S
hi : i ∈ s
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i) :
      ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
      ENNReal)
have rw : Eq (α := ENNReal)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
      ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
    ENNReal)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
      ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
    ENNReal)
Tactic: rw [hu i hi]
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun (i : S) ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i = f i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i)
h3' :
  ∀ (a : α),
    Eq (α := ENNReal) (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i))
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : (↑(I i) : Type u_5)) → 𝓧 i (↑a : T i))
hI : ∀ (i : S) (hi : i ∈ s), (I i).Countable
hu : ∀ (i : S) (hi : i ∈ s), g i = (I i).restrict (π := 𝓧 i) ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i)
      (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (ω : Ω) (j : T i) ↦ X' i j ω) ⁻¹' g i) :
        ENNReal)
      (∏ x ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T x) ↦ X' x j ω) ⁻¹' g x) :
        ENNReal)
have h4' : ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
  Eq (α := ENNReal)
    (∏ i ∈ s,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i))
    (∏ i ∈ s,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i))
Tactic: have h4' a (f : (i : S) → (j : T i) → Ω → 𝓧 i j) :
      ∏ i ∈ s, κ a ((fun i ω j ↦ f i j ω) i ⁻¹' g i) =
      ∏ i ∈ s, κ a ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).restrict ⁻¹' u i) := by
    refine Finset.prod_congr rfl fun i hi ↦ ?_
    rw [hu i hi]
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun (i : S) ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i = f i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i)
h3' :
  ∀ (a : α),
    Eq (α := ENNReal) (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i))
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : (↑(I i) : Type u_5)) → 𝓧 i (↑a : T i))
hI : ∀ (i : S) (hi : i ∈ s), (I i).Countable
hu : ∀ (i : S) (hi : i ∈ s), g i = (I i).restrict (π := 𝓧 i) ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i)
      (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
h4' :
  ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq (α := ENNReal)
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i))
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (ω : Ω) (j : T i) ↦ X' i j ω) ⁻¹' g i) :
        ENNReal)
      (∏ x ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T x) ↦ X' x j ω) ⁻¹' g x) :
        ENNReal)
have h5 : ∀ᵐ (a : α) ∂P,
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) i ⁻¹' g i) :
      ENNReal)
    (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) i ⁻¹' g i) :
      ENNReal)
Tactic: have h5 := h1 s (fun i hi ↦ ⟨g i, mg i hi, rfl⟩)
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun (i : S) ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i = f i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i)
h3' :
  ∀ (a : α),
    Eq (α := ENNReal) (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i))
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : (↑(I i) : Type u_5)) → 𝓧 i (↑a : T i))
hI : ∀ (i : S) (hi : i ∈ s), (I i).Countable
hu : ∀ (i : S) (hi : i ∈ s), g i = (I i).restrict (π := 𝓧 i) ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i)
      (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
h4' :
  ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq (α := ENNReal)
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i))
h6 :
  ∀ (i : S) (f : (j : T i) → Ω → 𝓧 i j),
    Eq.{u_3 + 1} (α := Set Ω) ((fun (ω : Ω) (j : T i) ↦ f j ω) ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
      ((fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ f (↑j : T i) ω) ⁻¹' u i)
h5 :
  ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ X i (↑j : T i) ω) ⁻¹' u i) :
        ENNReal)
      (∏ x ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : (↑(I x) : Type u_5)) ↦ X x (↑j : T x) ω) ⁻¹' u x) :
        ENNReal)
i : S
hi : i ∈ (↑s : Set S)
⊢ ∀ᵐ (x : α) ∂P,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)).EventuallyEq (β :=
      (j : (↑(I i) : Type u_5)) → 𝓧 i (↑j : T i)) (fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ X i (↑j : T i) ω)
      fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ X' i (↑j : T i) ω
have this : Countable.{u_5 + 1} (↑(I i) : Type u_5)
Tactic: have := (hI i hi).to_subtype
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
have inl : ∀
  (h :
    ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
      iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
        (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ 0),
  iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ 0
Tactic: obtain rfl | hμ := eq_or_ne P 0
Cleared hypotheses: P, 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
inl :
  ∀
    (h :
      ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
        iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
          (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ 0),
    iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ 0
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
have inr : ∀ (hμ : P ≠ 0), iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
Tactic: obtain rfl | hμ := eq_or_ne P 0
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
have inr : ∀ (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η),
  iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
Tactic: obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[P] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel (h ∅ fun _ ↦ ∅).ae_isProbabilityMeasure 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
have inr : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) η P
Tactic: apply iIndepFun.congr (Filter.EventuallyEq.symm η_eq)
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) η P
have π_pi : ∀ (i : S), IsPiSystem (π i)
Tactic: have π_pi i : IsPiSystem (π i) :=
    (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp)).comap _
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
i : S
⊢ MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
    generateFrom (π i)
have rw : generateFrom
    (image (α := Set ((j : T i) → 𝓧 i j)) (preimage fun (ω : Ω) (j : T i) ↦ X i j ω)
      (squareCylinders (α := 𝓧 i) fun (i_1 : T i) ↦ {s : Set (𝓧 i i_1) | MeasurableSet s})) =
  generateFrom (π i)
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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) η P
have π_gen : ∀ (i : S),
  MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
    generateFrom (π i)
Tactic: have π_gen i : (MeasurableSpace.pi.comap fun ω j ↦ X i j ω) = generateFrom (π i) := 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen :
  ∀ (i : S),
    MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
      generateFrom (π i)
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) η P
have inr : ∀ (I : Finset S) (s : S → Set Ω) (hs : ∀ i ∈ I, s i ∈ π i),
  ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ I, s i) : ENNReal)
      (∏ i ∈ I, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s i) : ENNReal)
Tactic: refine iIndepSets.iIndep _ (fun i ↦ (measurable_pi_iff.2 (hX i)).comap_le) π π_pi π_gen
    fun I s hs ↦ ?_
-- 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 α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen :
  ∀ (i : S),
    MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
      generateFrom (π i)
I : Finset S
s : S → Set Ω
hs : ∀ i ∈ I, s i ∈ π i
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ I, s i) : ENNReal)
      (∏ i ∈ I, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s i) : ENNReal)
have hs₁ : ∀ i ∈ I,
  ∃ (s_1 : Finset (T i)) (t : (i_1 : T i) → Set (𝓧 i i_1)),
    (∀ (i_1 : T i), MeasurableSet (t i_1)) ∧
      (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑s_1 : Set (T i)).pi (α := 𝓧 i) t = s i
Tactic: simp only [squareCylinders, Set.mem_pi, Set.mem_univ, Set.mem_setOf_eq, forall_const,
    ↓existsAndEq, and_true, π] at hs
Cleared hypotheses: hs