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 : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen :
  MeasurableSpace.comap (β := (i : ↥S) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥S) ↦ β (↑a : ι))) =
    generateFrom πS
πTβ : Set (Set ((i : ↥T) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥T) ↦ Set (β (↑i : ι))) univ fun (i : ↥T) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πT : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πTβ, (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen :
  MeasurableSpace.comap (β := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥T) ↦ β (↑a : ι))) =
    generateFrom πT
s : Set ((i : ↥S) → β (↑i : ι))
sets_s : (i : ↥S) → Set (β (↑i : ι))
hs2 : Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s = s
t : Set ((i : ↥T) → β (↑i : ι))
sets_t : (i : ↥T) → Set (β (↑i : ι))
ht2 : Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) :=
  fun (i : ι) ↦ if hi : i ∈ S then sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi) else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi)
h_sets_s'_univ : ∀ {i : ι} (_hi : i ∈ T), sets_s' i = univ
sets_t' : (i : ι) → Set (β i) :=
  fun (i : ι) ↦ if hi : i ∈ T then sets_t (Subtype.mk (p := fun (x : ι) ↦ x ∈ T) i hi) else univ
h_sets_t'_univ : ∀ {i : ι} (_hi : i ∈ S), sets_t' i = univ
h_meas_s' : ∀ i ∈ S, MeasurableSet (sets_s' i)
h_meas_t' : ∀ i ∈ T, MeasurableSet (sets_t' i)
h_eq_inter_S :
  Eq.{u_2 + 1} (α := Set Ω)
    ((fun (ω : Ω) (i : ↥S) ↦ f (↑i : ι) ω) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s)
    (⋂ i ∈ S, f i ⁻¹' sets_s' i)
⊢ Eq.{u_2 + 1} (α := Set Ω)
    ((fun (ω : Ω) (i : ↥T) ↦ f (↑i : ι) ω) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t)
    (⋂ i ∈ T, f i ⁻¹' sets_t' i)

Tactic:
have h_eq_inter_T : (fun (ω : Ω) (i : ↥T) => f (↑i) ω) ⁻¹' Set.pi Set.univ sets_t
    = ⋂ i ∈ T, f i ⁻¹' sets_t' i := by
    ext1 x
    simp only [Set.mem_preimage, Set.mem_univ_pi, Set.mem_iInter]
    constructor <;> intro h
    · intro i hi; simp_rw [sets_t', dif_pos hi]; exact h ⟨i, hi⟩
    · rintro ⟨i, hi⟩; specialize h i hi; simp_rw [sets_t', dif_pos hi] at h; exact h
-- 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 : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πS : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πSβ, (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen :
  MeasurableSpace.comap (β := (i : ↥S) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥S) ↦ β (↑a : ι))) =
    generateFrom πS
πTβ : Set (Set ((i : ↥T) → β (↑i : ι))) :=
  Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ ''
    Set.pi (α := fun (i : ↥T) ↦ Set (β (↑i : ι))) univ fun (i : ↥T) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}
πT : Set (Set Ω) := {s : Set Ω | ∃ t ∈ πTβ, (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen :
  MeasurableSpace.comap (β := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥T) ↦ β (↑a : ι))) =
    generateFrom πT
s : Set ((i : ↥S) → β (↑i : ι))
sets_s : (i : ↥S) → Set (β (↑i : ι))
hs2 : Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s = s
t : Set ((i : ↥T) → β (↑i : ι))
sets_t : (i : ↥T) → Set (β (↑i : ι))
ht2 : Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) :=
  fun (i : ι) ↦ if hi : i ∈ S then sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi) else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi)
h_sets_s'_univ : ∀ {i : ι} (_hi : i ∈ T), sets_s' i = univ
sets_t' : (i : ι) → Set (β i) :=
  fun (i : ι) ↦ if hi : i ∈ T then sets_t (Subtype.mk (p := fun (x : ι) ↦ x ∈ T) i hi) else univ
h_sets_t'_univ : ∀ {i : ι} (_hi : i ∈ S), sets_t' i = univ
h_meas_s' : ∀ i ∈ S, MeasurableSet (sets_s' i)
h_meas_t' : ∀ i ∈ T, MeasurableSet (sets_t' i)
h_eq_inter_S :
  Eq.{u_2 + 1} (α := Set Ω)
    ((fun (ω : Ω) (i : ↥S) ↦ f (↑i : ι) ω) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s)
    (⋂ i ∈ S, f i ⁻¹' sets_s' i)
h_eq_inter_T :
  Eq.{u_2 + 1} (α := Set Ω)
    ((fun (ω : Ω) (i : ↥T) ↦ f (↑i : ι) ω) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t)
    (⋂ i ∈ T, f i ⁻¹' sets_t' i)
⊢ iIndepFun (β := β) f η μ

Tactic:
replace hf_Indep := hf_Indep.congr η_eq
-- 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 : (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 Ω) ∘ₘ μ)
⊢ 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)
    κ μ

Tactic:
iIndepFun.indepFun_finset S T hST ?_ fun i ↦ (hf_meas i).measurable_mk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, 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 : (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 Ω) ∘ₘ μ)
refine : iIndepFun (β := β) (fun (i : ι) ↦ AEMeasurable.mk (f i) ⋯) κ μ
⊢ 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)
    κ μ

Tactic:
refine iIndepFun.indepFun_finset S T hST ?_ fun i ↦ (hf_meas i).measurable_mk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, 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 : (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 Ω) ∘ₘ μ)
⊢ iIndepFun (β := β) (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 : (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 Ω) ∘ₘ μ)
⊢ iIndepFun (β := β) (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 : (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 Ω) ∘ₘ μ)
⊢ 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)
    κ μ

Tactic:
have h : IndepFun (fun a (i : S) ↦ (hf_meas i).mk (f i) a)
      (fun a (i : T) ↦ (hf_meas i).mk (f i) a) κ μ := by
    refine iIndepFun.indepFun_finset S T hST ?_ fun i ↦ (hf_meas i).measurable_mk
    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 : (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)
    κ μ
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ

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 : (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)
    κ μ
refine_1 :
  ∀ᵐ (a : α) ∂μ,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥S) → β (↑i : ι))
      (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a
refine_2 :
  ∀ᵐ (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
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ

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 : (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)
    κ μ
rw :
  ∀ (i : ↥S),
    ∀ᵐ (a : α) ∂μ,
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
⊢ ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥S),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (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 : (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)
    κ μ
⊢ ∀ (i : ↥S),
    ∀ᵐ (a : α) ∂μ,
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (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 : (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)
    κ μ
⊢ ∀ (i : ↥S),
    ∀ᵐ (a : α) ∂μ,
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (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 : (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 : ↥S),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (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 : (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 : ι)) ⋯)
h₁ :
  ∀ (a : α)
    (ha :
      ∀ (i : ↥S),
        (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
          (AEMeasurable.mk (f (↑i : ι)) ⋯)),
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥S) → β (↑i : ι))
      (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a
⊢ ∀ᵐ (a : α) ∂μ,
    (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥S) → β (↑i : ι))
      (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a

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 : (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 : ι)) ⋯)
h₁ :
  ∀ (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
⊢ (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := (i : ↥S) → β (↑i : ι))
    (fun (a : Ω) (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ a) fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a

Tactic:
filter_upwards [ae_all_iff.2 ha] with b hb

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 : (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)
h₁ : ∀ (i : ↥S), Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) ⋯ b) (f (↑i : ι) b)
⊢ Eq (α := (i : ↥S) → β (↑i : ι)) (fun (i : ↥S) ↦ AEMeasurable.mk (f (↑i : ι)) ⋯ b) fun (i : ↥S) ↦ f (↑i : ι) b

Tactic:
ext i
-- 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 : (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)
i : ↥S
⊢ Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) ⋯ b) (f (↑i : ι) b)

Tactic:
(hb i).symm

Premises used: Eq.symm
-- 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 : (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)
i : ↥S
⊢ Eq (α := β (↑i : ι)) (AEMeasurable.mk (f (↑i : ι)) ⋯ b) (f (↑i : ι) b)

Tactic:
exact (hb i).symm

Premises used: Eq.symm
-- 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 : (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)
    κ μ
rw :
  ∀ (i : ↥T),
    ∀ᵐ (a : α) ∂μ,
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)
⊢ ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥T),
      (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)).EventuallyEq (β := β (↑i : ι)) (f (↑i : ι))
        (AEMeasurable.mk (f (↑i : ι)) ⋯)

Tactic:
rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff