-- 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
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) κ μ

Tactic:
rw [h_left, h_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, ⋯⟩)
⊢ IndepFun ((fun p => (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j => f (↑j) a) ((fun p => p ⟨k, ⋯⟩) ∘ fun a j => f (↑j) 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
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) κ μ

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 [Prod.mk.inj_iff]
  constructor

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
⊢ 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, ⋯⟩)
⊢ Disjoint s {k}

Tactic:
rw [Finset.disjoint_singleton_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, ⋯⟩)
⊢ k ∉ s

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, ⋯⟩)
⊢ k ∉ s

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

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, ⋯⟩)
⊢ ¬k = i ∧ ¬k = j

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:
classical
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
have h_meas_right :  Measurable fun p : ∀ j : ({k} : Finset ι),
  β j => p ⟨k, Finset.mem_singleton_self k⟩ := measurable_pi_apply _
let s : Finset ι := {i, j}
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 [Prod.mk.inj_iff]
  constructor
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 _)
rw [h_left, h_right]
refine (hf_Indep.indepFun_finset s {k} ?_ hf_meas).comp h_meas_left h_meas_right
rw [Finset.disjoint_singleton_right]
simp only [s, Finset.mem_insert, Finset.mem_singleton, not_or]
exact ⟨hik.symm, hjk.symm⟩

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 : ι
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, ⋯⟩)
⊢ ¬k = i ∧ ¬k = j

Tactic:
exact ⟨hik.symm, hjk.symm⟩

Result:
no goals

Proof state:
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

Tactic:
constructor

Result:
no goals