awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ iIndepFun (β := β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
exact iIndepFun.congr' hf_indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr', MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ

Tactic:
have h : IndepFun (fun a ↦ ((hf_meas i).mk (f i) a, (hf_meas j).mk (f j) a))
      (fun a ↦ ((hf_meas k).mk (f k) a, (hf_meas l).mk (f l) a)) κ μ := by
    refine iIndepFun.indepFun_prodMk_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ _ hik hil
      hjk hjl
    exact iIndepFun.congr' hf_indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
⊢ IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) κ μ

Tactic:
IndepFun.congr' h ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
refine_1 :
  ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β i × β j) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) fun (a : Ω) ↦ (f i a, f j a)
refine_2 :
  ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β k × β l) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) fun (a : Ω) ↦ (f k a, f l a)
⊢ IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) κ μ

Tactic:
refine IndepFun.congr' h ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
h₁ :
  ∀ (a : α) (hi : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f i ω = AEMeasurable.mk (f i) ⋯ ω)
    (hj : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f j ω = AEMeasurable.mk (f j) ⋯ ω),
    Filter.EventuallyEq.{u_2, u_8} (β := β i × β j) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) fun (a : Ω) ↦ (f i a, f j a)
⊢ ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β i × β j) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) fun (a : Ω) ↦ (f i a, f j a)

Tactic:
filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk,
      Measure.ae_ae_of_ae_comp (hf_meas j).ae_eq_mk] with a hi hj

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hi : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f i ω = AEMeasurable.mk (f i) ⋯ ω
hj : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f j ω = AEMeasurable.mk (f j) ⋯ ω
h₁ :
  ∀ (ω : Ω) (hωi : f i ω = AEMeasurable.mk (f i) ⋯ ω) (hωj : f j ω = AEMeasurable.mk (f j) ⋯ ω),
    (AEMeasurable.mk (f i) ⋯ ω, AEMeasurable.mk (f j) ⋯ ω) = (f i ω, f j ω)
⊢ Filter.EventuallyEq.{u_2, u_8} (β := β i × β j) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) fun (a : Ω) ↦ (f i a, f j a)

Tactic:
filter_upwards [hi, hj] with ω hωi hωj
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hi : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f i ω = AEMeasurable.mk (f i) ⋯ ω
hj : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f j ω = AEMeasurable.mk (f j) ⋯ ω
ω : Ω
hωi : f i ω = AEMeasurable.mk (f i) ⋯ ω
hωj : f j ω = AEMeasurable.mk (f j) ⋯ ω
h₁ : (f i ω, AEMeasurable.mk (f j) ⋯ ω) = (f i ω, f j ω)
h₂ h₃ : (f i ω, f j ω) = (f i ω, f j ω)
⊢ (AEMeasurable.mk (f i) ⋯ ω, AEMeasurable.mk (f j) ⋯ ω) = (f i ω, f j ω)

Tactic:
rw [← hωi, ← hωj]
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
h₁ :
  ∀ (a : α) (hk : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f k ω = AEMeasurable.mk (f k) ⋯ ω)
    (hl : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f l ω = AEMeasurable.mk (f l) ⋯ ω),
    Filter.EventuallyEq.{u_2, u_8} (β := β k × β l) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) fun (a : Ω) ↦ (f k a, f l a)
⊢ ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β k × β l) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) fun (a : Ω) ↦ (f k a, f l a)

Tactic:
filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas k).ae_eq_mk,
      Measure.ae_ae_of_ae_comp (hf_meas l).ae_eq_mk] with a hk hl

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f l ω = AEMeasurable.mk (f l) ⋯ ω
h₁ :
  ∀ (ω : Ω) (hωk : f k ω = AEMeasurable.mk (f k) ⋯ ω) (hωl : f l ω = AEMeasurable.mk (f l) ⋯ ω),
    (AEMeasurable.mk (f k) ⋯ ω, AEMeasurable.mk (f l) ⋯ ω) = (f k ω, f l ω)
⊢ Filter.EventuallyEq.{u_2, u_8} (β := β k × β l) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) fun (a : Ω) ↦ (f k a, f l a)

Tactic:
filter_upwards [hk, hl] with ω hωk hωl
-- 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f l ω = AEMeasurable.mk (f l) ⋯ ω
ω : Ω
hωk : f k ω = AEMeasurable.mk (f k) ⋯ ω
hωl : f l ω = AEMeasurable.mk (f l) ⋯ ω
h₁ : (f k ω, AEMeasurable.mk (f l) ⋯ ω) = (f k ω, f l ω)
h₂ h₃ : (f k ω, f l ω) = (f k ω, f l ω)
⊢ (AEMeasurable.mk (f k) ⋯ ω, AEMeasurable.mk (f l) ⋯ ω) = (f k ω, f l ω)

Tactic:
rw [← hωk, ← hωl]
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ

Tactic:
have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i * f j) (f k) κ μ

Tactic:
simpa using this.comp (measurable_fst.mul measurable_snd) measurable_id

Premises used: Measurable.mul, measurable_id, ProbabilityTheory.Kernel.IndepFun.comp, measurable_snd, measurable_fst
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ

Tactic:
have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk₀ hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i * f j) (f k) κ μ

Tactic:
simpa using this.comp (measurable_fst.mul measurable_snd) measurable_id

Premises used: Measurable.mul, measurable_id, ProbabilityTheory.Kernel.IndepFun.comp, measurable_snd, measurable_fst
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ IndepFun (f i) (f j * f k) κ μ

Tactic:
(hf_indep.indepFun_mul_left hf_meas _ _ _ hij.symm hik.symm).symm

Premises used: Ne.symm, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left, ProbabilityTheory.Kernel.IndepFun.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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ IndepFun (f i) (f j * f k) κ μ

Tactic:
(hf_indep.indepFun_mul_left₀ hf_meas _ _ _ hij.symm hik.symm).symm

Premises used: Ne.symm, ProbabilityTheory.Kernel.IndepFun.symm, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left₀
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := 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
⊢ IndepFun (f i * f j) (f k * f l) κ μ

Tactic:
(hf_indep.indepFun_prodMk_prodMk hf_meas i j k l hik hil hjk hjl).comp
    measurable_mul measurable_mul

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk, MeasurableMul₂.measurable_mul, ProbabilityTheory.Kernel.IndepFun.comp
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun (f i * f j) (f k * f l) κ μ

Tactic:
(hf_indep.indepFun_prodMk_prodMk₀ hf_meas i j k l hik hil hjk hjl).comp
    measurable_mul measurable_mul

Premises used: MeasurableMul₂.measurable_mul, ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk₀, ProbabilityTheory.Kernel.IndepFun.comp
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ

Tactic:
have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i / f j) (f k) κ μ

Tactic:
simpa using this.comp (measurable_fst.div measurable_snd) measurable_id

Premises used: measurable_id, Measurable.div, ProbabilityTheory.Kernel.IndepFun.comp, measurable_snd, measurable_fst
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ

Tactic:
have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk₀ hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i / f j) (f k) κ μ

Tactic:
simpa using this.comp (measurable_fst.div measurable_snd) measurable_id

Premises used: measurable_id, Measurable.div, ProbabilityTheory.Kernel.IndepFun.comp, measurable_snd, measurable_fst
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ IndepFun (f i) (f j / f k) κ μ

Tactic:
(hf_indep.indepFun_div_left hf_meas _ _ _ hij.symm hik.symm).symm

Premises used: Ne.symm, ProbabilityTheory.Kernel.IndepFun.symm, ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ IndepFun (f i) (f j / f k) κ μ

Tactic:
(hf_indep.indepFun_div_left₀ hf_meas _ _ _ hij.symm hik.symm).symm

Premises used: Ne.symm, ProbabilityTheory.Kernel.IndepFun.symm, ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left₀
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := 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
⊢ IndepFun (f i / f j) (f k / f l) κ μ

Tactic:
(hf_indep.indepFun_prodMk_prodMk hf_meas i j k l hik hil hjk hjl).comp
    measurable_div measurable_div

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk, MeasurableDiv₂.measurable_div, ProbabilityTheory.Kernel.IndepFun.comp
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun (f i / f j) (f k / f l) κ μ

Tactic:
(hf_indep.indepFun_prodMk_prodMk₀ hf_meas i j k l hik hil hjk hjl).comp
    measurable_div measurable_div

Premises used: MeasurableDiv₂.measurable_div, ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk₀, ProbabilityTheory.Kernel.IndepFun.comp
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
⊢ f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a

Tactic:
have h_right : f i =
    (fun p : ({i} : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘
    fun a (j : ({i} : Finset ι)) => f j a := rfl
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
⊢ Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)

Tactic:
have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _