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
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
⊢ ∀ (i : ↥T),
    ∀ᵐ (a : α) ∂μ,
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)

Tactic:
fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Subtype.val
-- 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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
⊢ ∀ (i : ↥T),
    ∀ᵐ (a : α) ∂μ,
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)

Tactic:
exact fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

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
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)

Tactic:
have : ∀ᵐ (a : α) ∂μ, ∀ (i : T), f i =ᵐ[κ a] (hf_meas i).mk := by
      rw [ae_all_iff]
      exact 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
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
h₁ :
  ∀ (a : α)
    (ha :
      ∀ (i : ↥T),
        (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
          (AEMeasurable.mk (f (↑i : ι)) ⋯)),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥T) → β (↑i : ι))
      (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a
⊢ ∀ᵐ (a : α) ∂μ,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥T) → β (↑i : ι))
      (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a

Tactic:
filter_upwards [this] with a ha
-- 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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
a : α
ha :
  ∀ (i : ↥T),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
      (AEMeasurable.mk (f (↑i : ι)) ⋯)
h₁ :
  ∀ (b : Ω) (hb : ∀ (i : ↥T), Eq (α := β (↑i : ι)) (f (↑i : ι) b) (AEMeasurable.mk (f (↑i : ι)) ⋯ b)),
    Eq (α := (i : ↥T) → β (↑i : ι)) (fun (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ b) fun (i : ↥T) ↦ f (↑i : ι) b
⊢ (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a

Tactic:
filter_upwards [ae_all_iff.2 ha] with b hb

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- 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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
a : α
ha :
  ∀ (i : ↥T),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
      (AEMeasurable.mk (f (↑i : ι)) ⋯)
b : Ω
hb : ∀ (i : ↥T), Eq (α := β (↑i : ι)) (f (↑i : ι) b) (AEMeasurable.mk (f (↑i : ι)) ⋯ b)
h₁ : ∀ (i : ↥T), Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) ⋯ b) (f (↑i : ι) b)
⊢ Eq (α := (i : ↥T) → β (↑i : ι)) (fun (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ b) fun (i : ↥T) ↦ f (↑i : ι) b

Tactic:
ext i
-- 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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
a : α
ha :
  ∀ (i : ↥T),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
      (AEMeasurable.mk (f (↑i : ι)) ⋯)
b : Ω
hb : ∀ (i : ↥T), Eq (α := β (↑i : ι)) (f (↑i : ι) b) (AEMeasurable.mk (f (↑i : ι)) ⋯ b)
i : ↥T
⊢ Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) ⋯ b) (f (↑i : ι) b)

Tactic:
(hb i).symm

Premises used: Eq.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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
h :
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a)
    κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
a : α
ha :
  ∀ (i : ↥T),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
      (AEMeasurable.mk (f (↑i : ι)) ⋯)
b : Ω
hb : ∀ (i : ↥T), Eq (α := β (↑i : ι)) (f (↑i : ι) b) (AEMeasurable.mk (f (↑i : ι)) ⋯ b)
i : ↥T
⊢ Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) ⋯ b) (f (↑i : ι) b)

Tactic:
exact (hb i).symm

Premises used: Eq.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 j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ 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

Tactic:
have h_right :
      f k = (fun p : ∀ j : ({k} : Finset ι), β j => p ⟨k, Finset.mem_singleton_self k⟩) ∘
        fun a (j : ({k} : 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 : (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
⊢ 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 ⋯)

Tactic:
have h_meas_right : Measurable fun p : ∀ j : ({k} : Finset ι),
      β j => p ⟨k, Finset.mem_singleton_self k⟩ :=
    measurable_pi_apply _
-- 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 :
  ∀ (a : Ω),
    (f i a, f j a) =
      ((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)
        a
⊢ 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)

Tactic:
ext1 a
-- 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}
a : Ω
h :
  (f i a, f j a) =
    ((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)
      a
⊢ (f i a, f j a) =
    ((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)
      a

Tactic:
simp only
-- 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}
a : Ω
⊢ (f i a, f j a) =
    ((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)
      a

Tactic:
constructor
-- 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}
⊢ 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)

Tactic:
have h_left : (fun ω => (f i ω, f j ω)) = (fun p : ∀ l : s, β l =>
      (p ⟨i, Finset.mem_insert_self i _⟩,
        p ⟨j, Finset.mem_insert_of_mem (Finset.mem_singleton_self _)⟩)) ∘
        fun a (j : s) => f j a := by
    ext1 a
    simp only
    constructor
-- 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)
⊢ 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 ⋯))

Tactic:
have h_meas_left : Measurable fun p : ∀ l : s, β l =>
      (p ⟨i, Finset.mem_insert_self i _⟩,
        p ⟨j, Finset.mem_insert_of_mem (Finset.mem_singleton_self _)⟩) :=
    Measurable.prod (measurable_pi_apply _) (measurable_pi_apply _)
-- 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 :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k)
    ((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)
    ((fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
      fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    κ μ
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ

Tactic:
rw [h_left, h_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 ⋯))
⊢ IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k)
    ((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)
    ((fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
      fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    κ μ

Tactic:
(hf_Indep.indepFun_finset s {k} ?_ hf_meas).comp h_meas_left h_meas_right

Premises used: 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 : ι
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 ⋯))
refine : Disjoint s {k}
⊢ IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k)
    ((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)
    ((fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
      fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    κ μ

Tactic:
refine (hf_Indep.indepFun_finset s {k} ?_ hf_meas).comp h_meas_left h_meas_right

Premises used: ProbabilityTheory.Kernel.IndepFun.comp, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, Singleton.singleton