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_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
rw rw₁ rw₂ :
  (∀ (s : Set β) (t : Set γ),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)) ↔
    Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
⊢ IndepFun f g κ μ ↔ Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
have refine_1 : ∀
  (h :
    ∀ (s : Set β) (t : Set γ),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)),
  Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
Tactic: classical
  rw [indepFun_iff_measure_inter_preimage_eq_mul]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [Measure.ext_prod₃_iff]
    intro u s t hu hs ht
    rw [Measure.compProd_apply (hu.prod (hs.prod ht)),
      Measure.compProd_apply (hu.prod (hs.prod ht))]
    refine lintegral_congr_ae ?_
    have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp
    simp_rw [h_set_eq]
    filter_upwards [h s t hs ht] with ω hω
    by_cases hωu : ω ∈ u
    swap; · simp [hωu]
    simp only [hωu, ↓reduceIte]
    rw [map_apply _ (by fun_prop), Measure.map_apply (by fun_prop) (hs.prod ht),
      mk_preimage_prod, hω, prod_apply_prod, map_apply' _ (by fun_prop), map_apply' _ (by fun_prop)]
    exacts [ht, hs]
  · intro s t hs ht
    rw [Measure.ext_prod₃_iff] at h
    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_
    · exact Kernel.measurable_coe _ ((hf hs).inter (hg ht))
    · exact (Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))
    intro u hu hμu
    specialize h hu hs ht
    rw [Measure.compProd_apply_prod hu (hs.prod ht),
      Measure.compProd_apply_prod hu (hs.prod ht)] at h
    convert! h with ω ω
    · rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]
    · rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ ht]
-- 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 : ι), Measurable (f i)
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
have inl : ∀ (hf_Indep : iIndepFun (β := β) f κ 0),
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ 0
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
Cleared hypotheses: μ, hf_Indep
-- 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 : ι), Measurable (f i)
inl :
  ∀ (hf_Indep : iIndepFun (β := β) f κ 0),
    IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ 0
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
have inr : ∀ (hμ : μ ≠ 0),
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
-- 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 : ι), Measurable (f i)
hμ : μ ≠ 0
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
have inr : ∀ (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η),
  IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
Tactic: obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hf_Indep.ae_isProbabilityMeasure hμ
-- 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 : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) κ μ
have inr : IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
  (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ
Tactic: apply IndepFun.congr (Filter.EventuallyEq.symm η_eq)
-- 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 : ι), 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}
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ
have hπS_pi : IsPiSystem πS
Tactic: have hπS_pi : IsPiSystem πS := by exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _
-- 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 : ι), 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
⊢ MeasurableSpace.comap (β := (i : ↥S) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥S) ↦ β (↑a : ι))) =
    generateFrom πS
have rw : generateFrom
    (image (α := Set ((i : ↥S) → β (↑i : ι))) (preimage fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
      (Set.pi (α := fun (a : ↥S) ↦ β (↑a : ι)) univ ''
        Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s})) =
  generateFrom πS
Tactic: rw [generateFrom_pi.symm, comap_generateFrom]
-- 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 : ι), 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
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ
have hπS_gen : MeasurableSpace.comap (β := (i : ↥S) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (MeasurableSpace.pi (X := fun (a : ↥S) ↦ β (↑a : ι))) =
  generateFrom πS
Tactic: have hπS_gen : (MeasurableSpace.pi.comap fun a (i : S) => f i a) = generateFrom πS := by
    rw [generateFrom_pi.symm, comap_generateFrom]
    congr
-- 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 : ι), 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}
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ
have hπT_pi : IsPiSystem πT
Tactic: have hπT_pi : IsPiSystem πT := by exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _
-- 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 : ι), 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
⊢ MeasurableSpace.comap (β := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥T) ↦ β (↑a : ι))) =
    generateFrom πT
have rw : generateFrom
    (image (α := Set ((i : ↥T) → β (↑i : ι))) (preimage fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a)
      (Set.pi (α := fun (a : ↥T) ↦ β (↑a : ι)) univ ''
        Set.pi (α := fun (i : ↥T) ↦ Set (β (↑i : ι))) univ fun (i : ↥T) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s})) =
  generateFrom πT
Tactic: rw [generateFrom_pi.symm, comap_generateFrom]
-- 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 : ι), 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
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ
have hπT_gen : MeasurableSpace.comap (β := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a)
    (MeasurableSpace.pi (X := fun (a : ↥T) ↦ β (↑a : ι))) =
  generateFrom πT
Tactic: have hπT_gen : (MeasurableSpace.pi.comap fun a (i : T) => f i a) = generateFrom πT := by
    rw [generateFrom_pi.symm, comap_generateFrom]
    congr
-- 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 : ι), 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
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ
have inr : IndepSets πS πT η μ
Tactic: refine IndepSets.indep (Measurable.comap_le (measurable_pi_iff.mpr fun i => hf_meas i))
    (Measurable.comap_le (measurable_pi_iff.mpr fun i => hf_meas i)) hπS_pi hπT_pi hπS_gen hπT_gen
    ?_
-- 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 : ι), 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 : ι))
hs1 :
  Membership.mem (γ := Set ((i : ↥S) → Set (β (↑i : ι))))
    (Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}) sets_s
hs2 : Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s = s
t : Set ((i : ↥T) → β (↑i : ι))
sets_t : (i : ↥T) → Set (β (↑i : ι))
ht1 :
  Membership.mem (γ := Set ((i : ↥T) → Set (β (↑i : ι))))
    (Set.pi (α := fun (i : ↥T) ↦ Set (β (↑i : ι))) univ fun (i : ↥T) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}) sets_t
ht2 : Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t = t
⊢ ∀ᵐ (a : α) ∂μ,
    (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' s ∩ (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' s) :
          ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' t) :
          ENNReal)
have hs1₁ : ∀ (i : ↥S), MeasurableSet (sets_s i)
Tactic: simp only [Set.mem_univ_pi, Set.mem_setOf_eq] at hs1 ht1
Cleared hypotheses: hs1, ht1
-- 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 : ι), 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 : ι))
hs1 :
  Membership.mem (γ := Set ((i : ↥S) → Set (β (↑i : ι))))
    (Set.pi (α := fun (i : ↥S) ↦ Set (β (↑i : ι))) univ fun (i : ↥S) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}) sets_s
hs2 : Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s = s
t : Set ((i : ↥T) → β (↑i : ι))
sets_t : (i : ↥T) → Set (β (↑i : ι))
ht1 :
  Membership.mem (γ := Set ((i : ↥T) → Set (β (↑i : ι))))
    (Set.pi (α := fun (i : ↥T) ↦ Set (β (↑i : ι))) univ fun (i : ↥T) ↦ {s : Set (β (↑i : ι)) | MeasurableSet s}) sets_t
ht2 : Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t = t
hs1₁ : ∀ (i : ↥S), MeasurableSet (sets_s i)
⊢ ∀ᵐ (a : α) ∂μ,
    (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' s ∩ (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' s) :
          ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' t) :
          ENNReal)
have ht1₁ : ∀ (i : ↥T), MeasurableSet (sets_t i)
Tactic: simp only [Set.mem_univ_pi, Set.mem_setOf_eq] at hs1 ht1
Cleared hypotheses: hs1, ht1