-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
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 X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun (i : S) ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i = f i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i)
h3' :
  ∀ (a : α),
    Eq (α := ENNReal) (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i))
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : (↑(I i) : Type u_5)) → 𝓧 i (↑a : T i))
hI : ∀ (i : S) (hi : i ∈ s), (I i).Countable
hu : ∀ (i : S) (hi : i ∈ s), g i = (I i).restrict (π := 𝓧 i) ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i)
      (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
h4' :
  ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    Eq (α := ENNReal)
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i))
      (∏ i ∈ s,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i))
h5 :
  ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
        ENNReal)
      (∏ x ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T x) ↦ X x j ω) ⁻¹' (I x).restrict (π := 𝓧 x) ⁻¹' u x) :
        ENNReal)
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (ω : Ω) (j : T i) ↦ X' i j ω) ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
        ENNReal)
      (∏ x ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T x) ↦ X' x j ω) ⁻¹' (I x).restrict (π := 𝓧 x) ⁻¹' u x) :
        ENNReal)
have h6 : ∀ (i : S) (f : (j : T i) → Ω → 𝓧 i j),
  Eq.{u_3 + 1} (α := Set Ω) ((fun (ω : Ω) (j : T i) ↦ f j ω) ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
    ((fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ f (↑j : T i) ω) ⁻¹' u i)
Tactic: have h6 i (f : (j : T i) → Ω → 𝓧 i j) : (fun ω j ↦ f j ω) ⁻¹' (I i).restrict ⁻¹' (u i) =
      (fun ω (j : I i) ↦ f j ω) ⁻¹' (u i) := rfl