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}
⊢ IsPiSystem πT

Tactic:
exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _

Premises used: IsPiSystem.comap, isPiSystem_pi
-- 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}
⊢ IsPiSystem πT

Tactic:
have hπT_pi : IsPiSystem πT := by exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _
-- 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
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
⊢ MeasurableSpace.comap (β := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a)
      (MeasurableSpace.pi (X := fun (a : ↥T) ↦ β (↑a : ι))) =
    generateFrom πT

Tactic:
rw [generateFrom_pi.symm, comap_generateFrom]

Premises used: generateFrom_pi, Eq.symm, MeasurableSpace.comap_generateFrom
-- 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
⊢ 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:
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 : ι), 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

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
-- 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
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ

Tactic:
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
    ?_

Premises used: Iff.mpr, measurable_pi_iff, Measurable.comap_le, ProbabilityTheory.Kernel.IndepFun, ProbabilityTheory.Kernel.IndepSets.indep, 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 : ι), 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
inr : IndepSets πS πT η μ
⊢ IndepFun (β := (i : ↥S) → β (↑i : ι)) (γ := (i : ↥T) → β (↑i : ι)) (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a)
    (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) η μ

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
    ?_
-- 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 : ι))
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
⊢ ∀ (i : ↥S), MeasurableSet (sets_s i)

Tactic:
simp only [Set.mem_univ_pi, Set.mem_setOf_eq] at hs1 ht1

Premises used: Set.mem_setOf_eq, Set.mem_univ_pi
-- 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 : ι))
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)
⊢ ∀ (i : ↥T), MeasurableSet (sets_t i)

Tactic:
simp only [Set.mem_univ_pi, Set.mem_setOf_eq] at hs1 ht1

Premises used: Set.mem_setOf_eq, Set.mem_univ_pi
-- 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
i : ι
hi : i ∈ S
simp_rw :
  Eq (α := Set (β i)) (if hi : i ∈ S then sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi) else univ : Set (β i))
    (sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi) : Set (β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi) : ι)))
⊢ sets_s' i = sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi)

Tactic:
simp_rw [sets_s', dif_pos hi]

Premises used: dif_pos
-- 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
⊢ ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi)

Tactic:
have h_sets_s'_eq : ∀ {i} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩ := by
    intro i hi; simp_rw [sets_s', dif_pos hi]
-- 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)
i : ι
hi : i ∈ T
simp_rw :
  Eq.{u_8 + 1} (α := Set (β i)) (if hi : i ∈ S then sets_s (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) i hi) else univ) univ
⊢ sets_s' i = univ

Tactic:
simp_rw [sets_s', dif_neg (Finset.disjoint_right.mp hST hi)]

Premises used: dif_neg, Iff.mp, Finset.disjoint_right