-- 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 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))
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)
h5 :
  ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ X i (↑j : T i) ω) ⁻¹' u i) :
        ENNReal)
      (∏ x ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : (↑(I x) : Type u_5)) ↦ X x (↑j : T x) ω) ⁻¹' u x) :
        ENNReal)
i : S
hi : i ∈ (↑s : Set S)
this : Countable.{u_5 + 1} (↑(I i) : Type u_5)
a : α
ha :
  ∀ (j : (↑(I i) : Type u_5)),
    ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω),
      Eq (α := 𝓧 i (↑j : T i)) (X i (↑j : T i) ω) (X' i (↑j : T i) ω)
⊢ (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β :=
    (j : (↑(I i) : Type u_5)) → 𝓧 i (↑j : T i)) (fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ X i (↑j : T i) ω)
    fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ X' i (↑j : T i) ω
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (a : Ω) ↦
                ∀ (i_1 : (↑(I i) : Type u_5)), Eq (α := 𝓧 i (↑i_1 : T i)) (X i (↑i_1 : T i) a) (X' i (↑i_1 : T i) a))
              x}
          x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq (α := (j : (↑(I i) : Type u_5)) → 𝓧 i (↑j : T i))
                  ((fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ (X i (↑j : T i) ω : 𝓧 i (↑j : T i))) x)
                  ((fun (ω : Ω) (j : (↑(I i) : Type u_5)) ↦ (X' i (↑j : T i) ω : 𝓧 i (↑j : T i))) x))
              x}
          x}
    a
Tactic: filter_upwards [ae_all_iff.2 ha] with ω hω using by simp [hω]