-- 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)))
h1 :
  MeasurableSet (α := (i : ↥I) → 𝓧 (↑i : S))
    ((↑Finset.univ : Set ↥I).pi (α := fun (i : ↥I) ↦ 𝓧 (↑i : S)) fun (i : ↥I) ↦ s (↑i : S))
h₁ :
  ∀ (ω : α)
    (hω :
      (((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal)
          (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)) ∩
            Y ⁻¹' t) =
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal)
              (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))) :
            ENNReal)
          ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)),
    (((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' (↑I : Set S).pi (α := 𝓧) s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)

Tactic:
filter_upwards [(h I).measure_inter_preimage_eq_mul _ _ h1 ht] with ω hω

Premises used: ProbabilityTheory.Kernel.IndepFun.measure_inter_preimage_eq_mul