awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy_1 :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt_1 : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg_1 : ∀ (i : ι), MeasurableSet (g i)
a : α
hy :
  ∀ i ∉ s,
    Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
      (0 : ENNReal)
h : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a)
hYt :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
hg :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
pos :
  ∀ (hi : i ∈ s),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal) =
      if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1
neg :
  ∀ (hi : i ∉ s),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal) =
      if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal) =
    if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy_1 :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt_1 : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg_1 : ∀ (i : ι), MeasurableSet (g i)
a : α
hy :
  ∀ i ∉ s,
    Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
      (0 : ENNReal)
h : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a)
hYt :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
hg :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∈ s
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal) =
    if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1

Tactic:
simp only [hi, ↓reduceIte, g, cond_apply (hY i (ht i))]

Premises used: ProbabilityTheory.cond_apply, reduceIte
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy_1 :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt_1 : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg_1 : ∀ (i : ι), MeasurableSet (g i)
a : α
hy :
  ∀ i ∉ s,
    Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
      (0 : ENNReal)
h : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a)
hYt :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
hg :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∉ s
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal) =
    if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1

Tactic:
simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top _ _)]

Premises used: MeasureTheory.measure_ne_top, reduceIte, ENNReal.inv_mul_cancel
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy_1 :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt_1 : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg_1 : ∀ (i : ι), MeasurableSet (g i)
a : α
hy :
  ∀ i ∉ s,
    Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
      (0 : ENNReal)
h : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a)
hYt :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
hg :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)
⊢ Eq (α := ENNReal) (∏ i : ι, if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1)
    (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i])

Tactic:
simp
-- 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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
s : Set ((i : S) → 𝓧 i)
hs : MeasurableSet s
t : Set 𝓨
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)

Tactic:
have : ∀ᵐ a ∂P, κ a (((fun ω i ↦ X i ω) ⁻¹' s) ∩ (Y ⁻¹' t)) =
      κ a ((fun ω i ↦ X i ω) ⁻¹' s) * κ a (Y ⁻¹' t) :=
    h1 ((fun ω i ↦ X i ω) ⁻¹' s) (Y ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, 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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
s : Set ((i : S) → 𝓧 i)
hs : MeasurableSet s
t : Set 𝓨
ht : MeasurableSet t
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
⊢ ∃ (I : Set S) (u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))), I.Countable ∧ s = I.restrict (π := 𝓧) ⁻¹' u

Tactic:
hs.eq_preimage_restrict_countable

Premises used: MeasureTheory.MeasurableSet.eq_preimage_restrict_countable
-- 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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
s : Set ((i : S) → 𝓧 i)
hs : MeasurableSet s
t : Set 𝓨
ht : MeasurableSet t
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
obtain :
  ∀ (I : Set S) (u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))) (hI : I.Countable)
    (hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u))
    (this :
      ∀ᵐ (a : α) ∂P,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u ∩ Y ⁻¹' t) =
          HMul.hMul (α := ENNReal) (β := ENNReal)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
                ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u) :
              ENNReal)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)),
    ∀ᵐ (a : α) ∂P,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (ω : Ω) (i : S) ↦ X' i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u ∩ Y ⁻¹' t) =
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              ((fun (ω : Ω) (i : S) ↦ X' i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u) :
            ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X' i ω) ⁻¹' s ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) ((fun (ω : Ω) (i : S) ↦ X' i ω) ⁻¹' s) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)

Tactic:
obtain ⟨I, u, hI, rfl⟩ : ∃ (I : Set S) (u : Set (Π i : I, 𝓧 i)),
      I.Countable ∧ s = I.restrict ⁻¹' u := hs.eq_preimage_restrict_countable

Premises used: MeasureTheory.MeasurableSet.eq_preimage_restrict_countable, rfl, Set
-- 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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
⊢ ∀ (f : (i : S) → Ω → 𝓧 i),
    Eq.{u_3 + 1} (α := Set Ω) ((fun (ω : Ω) (i : S) ↦ f i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u)
      ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ f (↑i : S) ω) ⁻¹' u)

Tactic:
have aux (f : (i : S) → Ω → 𝓧 i) : (fun ω i ↦ f i ω) ⁻¹' I.restrict ⁻¹' u =
      (fun ω (i : I) ↦ f i ω) ⁻¹' u := 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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux :
  ∀ (f : (i : S) → Ω → 𝓧 i),
    Eq.{u_3 + 1} (α := Set Ω) ((fun (ω : Ω) (i : S) ↦ f i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u)
      ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ f (↑i : S) ω) ⁻¹' u)
simp_rw :
  ∀
    (this :
      ∀ᵐ (a : α) ∂P,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
          HMul.hMul (α := ENNReal) (β := ENNReal)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
                ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
              ENNReal)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal))
    (aux : ∀ (f : (i : S) → Ω → 𝓧 i), True),
    ∀ᵐ (a : α) ∂P,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω) ⁻¹' u) :
            ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
⊢ ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : S) ↦ X' i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : S) ↦ X' i ω) ⁻¹' I.restrict (π := 𝓧) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)

Tactic:
simp_rw [aux] at *
-- 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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
⊢ Countable.{u_1 + 1} (↑I : Type u_1)

Tactic:
have _ : Countable I := hI.to_subtype
-- 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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
h_1 : Countable.{u_1 + 1} (↑I : Type u_1)
a : α
h :
  ∀
    (ha :
      ∀ (i : (↑I : Type u_1)),
        ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), Eq (α := 𝓧 (↑i : S)) (X (↑i : S) ω) (X' (↑i : S) ω)),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β :=
      (i : (↑I : Type u_1)) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω)
      fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω
⊢ (∀ (i : (↑I : Type u_1)),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := 𝓧 (↑i : S)) (X (↑i : S))
        (X' (↑i : S))) →
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β :=
      (i : (↑I : Type u_1)) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω)
      fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω

Tactic:
(ha : ∀ (i : I), ∀ᵐ ω ∂κ a, X i ω = X' i ω)
-- 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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : (↑I : Type u_1)) → 𝓧 (↑i : S))
hI : I.Countable
hs : MeasurableSet (I.restrict (π := 𝓧) ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u ∩ Y ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω) ⁻¹' u) :
          ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y ⁻¹' t) : ENNReal)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
h_1 : Countable.{u_1 + 1} (↑I : Type u_1)
h :
  ∀ (a : α)
    (ha :
      ∀ (i : (↑I : Type u_1)),
        ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), Eq (α := 𝓧 (↑i : S)) (X (↑i : S) ω) (X' (↑i : S) ω)),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β :=
      (i : (↑I : Type u_1)) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω)
      fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω
⊢ ∀ᵐ (a : α) ∂P,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β :=
      (i : (↑I : Type u_1)) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X (↑i : S) ω)
      fun (ω : Ω) (i : (↑I : Type u_1)) ↦ X' (↑i : S) ω

Tactic:
filter_upwards [ae_all_iff.2 fun (i : I) ↦ h2 i] with
      a (ha : ∀ (i : I), ∀ᵐ ω ∂κ a, X i ω = X' i ω)

Premises used: Iff.mpr, MeasureTheory.ae_all_iff, Subtype.val