no goals
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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)
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 [Finset.mem_insert, Finset.mem_singleton, not_or]
  exact ⟨hik.symm, hjk.symm⟩
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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)
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
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
have h_meas_right :  Measurable fun p : ∀ j : ({k} : Finset ι),
  β j => p ⟨k, Finset.mem_singleton_self k⟩ := measurable_pi_apply _
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
let s : Finset ι := {i, j}
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
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
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
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 _)
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ IndepFun
    ((fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘
      fun a j => f (↑j) a)
    ((fun p => p { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a)
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ IndepFun (fun a => (f i a, f j a)) (f k)
rw [h_left, h_right]
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ Disjoint s {k}
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ IndepFun
    ((fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘
      fun a j => f (↑j) a)
    ((fun p => p { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a)
refine' (hf_Indep.indepFun_finset s {k} _ hf_meas).comp h_meas_left h_meas_right
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ ¬k ∈ s
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ Disjoint s {k}
rw [Finset.disjoint_singleton_right]
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ ¬k = i ∧ ¬k = j
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ ¬k ∈ s
simp only [Finset.mem_insert, Finset.mem_singleton, not_or]
no goals
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
h_left :
  (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
h_meas_left :
  Measurable fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })
⊢ ¬k = i ∧ ¬k = j
exact ⟨hik.symm, hjk.symm⟩
case h
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
a : Ω
⊢ (f i a, f j a) =
    ((fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘
        fun a j => f (↑j) a)
      a
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
⊢ (fun ω => (f i ω, f j ω)) =
    (fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘ fun a j =>
      f (↑j) a
ext1 a
case h
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
a : Ω
⊢ (f i a, f j a) =
    ((fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘
        fun a j_1 => f (↑j_1) a)
      a
case h
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
a : Ω
⊢ (f i a, f j a) =
    ((fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘
        fun a j => f (↑j) a)
      a
simp only [Prod.mk.inj_iff]
no goals
case h
Ω : Type u_1
ι✝ : Type ?u.3447382
β✝ : Type ?u.3447385
β' : Type ?u.3447388
γ : Type ?u.3447391
γ' : Type ?u.3447394
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
β : ι → Type u_3
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 { val := k, property := (_ : k ∈ {k}) }) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p { val := k, property := (_ : k ∈ {k}) }
s : Finset ι := {i, j}
a : Ω
⊢ (f i a, f j a) =
    ((fun p => (p { val := i, property := (_ : i ∈ {i, j}) }, p { val := j, property := (_ : j ∈ {i, j}) })) ∘
        fun a j_1 => f (↑j_1) a)
      a
constructor