-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
inl :
  ∀ (hs : iIndepSet s κ 0),
    Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ 0
inr inr₁ :
  ∀ (hμ : μ ≠ 0), Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η),
    Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η),
    Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) η μ
inr₄ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η),
    Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T))
      η μ
inr₅ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η) (t : Set Ω)
    (ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t) (n : ι), generateFrom {s n} ≤ _mΩ
inr₆ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η) (t : Set Ω)
    (ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) T) t) (n : ι), generateFrom {s n} ≤ _mΩ
inr₇ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (k : ι) ↦ {s k}) S)
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
have inr₈ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (k : ι) ↦ {s k}) T)
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
  refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST