awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : AEMeasurable (_m := mΩ) Y ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
h1 : IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω) (AEMeasurable.mk Y hY) κ P
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ X i ω) (AEMeasurable.mk Y hY) κ P
have h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, AEMeasurable.mk (X i) sorry =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] X i
Tactic: apply process_congr_left (X := fun i ↦ (hX i).mk (X i))
-- 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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : AEMeasurable (_m := mΩ) Y ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω) (AEMeasurable.mk Y hY) κ P
have h1 : ∀ (I : Finset S),
  IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ (fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i ω)
    (AEMeasurable.mk Y hY) κ P
Tactic: refine IndepFun.process_indepFun (fun i ↦ (hX i).measurable_mk) hY.measurable_mk
      fun I ↦ process_congr_left (X := fun (i : I) ↦ X i) ?_ (fun i ↦ ?_)
-- 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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (_m := mΩ) (X i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
hY : AEMeasurable (_m := mΩ) Y ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) Y κ P
inst_2 : IsZeroOrMarkovKernel κ
h1 :
  ∀ (I : Finset S),
    IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (fun (ω : Ω) (i : ↥I) ↦ (fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i ω)
      (AEMeasurable.mk Y hY) κ P
⊢ IndepFun (β := (i : S) → 𝓧 i) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) ⋯ ω) (AEMeasurable.mk Y hY) κ P
have h1₁ : ∀ (I : Finset S) (i : ↥I),
  ∀ᵐ (a : α) ∂P,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := 𝓧 (↑i : S))
      ((fun (i : ↥I) ↦ (X (↑i : S) : Ω → 𝓧 (↑i : S))) i) (AEMeasurable.mk (X (↑i : S)) sorry)
Tactic: refine IndepFun.process_indepFun (fun i ↦ (hX i).measurable_mk) hY.measurable_mk
      fun I ↦ process_congr_left (X := fun (i : I) ↦ X i) ?_ (fun i ↦ ?_)
-- 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 : 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 κ
⊢ IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ X i ω) (fun (ω : Ω) (j : T) ↦ Y j ω) κ P
have refine : ∀ (I : Finset S),
  IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (fun (ω : Ω) (j : T) ↦ Y j ω) κ P
Tactic: refine IndepFun.process_indepFun hX (measurable_pi_lambda _ hY) fun I ↦ ?_
-- 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 : 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
have refine : IndepFun (β := (i : S) → 𝓧 i) (γ := (j : T) → 𝓨 j) (fun (ω : Ω) (i : S) ↦ AEMeasurable.mk (X i) sorry ω)
  (fun (ω : Ω) (j : T) ↦ AEMeasurable.mk (Y j) sorry ω) κ 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)
-- 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 : 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
have refine : ∀ (I : Finset S) (J : Finset T),
  IndepFun (β := (i : ↥I) → 𝓧 (↑i : S)) (γ := (j : ↥J) → 𝓨 (↑j : T))
    (fun (ω : Ω) (i : ↥I) ↦ AEMeasurable.mk (X (↑i : S)) sorry ω) (fun (ω : Ω) (j : ↥J) ↦ AEMeasurable.mk (Y (↑j : T)) sorry ω)
    κ P
Tactic: refine process_indepFun_process
    (fun i ↦ (hX i).measurable_mk) (fun j ↦ (hY j).measurable_mk) fun I J ↦ ?_
-- 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 Ω
hf : ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) ((fun (x : S) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) 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)
have 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)
Tactic: choose! g mg hg using hf
Cleared hypotheses: hf
-- 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
⊢ ∀ᵐ (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)
have h3 : 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
-- 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)
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))
have 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)
Tactic: refine Finset.prod_congr rfl fun i hi ↦ ?_
-- 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)
a : α
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)
have rw : Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i) : ENNReal)
Tactic: rw [hg i hi]
-- 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)
⊢ ∀ᵐ (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)
have 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))
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]
-- 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))
⊢ ∀ᵐ (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)
have 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)
Tactic: simp_rw [h3, h3']
-- 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))
⊢ ∀ᵐ (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)
have 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)
Tactic: choose! I u hI hu using fun i hi ↦ (mg i hi).eq_preimage_restrict_countable
-- 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_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
⊢ 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)
have 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)
Tactic: rw [hu i hi]
-- 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
⊢ ∀ᵐ (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)
have 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)
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
-- 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_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))
have 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)
Tactic: refine Finset.prod_congr rfl fun i hi ↦ ?_