-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
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η_1 : 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ω :
  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)
    (∏ 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)))))
    (∏ i : ↥I,
      (((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (j : T (↑i : S)) ↦ X (↑i : S) j ω) ⁻¹'
          (↑(J (↑i : S)) : Set (T (↑i : S))).pi (α := 𝓧 (↑i : S)) (t (↑i : S))))
have h₁ : ∀ (x : ↥I),
  Eq.{u_3 + 1} (α := Set Ω)
    (preimage (β := (j : ↥(J (↑x : S))) → 𝓧 (↑x : S) (↑j : T (↑x : S)))
      (fun (ω : Ω) (j : ↥(J (↑x : S))) ↦ X (↑x : S) (↑j : T (↑x : S)) ω)
      ((↑Finset.univ : Set ↥(J (↑x : S))).pi (α := fun (j : ↥(J (↑x : S))) ↦ 𝓧 (↑x : S) (↑j : T (↑x : S)))
        fun (j : ↥(J (↑x : S))) ↦ t (↑x : S) (↑j : T (↑x : S))))
    ((fun (ω : Ω) (j : T (↑x : S)) ↦ X (↑x : S) j ω) ⁻¹'
      (↑(J (↑x : S)) : Set (T (↑x : S))).pi (α := 𝓧 (↑x : S)) (t (↑x : S)))
Tactic: congrm ∏ _, κ ω ?_