Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi 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 ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
h_sets_t'_univ : ∀ {i : ι}, 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 : (fun ω i ↦ f (↑i) ω) ⁻¹' univ.pi sets_s = ⋂ i ∈ S, f i ⁻¹' sets_s' i
h_eq_inter_T : (fun ω i ↦ f (↑i) ω) ⁻¹' univ.pi sets_t = ⋂ i ∈ T, f i ⁻¹' sets_t' i
hf_Indep :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (η a) (f i ⁻¹' sets i)
h_Inter_inter : (⋂ i ∈ S, f i ⁻¹' sets_s' i) ∩ ⋂ i ∈ T, f i ⁻¹' sets_t' i = ⋂ i ∈ S ∪ T, f i ⁻¹' (sets_s' i ∩ sets_t' i)
h_meas_inter : ∀ i ∈ S ∪ T, MeasurableSet (sets_s' i ∩ sets_t' i)
a : α
h_indepS : (η a) (⋂ i ∈ S, f i ⁻¹' sets_s' i) = ∏ i ∈ S, (η a) (f i ⁻¹' sets_s' i)
h_indepT : (η a) (⋂ i ∈ T, f i ⁻¹' sets_t' i) = ∏ i ∈ T, (η a) (f i ⁻¹' sets_t' i)
h_indepST : (η a) (⋂ i ∈ S ∪ T, f i ⁻¹' (sets_s' i ∩ sets_t' i)) = ∏ i ∈ S ∪ T, (η a) (f i ⁻¹' (sets_s' i ∩ sets_t' i))
⊢ (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t) =
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t)

Tactic:
rw [h_eq_inter_S, h_eq_inter_T, h_indepS, h_indepT, h_Inter_inter, h_indepST,
    Finset.prod_union hST]

Goal state after:
α : 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_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi 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 ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
h_sets_t'_univ : ∀ {i : ι}, 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 : (fun ω i ↦ f (↑i) ω) ⁻¹' univ.pi sets_s = ⋂ i ∈ S, f i ⁻¹' sets_s' i
h_eq_inter_T : (fun ω i ↦ f (↑i) ω) ⁻¹' univ.pi sets_t = ⋂ i ∈ T, f i ⁻¹' sets_t' i
hf_Indep :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (η a) (f i ⁻¹' sets i)
h_Inter_inter : (⋂ i ∈ S, f i ⁻¹' sets_s' i) ∩ ⋂ i ∈ T, f i ⁻¹' sets_t' i = ⋂ i ∈ S ∪ T, f i ⁻¹' (sets_s' i ∩ sets_t' i)
h_meas_inter : ∀ i ∈ S ∪ T, MeasurableSet (sets_s' i ∩ sets_t' i)
a : α
h_indepS : (η a) (⋂ i ∈ S, f i ⁻¹' sets_s' i) = ∏ i ∈ S, (η a) (f i ⁻¹' sets_s' i)
h_indepT : (η a) (⋂ i ∈ T, f i ⁻¹' sets_t' i) = ∏ i ∈ T, (η a) (f i ⁻¹' sets_t' i)
h_indepST : (η a) (⋂ i ∈ S ∪ T, f i ⁻¹' (sets_s' i ∩ sets_t' i)) = ∏ i ∈ S ∪ T, (η a) (f i ⁻¹' (sets_s' i ∩ sets_t' i))
⊢ (∏ x ∈ S, (η a) (f x ⁻¹' (sets_s' x ∩ sets_t' x))) * ∏ x ∈ T, (η a) (f x ⁻¹' (sets_s' x ∩ sets_t' x)) =
    (∏ i ∈ S, (η a) (f i ⁻¹' sets_s' i)) * ∏ i ∈ T, (η a) (f i ⁻¹' sets_t' i)