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 : (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 Ω
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
inr :
  ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) :
        ENNReal)
      (∏ i ∈ I,
          (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t 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:
simp_rw [Set.iInter₂_congr (fun i hi ↦ (hs i hi).symm),
    I.prod_congr rfl (fun i hi ↦ congrArg _ (hs i hi).symm)]

Premises used: congrArg, Finset.prod_congr, Set.iInter₂_congr, Eq.symm, 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)
I : Finset S
s : S → Set Ω
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
h₁ :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω)
        (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) x ↔
      Membership.mem (γ := Set Ω)
        (⋂ (i : ↥I),
          ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
            preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
              (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
              ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
                fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S))))
        x
⊢ Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
    (⋂ (i : ↥I),
      ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
        preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
          (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
          ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
            fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑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 α
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 Ω
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
x : Ω
⊢ Membership.mem (γ := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
      x ↔
    Membership.mem (γ := Set Ω)
      (⋂ (i : ↥I),
        ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
          preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
            (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
            ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
              fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑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 α
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 Ω
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
⊢ Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
    (⋂ (i : ↥I),
      ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
        preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
          (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
          ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
            fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S))))

Tactic:
have : (⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' .pi (J i) (t i)) =
      (⋂ i ∈ (.univ : Finset I), (fun ω (j : J i) ↦ X i j ω) ⁻¹'
        .pi (SetLike.coe Finset.univ) (fun j ↦ t i j)) := 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 α
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 Ω
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
this :
  Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
    (⋂ (i : ↥I),
      ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
        preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
          (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
          ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
            fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S))))
⊢ ∀ (i : ↥I) (hi : Membership.mem (γ := Finset ↥I) Finset.univ i),
    MeasurableSet (α := (i_1 : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑i_1 : T (↑i : S)))
      ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
        fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S)))

Tactic:
have h' (i : I) (hi : i ∈ Finset.univ) :
      MeasurableSet <| (SetLike.coe Finset.univ).pi fun (j : J i) ↦ t i j :=
    .pi (Finset.countable_toSet _) (fun _ _ ↦ ht _ i.2 _)
-- 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), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
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

Tactic:
process_congr ?_ (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk.symm)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, ProbabilityTheory.Kernel.iIndepFun.process_congr, 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 α
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), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
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
refine :
  iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ AEMeasurable.mk (X i j) ⋯ ω) κ P
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P

Tactic:
refine process_congr ?_ (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk.symm)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, ProbabilityTheory.Kernel.iIndepFun.process_congr, 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 α
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), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
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) ↦ AEMeasurable.mk (X i j) ⋯ ω) κ P

Tactic:
iIndepFun_process (fun i j ↦ (hX i j).measurable_mk) fun I J ↦ ?_

Premises used: ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process, 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 α
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), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
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
refine :
  ∀ (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)) ↦ AEMeasurable.mk (X (↑i : S) (↑j : T (↑i : S))) ⋯ ω) κ P
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ AEMeasurable.mk (X i j) ⋯ ω) κ P

Tactic:
refine iIndepFun_process (fun i j ↦ (hX i j).measurable_mk) fun I J ↦ ?_

Premises used: ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process, 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 α
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), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
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
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)) ↦ AEMeasurable.mk (X (↑i : S) (↑j : T (↑i : S))) ⋯ ω) κ P

Tactic:
(h I J).process_congr (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, ProbabilityTheory.Kernel.iIndepFun.process_congr, 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 α
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), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
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
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)) ↦ AEMeasurable.mk (X (↑i : S) (↑j : T (↑i : S))) ⋯ ω) κ P

Tactic:
exact (h I J).process_congr (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, ProbabilityTheory.Kernel.iIndepFun.process_congr, AEMeasurable.ae_eq_mk, Subtype.val
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : (fun (ω : Ω) (i : S) ↦ X i ω) ⟂ᵢ[P] Y
h2 : ∀ (i : S), X i =ᶠ[ae P] X' i
⊢ ∀ (i : S),
    ∀ᵐ (a : Unit) ∂Measure.dirac (),
      X i =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit P : (a : Unit) → Measure Ω) a : Measure Ω)] X' i

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : Y ⟂ᵢ[P] fun (ω : Ω) (i : S) ↦ X i ω
h2 : ∀ (i : S), X i =ᶠ[ae P] X' i
⊢ ∀ (i : S),
    ∀ᵐ (a : Unit) ∂Measure.dirac (),
      X i =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit P : (a : Unit) → Measure Ω) a : Measure Ω)] X' i

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun (ω : Ω) (i : S) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : T) ↦ Y j ω
hX : ∀ (i : S), X i =ᶠ[ae P] X' i
hY : ∀ (j : T), Y j =ᶠ[ae P] Y' j
⊢ ∀ (i : S),
    ∀ᵐ (a : Unit) ∂Measure.dirac (),
      X i =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit P : (a : Unit) → Measure Ω) a : Measure Ω)] X' i

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun (ω : Ω) (i : S) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : T) ↦ Y j ω
hX : ∀ (i : S), X i =ᶠ[ae P] X' i
hY : ∀ (j : T), Y j =ᶠ[ae P] Y' j
⊢ ∀ (j : T),
    ∀ᵐ (a : Unit) ∂Measure.dirac (),
      Y j =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit P : (a : Unit) → Measure Ω) a : Measure Ω)] Y' j

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
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), (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) ⟂ᵢ[P] Y
inst_2 : IsZeroOrProbabilityMeasure P
⊢ (fun (ω : Ω) (i : S) ↦ X i ω) ⟂ᵢ[P] Y

Tactic:
Kernel.IndepFun.process_indepFun hX hY h

Premises used: ProbabilityTheory.Kernel.IndepFun.process_indepFun, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) ⟂ᵢ[P] Y
inst_2 : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S),
    AEMeasurable (_m := mΩ) (X i)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit P) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) ⟂ᵢ[P] Y
inst_2 : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable (_m := mΩ) Y
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit P) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
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), X ⟂ᵢ[P] fun (ω : Ω) (i : ↥I) ↦ Y (↑i : S) ω
inst_2 : IsZeroOrProbabilityMeasure P
⊢ X ⟂ᵢ[P] fun (ω : Ω) (i : S) ↦ Y i ω

Tactic:
Kernel.IndepFun.indepFun_process hX hY h

Premises used: ProbabilityTheory.Kernel.IndepFun.indepFun_process, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst : MeasurableSpace 𝓧
inst_1 : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun (ω : Ω) (i : ↥I) ↦ Y (↑i : S) ω
inst_2 : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable (_m := mΩ) X
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit P) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst : MeasurableSpace 𝓧
inst_1 : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun (ω : Ω) (i : ↥I) ↦ Y (↑i : S) ω
inst_2 : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S),
    AEMeasurable (_m := mΩ) (Y i)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit P) : (a : Unit) → Measure Ω))

Tactic:
simpa