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
hf_indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f l ω = AEMeasurable.mk (f l) ⋯ ω
⊢ Filter.EventuallyEq.{u_2, u_8} (β := β k × β l) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) fun (a : Ω) ↦ (f k a, f l a)
have h₁ : ∀ (ω : Ω) (hωk : f k ω = AEMeasurable.mk (f k) sorry ω) (hωl : f l ω = AEMeasurable.mk (f l) sorry ω),
  (AEMeasurable.mk (f k) sorry ω, AEMeasurable.mk (f l) sorry ω) = (f k ω, f l ω)
Tactic: filter_upwards [hk, hl] with ω hωk hωl
-- 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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f l ω = AEMeasurable.mk (f l) ⋯ ω
ω : Ω
hωk : f k ω = AEMeasurable.mk (f k) ⋯ ω
hωl : f l ω = AEMeasurable.mk (f l) ⋯ ω
⊢ (AEMeasurable.mk (f k) ⋯ ω, AEMeasurable.mk (f l) ⋯ ω) = (f k ω, f l ω)
have h₁ : (f k ω, AEMeasurable.mk (f l) sorry ω) = (f k ω, f l ω)
Tactic: rw [← hωk, ← hωl]
-- 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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k × β l)
    (fun (a : Ω) ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun (a : Ω) ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), f l ω = AEMeasurable.mk (f l) ⋯ ω
ω : Ω
hωk : f k ω = AEMeasurable.mk (f k) ⋯ ω
hωl : f l ω = AEMeasurable.mk (f l) ⋯ ω
h₁ : (f k ω, AEMeasurable.mk (f l) ⋯ ω) = (f k ω, f l ω)
⊢ (AEMeasurable.mk (f k) ⋯ ω, AEMeasurable.mk (f l) ⋯ ω) = (f k ω, f l ω)
have h₂ : (f k ω, f l ω) = (f k ω, f l ω)
Tactic: rw [← hωk, ← hωl]
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i * f j) (f k) κ μ
have this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
Tactic: have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i * f j) (f k) κ μ
have this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
Tactic: have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk₀ hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i / f j) (f k) κ μ
have this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
Tactic: have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i / f j) (f k) κ μ
have this : IndepFun (β := β × β) (fun (ω : Ω) ↦ (f i ω, f j ω)) (f k) κ μ
Tactic: have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk₀ hf_meas i j k hik hjk
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have h_right : f i =
  (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)) ∘
    fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
Tactic: have h_right : f i =
    (fun p : ({i} : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘
    fun a (j : ({i} : 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have h_meas_right : Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)
Tactic: have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
⊢ Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
have h : ∀ (a : Ω),
  Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a)
    (((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a) a)
Tactic: ext1 a
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
a : Ω
⊢ Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a)
    (((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a) a)
have h : Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) (∏ x : ↥s, f (↑x : ι) a)
Tactic: simp only [Function.comp_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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
a : Ω
⊢ Eq.{u_8 + 1} (α := β) (∏ j : ↥s, f (↑j : ι) a) ((∏ j : ↥s, f (↑j : ι)) a)
have rw : Eq.{u_8 + 1} (α := β) (∏ j : ↥s, f (↑j : ι) a) (∏ c : ↥s, f (↑c : ι) a)
Tactic: rw [Finset.prod_apply]
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
a : Ω
⊢ Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) (∏ x : ↥s, f (↑x : ι) a)
have this : Eq.{u_8 + 1} (α := β) (∏ j : ↥s, f (↑j : ι) a) ((∏ j : ↥s, f (↑j : ι)) a)
Tactic: have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
a : Ω
this : Eq.{u_8 + 1} (α := β) (∏ j : ↥s, f (↑j : ι) a) ((∏ j : ↥s, f (↑j : ι)) a)
⊢ Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) (∏ x : ↥s, f (↑x : ι) a)
have h : Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) ((∏ j : ↥s, f (↑j : ι)) a)
Tactic: rw [this, Finset.prod_coe_sort]
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
a : Ω
this : Eq.{u_8 + 1} (α := β) (∏ j : ↥s, f (↑j : ι) a) ((∏ j : ↥s, f (↑j : ι)) a)
h : Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) ((∏ j : ↥s, f (↑j : ι)) a)
⊢ Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) (∏ x : ↥s, f (↑x : ι) a)
have h₁ : Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) ((∏ i ∈ s, f i) a)
Tactic: rw [this, Finset.prod_coe_sort]
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have h_left : Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
Tactic: have h_left : ∏ j ∈ s, f j = (fun p : s → β => ∏ j, p j) ∘ fun a (j : s) => f j a := by
    ext1 a
    simp only [Function.comp_apply]
    have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
    rw [this, Finset.prod_coe_sort]
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
h_left : Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have h_meas_left : Measurable (β := β) fun (p : ↥s → β) ↦ ∏ j : ↥s, p j
Tactic: have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
    Finset.univ.measurable_fun_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j
-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right :
  f i =
    (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a
h_meas_right :
  Measurable (β := β) fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
h_left : Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
h_meas_left : Measurable (β := β) fun (p : ↥s → β) ↦ ∏ j : ↥s, p j
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have rw : IndepFun.{u_1, u_2, u_8, u_8} (β := β) (γ := β)
  ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
  ((fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)) ∘
    fun (a : Ω) (j : ↥{i}) ↦ 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have have : ∀
  (h_right :
    f i =
      (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)) ∘
        fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a),
  IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
Tactic: classical
  have h_right : f i =
    (fun p : ({i} : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘
    fun a (j : ({i} : Finset ι)) => f j a := rfl
  have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _
  have h_left : ∏ j ∈ s, f j = (fun p : s → β => ∏ j, p j) ∘ fun a (j : s) => f j a := by
    ext1 a
    simp only [Function.comp_apply]
    have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
    rw [this, Finset.prod_coe_sort]
  have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
    Finset.univ.measurable_fun_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j
  rw [h_left, h_right]
  exact
    (hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
have have₁ have₂ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have have₃ : ∀
  (h_right :
    f i =
      (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)) ∘
        fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
  (h_meas_right :
    Measurable (β := β) fun (p : ↥{i} → β) ↦
      p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)),
  IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
Tactic: classical
  have h_right : f i =
    (fun p : ({i} : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘
    fun a (j : ({i} : Finset ι)) => f j a := rfl
  have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _
  have h_left : ∏ j ∈ s, f j = (fun p : s → β => ∏ j, p j) ∘ fun a (j : s) => f j a := by
    ext1 a
    simp only [Function.comp_apply]
    have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
    rw [this, Finset.prod_coe_sort]
  have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
    Finset.univ.measurable_fun_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j
  rw [h_left, h_right]
  exact
    (hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
have have₁ have₂ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have₃ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β) fun (p : ↥{i} → β) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have have₄ : ∀
  (h_right :
    f i =
      (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)) ∘
        fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
  (h_meas_right :
    Measurable (β := β) fun (p : ↥{i} → β) ↦
      p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry))
  (h_left : Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)),
  IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
Tactic: classical
  have h_right : f i =
    (fun p : ({i} : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘
    fun a (j : ({i} : Finset ι)) => f j a := rfl
  have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _
  have h_left : ∏ j ∈ s, f j = (fun p : s → β => ∏ j, p j) ∘ fun a (j : s) => f j a := by
    ext1 a
    simp only [Function.comp_apply]
    have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
    rw [this, Finset.prod_coe_sort]
  have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
    Finset.univ.measurable_fun_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j
  rw [h_left, h_right]
  exact
    (hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp
      h_meas_left h_meas_right