awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 :
  ∀ (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)
⊢ Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)

Tactic:
ext1 a
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : Ω
h : Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) (∏ x : ↥s, f (↑x : ι) 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:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : Ω
rw rw₁ : Eq.{u_8 + 1} (α := β) (∏ j : ↥s, f (↑j : ι) a) (∏ c : ↥s, f (↑c : ι) a)
⊢ Eq.{u_8 + 1} (α := β) (∏ j : ↥s, f (↑j : ι) a) ((∏ j : ↥s, f (↑j : ι)) a)

Tactic:
rw [Finset.prod_apply]

Premises used: Finset.prod_apply
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)

Tactic:
have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
h₁ h₂ : Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) ((∏ i ∈ s, f i) a)
⊢ Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, f j) a) (∏ x : ↥s, f (↑x : ι) a)

Tactic:
rw [this, Finset.prod_coe_sort]

Premises used: Finset.prod_coe_sort
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)

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]
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
⊢ 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
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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
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 ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ

Tactic:
rw [h_left, h_right]
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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.{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 ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    κ μ

Tactic:
(hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp
      h_meas_left h_meas_right

Premises used: Iff.mpr, ProbabilityTheory.Kernel.IndepFun.comp, Disjoint.symm, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, Finset.disjoint_singleton_left, Singleton.singleton
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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.{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 ⋯)) ∘
      fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    κ μ

Tactic:
exact
    (hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp
      h_meas_left h_meas_right

Premises used: Iff.mpr, ProbabilityTheory.Kernel.IndepFun.comp, Disjoint.symm, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, Finset.disjoint_singleton_left, Singleton.singleton
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
iIndepFun.indepFun_finsetProd_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
refine : iIndepFun (β := fun (x : ι) ↦ β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
refine iIndepFun.indepFun_finsetProd_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ iIndepFun (β := fun (x : ι) ↦ β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr', MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ iIndepFun (β := fun (x : ι) ↦ β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
exact iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr', MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ

Tactic:
have h : IndepFun (∏ j ∈ s, (hf_meas j).mk (f j)) ((hf_meas i).mk (f i)) κ μ := by
    refine iIndepFun.indepFun_finsetProd_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi
    exact iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ

Tactic:
IndepFun.congr' h ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.congr'
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
refine_1 :
  ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)
refine_2 : ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f i) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ

Tactic:
refine IndepFun.congr' h ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.congr'
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
rw :
  ∀ (i : ↥s),
    ∀ᵐ (a : α) ∂μ,
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
⊢ ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯

Tactic:
rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ (i : ↥s),
    ∀ᵐ (a : α) ∂μ,
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯

Tactic:
fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Subtype.val
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ (i : ↥s),
    ∀ᵐ (a : α) ∂μ,
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯

Tactic:
exact fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯

Tactic:
have : ∀ᵐ a ∂μ, ∀ (i : s), 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
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
h₁ :
  ∀ (a : α)
    (ha :
      ∀ (i : ↥s),
        f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯),
    Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)
⊢ ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)

Tactic:
filter_upwards [this] with a ha
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
a : α
ha :
  ∀ (i : ↥s),
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
h₁ :
  ∀ (ω : Ω) (hω : ∀ (i : ↥s), f (↑i : ι) ω = AEMeasurable.mk (f (↑i : ι)) ⋯ ω),
    Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, AEMeasurable.mk (f j) ⋯) ω) ((∏ j ∈ s, f j) ω)
⊢ Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
    (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)

Tactic:
filter_upwards [ae_all_iff.2 ha] with ω hω

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
a : α
ha :
  ∀ (i : ↥s),
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
ω : Ω
hω : ∀ (i : ↥s), f (↑i : ι) ω = AEMeasurable.mk (f (↑i : ι)) ⋯ ω
h₁ : Eq.{u_8 + 1} (α := β) (∏ c ∈ s, AEMeasurable.mk (f c) ⋯ ω) (∏ c ∈ s, f c ω)
⊢ Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, AEMeasurable.mk (f j) ⋯) ω) ((∏ j ∈ s, f j) ω)

Tactic:
simp only [Finset.prod_apply]

Premises used: Finset.prod_apply