awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  Eq (α := ENNReal) ((μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)
    ((μ ⊗ₘ (κ.map f ×ₖ κ.map g) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)
⊢ ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ

Tactic:
rw [Measure.compProd_apply_prod hu (hs.prod ht),
      Measure.compProd_apply_prod hu (hs.prod ht)] at h

Premises used: MeasurableSet.prod, MeasureTheory.Measure.compProd_apply_prod
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
⊢ ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ

Tactic:
h
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
h₁ :
  ∀ (ω : α),
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
      ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) :
            (a : Set (β × γ)) → ENNReal)
          (s ×ˢ t) :
        ENNReal)
h₂ :
  ∀ (ω : α),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t)
⊢ ∫⁻ (x : α) in u, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ =
    ∫⁻ (x : α) in u,
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) ∂μ

Tactic:
convert! h with ω ω
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
⊢ Measurable (β := β × γ) fun (ω : Ω) ↦ (f ω, g ω)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
h₁ :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) ((fun (ω : Ω) ↦ (f ω, g ω)) ⁻¹' s ×ˢ t) :
      ENNReal)
h₂ h₃ :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) :
      ENNReal)

Tactic:
rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]

Premises used: ProbabilityTheory.Kernel.map_apply', MeasurableSet.prod, Set.mk_preimage_prod
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
⊢ Measurable f

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
⊢ Measurable g

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
h₁ :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      (((((κ.map f : Kernel α β) : (a : α) → Measure β) ω : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      (((((κ.map g : Kernel α γ) : (a : α) → Measure γ) ω : Measure γ) : (a : Set γ) → ENNReal) t : ENNReal)
h₂ :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      (((((κ.map g : Kernel α γ) : (a : α) → Measure γ) ω : Measure γ) : (a : Set γ) → ENNReal) t : ENNReal)
h₃ h₄ :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t)

Tactic:
rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ ht]

Premises used: ProbabilityTheory.Kernel.map_apply', ProbabilityTheory.Kernel.prod_apply_prod
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
inl :
  ∀ (hf_Indep : iIndepFun (β := β) f κ 0),
    IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ 0
inr :
  ∀ (hμ : μ ≠ 0),
    IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ

Tactic:
rcases eq_or_ne μ 0 with rfl | hμ

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_meas : ∀ (i : ι), Measurable (f i)
hf_Indep : iIndepFun (β := β) f κ 0
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
⊢ ∃ (η : Kernel α Ω),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω) ∧
      IsMarkovKernel η

Tactic:
exists_ae_eq_isMarkovKernel hf_Indep.ae_isProbabilityMeasure hμ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
inr :
  ∀ (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η),
    IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ

Tactic:
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hf_Indep.ae_isProbabilityMeasure hμ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure, ProbabilityTheory.Kernel
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
inr :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ

Tactic:
apply IndepFun.congr (Filter.EventuallyEq.symm η_eq)

Premises used: ProbabilityTheory.Kernel.IndepFun.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
⊢ IsPiSystem πS

Tactic:
IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _

Premises used: Set.Mem, setOf, IsPiSystem.comap, isPiSystem_pi
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
⊢ IsPiSystem πS

Tactic:
exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _

Premises used: IsPiSystem.comap, isPiSystem_pi
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
⊢ IsPiSystem πS

Tactic:
have hπS_pi : IsPiSystem πS := by exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
rw :
  generateFrom
      (image (α := Set ((i : ↥S) → β (↑i : ι))) (preimage fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
        (Set.pi (α := fun (a : ↥S) ↦ β (↑a : ι)) univ ''
          Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s})) =
    generateFrom πS
⊢ MeasurableSpace.comap (β := (i : ↥S) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥S) ↦ β (↑a : ι))) =
    generateFrom πS

Tactic:
rw [generateFrom_pi.symm, comap_generateFrom]

Premises used: generateFrom_pi, Eq.symm, MeasurableSpace.comap_generateFrom
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ generateFrom
      (image (α := Set ((i : ↥S) → β (↑i : ι))) (preimage fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
        (Set.pi (α := fun (a : ↥S) ↦ β (↑a : ι)) univ ''
          Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s})) =
    generateFrom πS

Tactic:
congr
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ MeasurableSpace.comap (β := (i : ↥S) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥S) ↦ β (↑a : ι))) =
    generateFrom πS

Tactic:
have hπS_gen : (MeasurableSpace.pi.comap fun a (i : S) => f i a) = generateFrom πS := by
    rw [generateFrom_pi.symm, comap_generateFrom]
    congr
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen :
  MeasurableSpace.comap (β := (i : ↥S) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥S) ↦ β (↑a : ι))) =
    generateFrom πS
πTβ : Set (Set ((i : ↥T) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥T) ↦ Set (β (↑i : ι))) univ fun (i : ↥T) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πT : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πTβ, (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' t = s}
⊢ IsPiSystem πT

Tactic:
IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _

Premises used: Set.Mem, setOf, IsPiSystem.comap, isPiSystem_pi