-- Mathlib/Probability/Independence/Kernel.lean
lemma iIndepFun.indepFun_prod_mk_prod_mk (hf_indep : iIndepFun m f κ μ)
    (hf_meas : ∀ i, Measurable (f i))
    (i j k l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) :
    IndepFun (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) κ μ

Proof state:
α : 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 m f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ

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

Result:
α : 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 m 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 : ι) → ((x : { x // x ∈ {i, j} }) → β ↑x) → β i × β j := fun i j v => (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
⊢ IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ

Proof state:
α : 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 m 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 : ι) → ((x : { x // x ∈ {i, j} }) → β ↑x) → β i × β j := fun i j v => (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
i j : ι
⊢ Measurable (g i j)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : 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 m 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 : ι) → ((x : { x // x ∈ {i, j} }) → β ↑x) → β i × β j := fun i j v => (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
hg : ∀ (i j : ι), Measurable (g i j)
⊢ Disjoint {i, j} {k, l}

Tactic:
aesop

Result:
no goals

Proof state:
α : 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 m f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun (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)

Result:
no goals

Proof state:
α : 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 m 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 : ι) → ((x : { x // x ∈ {i, j} }) → β ↑x) → β i × β j := fun i j v => (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
⊢ IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ

Tactic:
have hg (i j : ι) : Measurable (g i j) := by fun_prop

Result:
α : 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 m 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 : ι) → ((x : { x // x ∈ {i, j} }) → β ↑x) → β i × β j := fun i j v => (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
hg : ∀ (i j : ι), Measurable (g i j)
⊢ IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ

Proof state:
α : 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 m 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 : ι) → ((x : { x // x ∈ {i, j} }) → β ↑x) → β i × β j := fun i j v => (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
hg : ∀ (i j : ι), Measurable (g i j)
⊢ IndepFun (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)

Result:
no goals