awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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
⊢ ∀ (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)

Tactic:
have h4 (f : (i : S) → (j : T i) → Ω → 𝓧 i j) : ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' g i =
      ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' (I i).restrict ⁻¹' u i :=
      (biInf_congr (fun i hi ↦ by rw [hu i hi])).symm
-- 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 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_1 : 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_1 i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f_1 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_1 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)
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))

Tactic:
Finset.prod_congr rfl fun i hi ↦ ?_

Premises used: Finset.prod_congr, rfl
-- 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 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_1 : 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_1 i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f_1 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_1 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)
a : α
f : (i : S) → (j : T i) → Ω → 𝓧 i j
refine :
  ∀ (i : S) (hi : i ∈ s),
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i) :
        ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
        ENNReal)
⊢ 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))

Tactic:
refine Finset.prod_congr rfl fun i hi ↦ ?_

Premises used: Finset.prod_congr, rfl
-- 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 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_1 : 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_1 i
h3 : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f_1 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_1 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)
a : α
f : (i : S) → (j : T i) → Ω → 𝓧 i j
i : S
hi : i ∈ s
rw rw₁ :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
      ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
      ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i) :
      ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i) :
      ENNReal)

Tactic:
rw [hu i hi]
-- 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 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)
⊢ ∀ (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))

Tactic:
have h4' a (f : (i : S) → (j : T i) → Ω → 𝓧 i j) :
      ∏ i ∈ s, κ a ((fun i ω j ↦ f i j ω) i ⁻¹' g i) =
      ∏ i ∈ s, κ a ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).restrict ⁻¹' u i) := by
    refine Finset.prod_congr rfl fun i hi ↦ ?_
    rw [hu i hi]
-- 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 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))
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) i ⁻¹' g i) :
        ENNReal)
      (∏ i ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) i ⁻¹' g i) :
        ENNReal)

Tactic:
have h5 := h1 s (fun i hi ↦ ⟨g i, mg i hi, rfl⟩)
-- 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 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)
⊢ ∀ (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
-- 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 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)
⊢ ∀ᵐ (a : α) ∂P,
    ∀ i ∈ s,
      (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) ω

Tactic:
(ae_ball_iff s.countable_toSet).2 fun i hi ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ae_ball_iff, Finset.countable_toSet
-- 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 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)
⊢ Countable.{u_5 + 1} (↑(I i) : Type u_5)

Tactic:
have := (hI i hi).to_subtype