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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), Measurable (X i)
hY : ∀ (j : T), Measurable (Y j)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
refine :
  ∀ (I : Finset S),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : T) ↦ Y j ω) κ P
⊢ IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ X i ω) (fun (ω : Ω) (j : T) ↦ Y j ω) κ P

Tactic:
refine IndepFun.process_indepFun hX (measurable_pi_lambda _ hY) fun I ↦ ?_

Premises used: measurable_pi_lambda, ProbabilityTheory.Kernel.IndepFun.process_indepFun
-- 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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), Measurable (X i)
hY : ∀ (j : T), Measurable (Y j)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
I : Finset S
⊢ IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (fun (ω : Ω) (j : T) ↦ Y j ω) κ P

Tactic:
IndepFun.indepFun_process (measurable_pi_lambda _ fun _ ↦ hX _) hY fun J ↦ h I J

Premises used: measurable_pi_lambda, ProbabilityTheory.Kernel.IndepFun.indepFun_process, Subtype.val
-- 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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), Measurable (X i)
hY : ∀ (j : T), Measurable (Y j)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
I : Finset S
⊢ IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (fun (ω : Ω) (j : T) ↦ Y j ω) κ P

Tactic:
exact IndepFun.indepFun_process (measurable_pi_lambda _ fun _ ↦ hX _) hY fun J ↦ h I J

Premises used: measurable_pi_lambda, ProbabilityTheory.Kernel.IndepFun.indepFun_process
-- 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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : ∀ (j : T), AEMeasurable (_m := mΩ) (Y j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ X i ω) (fun (ω : Ω) (j : T) ↦ Y j ω) κ P

Tactic:
process_congr ?_ (fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk.symm)
    (fun j ↦ Measure.ae_ae_of_ae_comp (hY j).ae_eq_mk.symm)

Premises used: ProbabilityTheory.Kernel.IndepFun.process_congr, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : ∀ (j : T), AEMeasurable (_m := mΩ) (Y j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
refine :
  IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω)
    (fun (ω : Ω) (j : T) ↦ AEMeasurable.mk (Y j) ⋯ ω) κ P
⊢ IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ X i ω) (fun (ω : Ω) (j : T) ↦ Y j ω) κ P

Tactic:
refine process_congr ?_ (fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk.symm)
    (fun j ↦ Measure.ae_ae_of_ae_comp (hY j).ae_eq_mk.symm)

Premises used: ProbabilityTheory.Kernel.IndepFun.process_congr, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : ∀ (j : T), AEMeasurable (_m := mΩ) (Y j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω)
    (fun (ω : Ω) (j : T) ↦ AEMeasurable.mk (Y j) ⋯ ω) κ P

Tactic:
process_indepFun_process
    (fun i ↦ (hX i).measurable_mk) (fun j ↦ (hY j).measurable_mk) fun I J ↦ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.process_indepFun_process, AEMeasurable.measurable_mk
-- 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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : ∀ (j : T), AEMeasurable (_m := mΩ) (Y j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
refine :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T))
      (fun (ω : Ω) (i : ↥I) ↦ AEMeasurable.mk (X (↑i : S)) ⋯ ω)
      (fun (ω : Ω) (j : ↥J) ↦ AEMeasurable.mk (Y (↑j : T)) ⋯ ω) κ P
⊢ IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω)
    (fun (ω : Ω) (j : T) ↦ AEMeasurable.mk (Y j) ⋯ ω) κ P

Tactic:
refine process_indepFun_process
    (fun i ↦ (hX i).measurable_mk) (fun j ↦ (hY j).measurable_mk) fun I J ↦ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.process_indepFun_process, AEMeasurable.measurable_mk
-- 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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : ∀ (j : T), AEMeasurable (_m := mΩ) (Y j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
I : Finset S
J : Finset T
⊢ IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T))
    (fun (ω : Ω) (i : ↥I) ↦ AEMeasurable.mk (X (↑i : S)) ⋯ ω) (fun (ω : Ω) (j : ↥J) ↦ AEMeasurable.mk (Y (↑j : T)) ⋯ ω)
    κ P

Tactic:
process_congr (h I J) (fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk)
    (fun j ↦ Measure.ae_ae_of_ae_comp (hY j).ae_eq_mk)

Premises used: ProbabilityTheory.Kernel.IndepFun.process_congr, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Subtype.val
-- 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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : ∀ (j : T), AEMeasurable (_m := mΩ) (Y j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : Finset T),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) κ P
inst_2 : IsZeroOrMarkovKernel κ
I : Finset S
J : Finset T
⊢ IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T))
    (fun (ω : Ω) (i : ↥I) ↦ AEMeasurable.mk (X (↑i : S)) ⋯ ω) (fun (ω : Ω) (j : ↥J) ↦ AEMeasurable.mk (Y (↑j : T)) ⋯ ω)
    κ P

Tactic:
exact process_congr (h I J) (fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk)
    (fun j ↦ Measure.ae_ae_of_ae_comp (hY j).ae_eq_mk)

Premises used: ProbabilityTheory.Kernel.IndepFun.process_congr, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Subtype.val
-- 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 Ω
hf : ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) ((fun (x : S) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)
choose! :
  ∀ (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),
    ∀ᵐ (a : α) ∂P,
      Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ s, f i) : ENNReal)
        (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ s, f i) : ENNReal)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)

Tactic:
choose! g mg hg using hf
-- 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
⊢ Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ i ∈ s, (fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i)

Tactic:
have h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i := (biInf_congr hg).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 : 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)
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))

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 : 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)
a : α
refine :
  ∀ (i : S) (hi : i ∈ s),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i) :
        ENNReal)
⊢ 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))

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 : 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)
a : α
i : S
hi : i ∈ s
rw rw₁ :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (i : S) (ω : Ω) (j : T i) ↦ X' i j ω) i ⁻¹' g i) :
      ENNReal)

Tactic:
rw [hg 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)
⊢ ∀ (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))

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

Tactic:
simp_rw [h3, h3']
-- 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))
choose! :
  ∀ (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),
    ∀ᵐ (a : α) ∂P,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ i ∈ s, (fun (ω : Ω) (j : T i) ↦ X' i j ω) ⁻¹' g i) :
          ENNReal)
        (∏ x ∈ s,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              ((fun (ω : Ω) (j : T x) ↦ X' x j ω) ⁻¹' g x) :
          ENNReal)
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ s, (fun (ω : Ω) (j : T i) ↦ X' i j ω) ⁻¹' g i) :
        ENNReal)
      (∏ x ∈ s,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T x) ↦ X' x j ω) ⁻¹' g x) :
        ENNReal)

Tactic:
choose! I u hI hu using fun i hi ↦ (mg i hi).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 α
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
f : (i : S) → (j : T i) → Ω → 𝓧 i j
i : S
hi : i ∈ s
rw rw₁ :
  Eq.{u_3 + 1} (α := Set Ω) ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
    ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
⊢ Eq.{u_3 + 1} (α := Set Ω) ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' (I i).restrict (π := 𝓧 i) ⁻¹' u i)
    ((fun (i : S) (ω : Ω) (j : T i) ↦ f i j ω) i ⁻¹' g i)

Tactic:
rw [hu i hi]