awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
h2 :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
⊢ Measurable (α := (γ × β') × β) (β := γ × β' × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
h2 :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
⊢ Measurable (α := γ × β' × β) (β := (γ × β') × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
h2 :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
⊢ Eq (α := Measure (γ × β' × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β)))
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β))))

Tactic:
have h2_symm : (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ μ.map k =
      (((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k).map e.symm := by
    rw [h2, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
h2 :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
h2_symm :
  Eq (α := Measure (γ × β' × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β)))
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β))))
⊢ Eq (α := Measure (γ × β' × β)) (Measure.map (fun (ω : Ω) ↦ (k ω, g ω, f ω)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))) ↔
    Eq (α := Measure ((γ × β') × β))
      (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
        (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
      (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
        (Measure.bind (mα := mγ) (Measure.map k μ)
          (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))

Tactic:
exact ⟨fun h ↦ by rw [h], fun h ↦ by rw [h1_symm, h1, h2_symm, h2, h]⟩
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_2 : Subsingleton ι
⊢ iCondIndepFun m' hm' (β := β) f μ

Tactic:
Kernel.iIndepFun.of_subsingleton

Premises used: ProbabilityTheory.Kernel.iIndepFun.of_subsingleton, ProbabilityTheory.iCondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_6
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iCondIndepFun m' hm' (β := β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
⊢ CondIndepFun m' hm' (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) μ

Tactic:
Kernel.iIndepFun.indepFun_finset S T hST hf_Indep hf_meas

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_6
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iCondIndepFun m' hm' (β := β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ CondIndepFun m' hm' (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) μ

Tactic:
Kernel.iIndepFun.indepFun_prodMk hf_Indep hf_meas i j k hik hjk

Premises used: ProbabilityTheory.CondIndepFun, ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i_1 j_1 k l : ι
hik : i_1 ≠ k
hil : i_1 ≠ l
hjk : j_1 ≠ k
hjl : j_1 ≠ l
g : (i j : ι) → (v : (x : ↥{i, j}) → β (↑x : ι)) → β i × β j :=
  fun (i j : ι) (v : (x : ↥{i, j}) → β (↑x : ι)) ↦
    (v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) i ⋯),
      v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) j ⋯))
i j : ι
⊢ Measurable (g i j)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
g : (i j : ι) → (v : (x : ↥{i, j}) → β (↑x : ι)) → β i × β j :=
  fun (i j : ι) (v : (x : ↥{i, j}) → β (↑x : ι)) ↦
    (v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) i ⋯),
      v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) j ⋯))
⊢ ∀ (i j : ι), Measurable (g i j)

Tactic:
have hg (i j : ι) : Measurable (g i j) := by fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
g : (i j : ι) → (v : (x : ↥{i, j}) → β (↑x : ι)) → β i × β j :=
  fun (i j : ι) (v : (x : ↥{i, j}) → β (↑x : ι)) ↦
    (v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) i ⋯),
      v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) j ⋯))
hg : ∀ (i j : ι), Measurable (g i j)
⊢ Disjoint (α := Finset ι) {i, j} {k, l}

Tactic:
aesop
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
g : (i j : ι) → (v : (x : ↥{i, j}) → β (↑x : ι)) → β i × β j :=
  fun (i j : ι) (v : (x : ↥{i, j}) → β (↑x : ι)) ↦
    (v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) i ⋯),
      v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) j ⋯))
hg : ∀ (i j : ι), Measurable (g i j)
⊢ CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) μ

Tactic:
exact (h_indep.indepFun_finset {i, j} {k, l} (by aesop) hf).comp (hg i j) (hg k l)

Premises used: Insert.insert, ProbabilityTheory.Kernel.IndepFun.comp, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, Singleton.singleton
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
let let₁ let₂ :
  CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) μ
let₃ :
  let g : (i j : ι) → (v : (x : ↥{i, j}) → β (↑x : ι)) → β i × β j := fun (i j : ι) (v : (x : ↥{i, j}) → β (↑x : ι)) ↦
    (v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) i ⋯),
      v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) j ⋯));
  ∀ (hg : ∀ (i j : ι), Measurable (g i j)),
    CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
      (fun (a : Ω) ↦ (f k a, f l a)) μ
⊢ CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) μ

Tactic:
classical
  let g (i j : ι) (v : Π x : ({i, j} : Finset ι), β x) : β i × β j :=
    ⟨v ⟨i, mem_insert_self _ _⟩, v ⟨j, mem_insert_of_mem <| mem_singleton_self _⟩⟩
  have hg (i j : ι) : Measurable (g i j) := by fun_prop
  exact (h_indep.indepFun_finset {i, j} {k, l} (by aesop) hf).comp (hg i j) (hg k l)
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : MeasurableSpace β
inst_2 : Mul β
inst_3 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iCondIndepFun m' hm' (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ CondIndepFun m' hm' (f i * f j) (f k) μ

Tactic:
Kernel.iIndepFun.indepFun_mul_left hf_indep hf_meas i j k hik hjk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : MeasurableSpace β
inst_2 : Mul β
inst_3 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iCondIndepFun m' hm' (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ CondIndepFun m' hm' (f i) (f j * f k) μ

Tactic:
Kernel.iIndepFun.indepFun_mul_right hf_indep hf_meas i j k hij hik

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : MeasurableSpace β
inst_2 : Mul β
inst_3 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iCondIndepFun m' hm' (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ CondIndepFun m' hm' (f i * f j) (f k * f l) μ

Tactic:
Kernel.iIndepFun.indepFun_mul_mul hf_indep hf_meas i j k l hik hil hjk hjl

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : MeasurableSpace β
inst_2 : Div β
inst_3 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iCondIndepFun m' hm' (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ CondIndepFun m' hm' (f i / f j) (f k) μ

Tactic:
Kernel.iIndepFun.indepFun_div_left hf_indep hf_meas i j k hik hjk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : MeasurableSpace β
inst_2 : Div β
inst_3 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iCondIndepFun m' hm' (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ CondIndepFun m' hm' (f i / f j) (f k / f l) μ

Tactic:
Kernel.iIndepFun.indepFun_div_div hf_indep hf_meas i j k l hik hil hjk hjl

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : MeasurableSpace β
inst_2 : CommMonoid β
inst_3 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iCondIndepFun m' hm' (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
⊢ CondIndepFun m' hm' (β := β) (∏ j ∈ s, f j) (f i) μ

Tactic:
Kernel.iIndepFun.indepFun_finsetProd_of_notMem hf_Indep hf_meas hi

Premises used: ProbabilityTheory.CondIndepFun, ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : MeasurableSpace β
inst_2 : CommMonoid β
inst_3 : MeasurableMul₂ β
f : ℕ → Ω → β
hf_Indep : iCondIndepFun m' hm' (β := fun (x : ℕ) ↦ β) f μ
hf_meas : ∀ (i : ℕ), Measurable (f i)
n : ℕ
⊢ CondIndepFun m' hm' (β := β) (∏ j ∈ Finset.range n, f j) (f n) μ

Tactic:
Kernel.iIndepFun.indepFun_prod_range_succ hf_Indep hf_meas n

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_3
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : Zero β
inst_3 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iCondIndepSet m' hm' s μ
⊢ iCondIndepFun m' hm' (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) μ

Tactic:
Kernel.iIndepSet.iIndepFun_indicator hs

Premises used: ProbabilityTheory.iCondIndepFun, ProbabilityTheory.Kernel.iIndepSet.iIndepFun_indicator
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : iIndepFun (β := 𝓧) X P
⊢ IsProbabilityMeasure P

Tactic:
have := h.isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : iIndepFun (β := 𝓧) X P
this : IsProbabilityMeasure P
⊢ ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)

Tactic:
have _ i := isProbabilityMeasure_map (mX.eval i)
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : iIndepFun (β := 𝓧) X P
this : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)

Tactic:
eq_infinitePi _ fun s t ht ↦ ?_

Premises used: MeasureTheory.Measure.eq_infinitePi
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : iIndepFun (β := 𝓧) X P
this : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
refine :
  ∀ (s : Finset ι) (t : (i : ι) → Set (𝓧 i)) (ht : ∀ (i : ι), MeasurableSet (t i)),
    Eq (α := ENNReal)
      ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) :
        ENNReal)
      (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)

Tactic:
refine eq_infinitePi _ fun s t ht ↦ ?_

Premises used: MeasureTheory.Measure.eq_infinitePi