-- 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))))
h' :
  ∀ (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)))
h₁ :
  ∀ (ω : α)
    (hω :
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ (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)))) :
          ENNReal)
        (∏ i : ↥I,
            (((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal)
              (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)))) :
          ENNReal))
    (hη :
      Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) ω : Measure Ω)
        ((η : (a : α) → Measure Ω) ω : Measure Ω)),
    Eq (α := ENNReal)
      ((((η : (a : α) → Measure Ω) ω : 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 Ω) ω : 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, (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)

Tactic:
filter_upwards [(h I (fun i ↦ J i)).measure_inter_preimage_eq_mul _ _ .univ h',
    η_eq] with ω hω hη

Premises used: Finset.univ, ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul, Subtype.val