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 α
𝓧 : 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

Tactic:
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 ?_

Premises used: Iff.mpr, MeasurableSpace.isPiSystem_measurableSet, measurable_pi_iff, Measurable.comap_le, MeasurableSpace.generateFrom_measurableSet, ProbabilityTheory.Kernel.IndepFun, ProbabilityTheory.Kernel.IndepSets.indep, Eq.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 α
𝓧 : 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
refine : IndepSets πX {s : Set Ω | MeasurableSet s} κ P
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ 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 ?_

Premises used: Iff.mpr, MeasurableSpace.isPiSystem_measurableSet, measurable_pi_iff, Measurable.comap_le, MeasurableSpace.generateFrom_measurableSet, ProbabilityTheory.Kernel.IndepSets.indep, Eq.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 α
𝓧 : 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
⊢ ∀ (i : S), MeasurableSet (s i)

Tactic:
simp only [Set.mem_pi, Set.mem_univ, Set.mem_setOf_eq, forall_const] at hs

Premises used: Set.mem_pi, Set.mem_setOf_eq, 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 α
𝓧 : 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)
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
⊢ 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:
ext
-- Module: Mathlib.Probability.Independence.Process.Basic
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)
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:
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 α
𝓧 : 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)))

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
-- Module: Mathlib.Probability.Independence.Process.Basic
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)))
⊢ 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 _)
-- Module: Mathlib.Probability.Independence.Process.Basic
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

Tactic:
.congr' ?_ (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk.symm)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.IndepFun.congr', Filter.EventuallyEq.rfl, AEMeasurable.ae_eq_mk, 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 α
𝓧 : 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 κ
refine : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (AEMeasurable.mk Y hY) κ P
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P

Tactic:
refine .congr' ?_ (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk.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 α
𝓧 : 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 κ
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω) (AEMeasurable.mk Y hY) κ P
h2 :
  ∀ (i : S),
    ∀ᵐ (a : α) ∂P, AEMeasurable.mk (X i) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X i
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (AEMeasurable.mk Y hY) κ P

Tactic:
apply process_congr_left (X := fun i ↦ (hX i).mk (X i))

Premises used: ProbabilityTheory.Kernel.IndepFun.process_congr_left
-- Module: Mathlib.Probability.Independence.Process.Basic
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) ↦ AEMeasurable.mk (X i) ⋯ ω) (AEMeasurable.mk Y hY) κ P

Tactic:
IndepFun.process_indepFun (fun i ↦ (hX i).measurable_mk) hY.measurable_mk
      fun I ↦ process_congr_left (X := fun (i : I) ↦ X i) ?_ (fun i ↦ ?_)

Premises used: ProbabilityTheory.Kernel.IndepFun.process_congr_left, ProbabilityTheory.Kernel.IndepFun.process_indepFun, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Independence.Process.Basic
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 κ
h1 :
  ∀ (I : Finset S),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ (fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i ω)
      (AEMeasurable.mk Y hY) κ P
h1₁ :
  ∀ (I : Finset S) (i : ↥I),
    ∀ᵐ (a : α) ∂P,
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := 𝓧 (↑i : S))
        ((fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i) (AEMeasurable.mk (X (↑i : S)) ⋯)
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω) (AEMeasurable.mk Y hY) κ P

Tactic:
refine IndepFun.process_indepFun (fun i ↦ (hX i).measurable_mk) hY.measurable_mk
      fun I ↦ process_congr_left (X := fun (i : I) ↦ X i) ?_ (fun i ↦ ?_)

Premises used: ProbabilityTheory.Kernel.IndepFun.process_congr_left, ProbabilityTheory.Kernel.IndepFun.process_indepFun, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Independence.Process.Basic
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 κ
I : Finset S
⊢ IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ (fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i ω)
    (AEMeasurable.mk Y hY) κ P

Tactic:
(h I).congr' (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.IndepFun.congr', Filter.EventuallyEq.rfl, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Process.Basic
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 κ
I : Finset S
⊢ IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ (fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i ω)
    (AEMeasurable.mk Y hY) κ P

Tactic:
exact (h I).congr' (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.IndepFun.congr', Filter.EventuallyEq.rfl, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Process.Basic
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 κ
I : Finset S
i : ↥I
⊢ ∀ᵐ (a : α) ∂P,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := 𝓧 (↑i : S))
      ((fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i) (AEMeasurable.mk (X (↑i : S)) ⋯)

Tactic:
Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Subtype.val
-- Module: Mathlib.Probability.Independence.Process.Basic
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 κ
I : Finset S
i : ↥I
⊢ ∀ᵐ (a : α) ∂P,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := 𝓧 (↑i : S))
      ((fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i) (AEMeasurable.mk (X (↑i : S)) ⋯)

Tactic:
exact Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Subtype.val
-- Module: Mathlib.Probability.Independence.Process.Basic
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 κ
⊢ ∀ (i : S),
    ∀ᵐ (a : α) ∂P, AEMeasurable.mk (X i) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X i

Tactic:
fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk.symm

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, 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 α
𝓧 : 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 κ
⊢ ∀ (i : S),
    ∀ᵐ (a : α) ∂P, AEMeasurable.mk (X i) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X i

Tactic:
exact fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk.symm

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, 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 α
𝓧 : Type u_5
𝓨 : S → Type u_6
inst : MeasurableSpace 𝓧
inst_1 : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : Measurable X
hY : ∀ (i : S), Measurable (Y i)
h : ∀ (I : Finset S), IndepFun (γ := (i : ↥I) → 𝓨 (↑i : S)) X (fun (ω : Ω) (i : ↥I) ↦ Y (↑i : S) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (γ := (i : S) → 𝓨 i) X (fun (ω : Ω) (i : S) ↦ Y i ω) κ P

Tactic:
(IndepFun.process_indepFun hY hX (fun I ↦ (h I).symm)).symm

Premises used: ProbabilityTheory.Kernel.IndepFun.process_indepFun, ProbabilityTheory.Kernel.IndepFun.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 α
𝓧 : Type u_5
𝓨 : S → Type u_6
inst : MeasurableSpace 𝓧
inst_1 : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable (_m := mΩ) X ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : ∀ (i : S), AEMeasurable (_m := mΩ) (Y i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (γ := (i : ↥I) → 𝓨 (↑i : S)) X (fun (ω : Ω) (i : ↥I) ↦ Y (↑i : S) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (γ := (i : S) → 𝓨 i) X (fun (ω : Ω) (i : S) ↦ Y i ω) κ P

Tactic:
(IndepFun.process_indepFun₀ hY hX (fun I ↦ (h I).symm)).symm

Premises used: ProbabilityTheory.Kernel.IndepFun.process_indepFun₀, ProbabilityTheory.Kernel.IndepFun.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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), Measurable (X i)
hY : ∀ (j : T), Measurable (Y j)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ X i ω) (fun (ω : Ω) (j : T) ↦ Y j ω) κ P

Tactic:
IndepFun.process_indepFun hX (measurable_pi_lambda _ hY) fun I ↦ ?_

Premises used: measurable_pi_lambda, ProbabilityTheory.Kernel.IndepFun.process_indepFun