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 : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right :
  f k =
    (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
      fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
    fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)
s : Finset ι := {i, j}
h_left :
  Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
    ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
        (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
      fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
h_meas_left :
  Measurable (β :=
    β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
    fun (p : (l : ↥s) → β (↑l : ι)) ↦
    (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))
rw : k ∉ s
⊢ Disjoint s {k}

Tactic:
rw [Finset.disjoint_singleton_right]

Premises used: Finset.disjoint_singleton_right
-- 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 : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right :
  f k =
    (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
      fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
    fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)
s : Finset ι := {i, j}
h_left :
  Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
    ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
        (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
      fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
h_meas_left :
  Measurable (β :=
    β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
    fun (p : (l : ↥s) → β (↑l : ι)) ↦
    (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))
simp : ¬k = i ∧ ¬k = j
⊢ k ∉ s

Tactic:
simp only [s, Finset.mem_insert, Finset.mem_singleton, not_or]

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or
-- 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 : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right :
  f k =
    (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
      fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
    fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)
s : Finset ι := {i, j}
h_left :
  Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
    ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
        (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
      fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
h_meas_left :
  Measurable (β :=
    β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
    fun (p : (l : ↥s) → β (↑l : ι)) ↦
    (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))
⊢ ¬k = i ∧ ¬k = j

Tactic:
⟨hik.symm, hjk.symm⟩

Premises used: Ne.symm, And.intro
-- 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 : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right :
  f k =
    (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
      fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
    fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)
s : Finset ι := {i, j}
h_left :
  Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
    ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
        (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
      fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
h_meas_left :
  Measurable (β :=
    β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
    fun (p : (l : ↥s) → β (↑l : ι)) ↦
    (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))
⊢ ¬k = i ∧ ¬k = j

Tactic:
exact ⟨hik.symm, hjk.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
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ

Tactic:
iIndepFun.indepFun_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ hik hjk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk, AEMeasurable.measurable_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 : ι
hik : i ≠ k
hjk : j ≠ k
refine : iIndepFun (β := β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ

Tactic:
refine iIndepFun.indepFun_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ hik hjk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk, AEMeasurable.measurable_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 : ι
hik : i ≠ k
hjk : j ≠ k
⊢ iIndepFun (β := β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
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 : ι
hik : i ≠ k
hjk : j ≠ k
⊢ 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 : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ

Tactic:
have h : IndepFun (fun a ↦ ((hf_meas i).mk (f i) a, (hf_meas j).mk (f j) a))
      ((hf_meas k).mk (f k)) κ μ := by
    refine iIndepFun.indepFun_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ hik hjk
    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 : ι
hik : i ≠ k
hjk : j ≠ k
h :
  IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ

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 : ι
hik : i ≠ k
hjk : j ≠ k
h :
  IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ
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 : α) ∂μ, AEMeasurable.mk (f k) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f k
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ

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 : ι
hik : i ≠ k
hjk : j ≠ k
h :
  IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ
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 : ι
hik : i ≠ k
hjk : j ≠ k
h :
  IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ
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 : ι
hik : i ≠ k
hjk : j ≠ k
h :
  IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ
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 : ι
hik : i ≠ k
hjk : j ≠ k
h :
  IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f k) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f k

Tactic:
Measure.ae_ae_of_ae_comp (hf_meas k).ae_eq_mk.symm

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, 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
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h :
  IndepFun (β := β i × β j) (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (AEMeasurable.mk (f k) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f k) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f k

Tactic:
exact Measure.ae_ae_of_ae_comp (hf_meas k).ae_eq_mk.symm

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, 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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (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.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 : ι), 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.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 : ι), 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.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 : ι), 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)
⊢ 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:
exact (hf_indep.indepFun_finset {i, j} {k, l} (by aesop) hf_meas).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.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 : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
let let₁ let₂ :
  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)) κ μ
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)),
    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)) κ μ
⊢ 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:
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 (hf_indep.indepFun_finset {i, j} {k, l} (by aesop) hf_meas).comp (hg i j) (hg k 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
⊢ 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:
iIndepFun.indepFun_prodMk_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ _ hik hil
      hjk hjl

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk, AEMeasurable.measurable_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
refine : iIndepFun (β := β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ
⊢ 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:
refine iIndepFun.indepFun_prodMk_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ _ hik hil
      hjk hjl

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk, AEMeasurable.measurable_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
⊢ iIndepFun (β := β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
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