awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Process.Basic
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)
this : Countable.{u_5 + 1} (↑(I i) : Type u_5)
a : α
ha :
  ∀ (j : (↑(I i) : Type u_5)),
    ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω),
      Eq (α := 𝓧 i (↑j : T i)) (X i (↑j : T i) ω) (X' i (↑j : T i) ω)
ω : Ω
hω : ∀ (i_1 : (↑(I i) : Type u_5)), Eq (α := 𝓧 i (↑i_1 : T i)) (X i (↑i_1 : T i) ω) (X' i (↑i_1 : T i) ω)
⊢ Eq (α := (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) ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Independence.Process.Basic
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
inr : ∀ (hμ : P ≠ 0), iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
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)) ω) κ 0
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Process.Basic
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 α Ω),
    Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω) ∧
      IsMarkovKernel η

Tactic:
exists_ae_eq_isMarkovKernel (h ∅ fun _ ↦ ∅).ae_isProbabilityMeasure hμ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, EmptyCollection.emptyCollection, ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Process.Basic
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
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
⊢ 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μ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, EmptyCollection.emptyCollection, ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure, ProbabilityTheory.Kernel
-- Module: Mathlib.Probability.Independence.Process.Basic
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 η
inr : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) η P
⊢ 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)

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Process.Basic
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}
i : S
⊢ ∀ (i_1 : T i), Membership.mem (γ := Set (Set (𝓧 i i_1))) {s : Set (𝓧 i i_1) | MeasurableSet s} univ

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Process.Basic
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}
⊢ ∀ (i : S), IsPiSystem (π i)

Tactic:
have π_pi i : IsPiSystem (π i) :=
    (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp)).comap _
-- Module: Mathlib.Probability.Independence.Process.Basic
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
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)
⊢ MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
    generateFrom (π i)

Tactic:
rw [generateFrom_squareCylinders.symm, MeasurableSpace.comap_generateFrom]

Premises used: MeasureTheory.generateFrom_squareCylinders, Eq.symm, MeasurableSpace.comap_generateFrom
-- Module: Mathlib.Probability.Independence.Process.Basic
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
⊢ 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:
rfl
-- Module: Mathlib.Probability.Independence.Process.Basic
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)

Tactic:
have π_gen i : (MeasurableSpace.pi.comap fun ω j ↦ X i j ω) = generateFrom (π i) := by
    rw [generateFrom_squareCylinders.symm, MeasurableSpace.comap_generateFrom]
    rfl
-- Module: Mathlib.Probability.Independence.Process.Basic
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

Tactic:
iIndepSets.iIndep _ (fun i ↦ (measurable_pi_iff.2 (hX i)).comap_le) π π_pi π_gen
    fun I s hs ↦ ?_

Premises used: Iff.mpr, measurable_pi_iff, ProbabilityTheory.Kernel.iIndepSets.iIndep, Measurable.comap_le, ProbabilityTheory.Kernel.iIndepFun
-- Module: Mathlib.Probability.Independence.Process.Basic
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)
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)
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) η P

Tactic:
refine iIndepSets.iIndep _ (fun i ↦ (measurable_pi_iff.2 (hX i)).comap_le) π π_pi π_gen
    fun I s hs ↦ ?_

Premises used: Iff.mpr, measurable_pi_iff, ProbabilityTheory.Kernel.iIndepSets.iIndep, Measurable.comap_le
-- Module: Mathlib.Probability.Independence.Process.Basic
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
⊢ ∀ 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

Premises used: and_true, ExistsAndEq.existsAndEq, Set.mem_pi, Set.mem_setOf_eq, MeasureTheory.squareCylinders, Set.mem_univ, forall_const
-- Module: Mathlib.Probability.Independence.Process.Basic
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_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
inr :
  ∀ (J : (i : S) → Finset (T i)) (t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1))
    (ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1))
    (hs : ∀ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i) = s 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)
⊢ ∀ᵐ (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:
choose! J t ht hs using hs