-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
inr inr₁ : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
inr₄ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
inr₅ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)
inr₆ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η),
    IndepSets (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
      (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T) η μ
inr₇ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)
inr₈ inr₉ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η),
    IndepSets (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
      (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T) η μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ

Tactic:
classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST

Premises used: iSup₂_le, MeasurableSpace.isPiSystem_measurableSet, generateFrom_piiUnionInter_measurableSet, isPiSystem_piiUnionInter, eq_or_ne, ProbabilityTheory.Kernel.IndepSets.indep, OfNat.ofNat, Eq.symm, rfl, ProbabilityTheory.Kernel