awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : ↥S),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
a : α
ha :
  ∀ (i : ↥S),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
      (AEMeasurable.mk (f (↑i : ι)) ⋯)
b : Ω
hb : ∀ (i : ↥S), Eq (α := β (↑i : ι)) (f (↑i : ι) b) (AEMeasurable.mk (f (↑i : ι)) ⋯ b)
⊢ Eq (α := (i : ↥S) → β (↑i : ι)) (fun (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ b) fun (i : ↥S) ↦ f (↑i : ι) b
have h₁ : ∀ (i : ↥S), Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) sorry b) (f (↑i : ι) b)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : ι)) ⋯)
have rw : ∀ (i : ↥T),
  ∀ᵐ (a : α) ∂μ,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
      (AEMeasurable.mk (f (↑i : ι)) sorry)
Tactic: rw [ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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 : α) ∂μ,
    (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
have this : ∀ᵐ (a : α) ∂μ,
  ∀ (i : ↥T),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
      (AEMeasurable.mk (f (↑i : ι)) sorry)
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
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : α) ∂μ,
    (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
have h₁ : ∀ (a : α)
  (ha :
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) sorry)),
  (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥T) → β (↑i : ι))
    (fun (a : Ω) (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) sorry a) fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a
Tactic: filter_upwards [this] with a ha
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : ι)) ⋯)
⊢ (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
have h₁ : ∀ (b : Ω) (hb : ∀ (i : ↥T), Eq (α := β (↑i : ι)) (f (↑i : ι) b) (AEMeasurable.mk (f (↑i : ι)) sorry b)),
  Eq (α := (i : ↥T) → β (↑i : ι)) (fun (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) sorry b) fun (i : ↥T) ↦ f (↑i : ι) b
Tactic: filter_upwards [ae_all_iff.2 ha] with b hb
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
⊢ Eq (α := (i : ↥T) → β (↑i : ι)) (fun (i : ↥T) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ b) fun (i : ↥T) ↦ f (↑i : ι) b
have h₁ : ∀ (i : ↥T), Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) sorry b) (f (↑i : ι) b)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have h_right : f k =
  (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k sorry)) ∘
    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
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have h_meas_right : Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k sorry) : ι))
  fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k sorry)
Tactic: have h_meas_right : Measurable fun p : ∀ j : ({k} : Finset ι),
      β j => p ⟨k, Finset.mem_singleton_self k⟩ :=
    measurable_pi_apply _
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
have h : ∀ (a : Ω),
  (f i a, f j a) =
    ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
          (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i sorry), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j sorry))) ∘
        fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
      a
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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}
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have h_left : Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
  ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
      (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i sorry), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j sorry))) ∘
    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
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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)
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have h_meas_left : Measurable (β :=
  β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i sorry) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j sorry) : ι))
  fun (p : (l : ↥s) → β (↑l : ι)) ↦
  (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i sorry), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j sorry))
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 _)
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have 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 sorry), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j sorry))) ∘
    fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
  ((fun (p : (j : ↥{k}) → β (↑j : ι)) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k sorry)) ∘
    fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
  κ μ
Tactic: rw [h_left, h_right]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
    κ μ
have refine : Disjoint s {k}
Tactic: refine (hf_Indep.indepFun_finset s {k} ?_ hf_meas).comp h_meas_left h_meas_right
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 ⋯))
⊢ Disjoint s {k}
have rw : k ∉ s
Tactic: rw [Finset.disjoint_singleton_right]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 ⋯))
⊢ k ∉ s
have simp : ¬k = i ∧ ¬k = j
Tactic: simp only [s, Finset.mem_insert, Finset.mem_singleton, not_or]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have have : ∀
  (h_right :
    f k =
      (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
          p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k sorry)) ∘
        fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a),
  IndepFun (β := β i × β j) (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
    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⟩