-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepFun.indepFun_prod_mk (hf_Indep : iIndepFun m f κ μ)
    (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) :
    IndepFun (fun a => (f i a, f j a)) (f k) κ μ

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ

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

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ

Tactic:
let s : Finset ι := {i, j}

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
s : Finset ι := {i, j}
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
s : Finset ι := {i, j}
⊢ (fun ω => (f i ω, f j ω)) = (fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a

Tactic:
ext1 a

Result:
case h
α : 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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
s : Finset ι := {i, j}
a : Ω
⊢ (f i a, f j a) = ((fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a) 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 : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ

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

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
s : Finset ι := {i, j}
h_left : (fun ω => (f i ω, f j ω)) = (fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a
h_meas_left : Measurable fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)
⊢ IndepFun ((fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a) ((fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a) κ μ

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

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
s : Finset ι := {i, j}
h_left : (fun ω => (f i ω, f j ω)) = (fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a
h_meas_left : Measurable fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)
⊢ Disjoint s {k}

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
s : Finset ι := {i, j}
h_left : (fun ω => (f i ω, f j ω)) = (fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ

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 _)

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 : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨k, ⋯⟩
s : Finset ι := {i, j}
h_left : (fun ω => (f i ω, f j ω)) = (fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a
h_meas_left : Measurable fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)
⊢ IndepFun (fun a => (f i a, f j a)) (f k) κ μ