-- 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
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)
inr inr₁ inr₂ :
  ∀ᵐ (a : α) ∂μ,
    (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s ∩
          (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s) :
          ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t) :
          ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s ∩
          (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s) :
          ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t) :
          ENNReal)
have inr₃ : let 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)),
  ∀ᵐ (a : α) ∂μ,
    (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s ∩
          (fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥S) ↦ β (↑i : ι)) univ sets_s) :
          ENNReal)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a) ⁻¹' Set.pi (α := fun (i : ↥T) ↦ β (↑i : ι)) univ sets_t) :
          ENNReal)
Tactic: classical
  let sets_s' : ∀ i : ι, Set (β i) := fun i =>
    dite (i ∈ S) (fun hi => sets_s ⟨i, hi⟩) fun _ => Set.univ
  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]
  have h_sets_s'_univ : ∀ {i} (_hi : i ∈ T), sets_s' i = Set.univ := by
    intro i hi; simp_rw [sets_s', dif_neg (Finset.disjoint_right.mp hST hi)]
  let sets_t' : ∀ i : ι, Set (β i) := fun i =>
    dite (i ∈ T) (fun hi => sets_t ⟨i, hi⟩) fun _ => Set.univ
  have h_sets_t'_univ : ∀ {i} (_hi : i ∈ S), sets_t' i = Set.univ := by
    intro i hi; simp_rw [sets_t', dif_neg (Finset.disjoint_left.mp hST hi)]
  have h_meas_s' : ∀ i ∈ S, MeasurableSet (sets_s' i) := by
    intro i hi; rw [h_sets_s'_eq hi]; exact hs1 _
  have h_meas_t' : ∀ i ∈ T, MeasurableSet (sets_t' i) := by
    intro i hi; simp_rw [sets_t', dif_pos hi]; exact ht1 _
  have h_eq_inter_S : (fun (ω : Ω) (i : ↥S) =>
    f (↑i) ω) ⁻¹' Set.pi Set.univ sets_s = ⋂ i ∈ S, f i ⁻¹' sets_s' i := by
    ext1 x
    simp_rw [Set.mem_preimage, Set.mem_univ_pi, Set.mem_iInter]
    grind
  have h_eq_inter_T : (fun (ω : Ω) (i : ↥T) => f (↑i) ω) ⁻¹' Set.pi Set.univ sets_t
    = ⋂ i ∈ T, f i ⁻¹' sets_t' i := by
    ext1 x
    simp only [Set.mem_preimage, Set.mem_univ_pi, Set.mem_iInter]
    constructor <;> intro h
    · intro i hi; simp_rw [sets_t', dif_pos hi]; exact h ⟨i, hi⟩
    · rintro ⟨i, hi⟩; specialize h i hi; simp_rw [sets_t', dif_pos hi] at h; exact h
  replace hf_Indep := hf_Indep.congr η_eq
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at hf_Indep
  have 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) := by
    ext1 x
    simp_rw [Set.mem_inter_iff, Set.mem_iInter, Set.mem_preimage, Finset.mem_union]
    constructor <;> intro h
    · grind
    · exact ⟨fun i hi => (h i (Or.inl hi)).1, fun i hi => (h i (Or.inr hi)).2⟩
  have h_meas_inter : ∀ i ∈ S ∪ T, MeasurableSet (sets_s' i ∩ sets_t' i) := by
    intro i hi_mem
    rw [Finset.mem_union] at hi_mem
    rcases hi_mem with hi_mem | hi_mem
    · rw [h_sets_t'_univ hi_mem, Set.inter_univ]
      exact h_meas_s' i hi_mem
    · rw [h_sets_s'_univ hi_mem, Set.univ_inter]
      exact h_meas_t' i hi_mem
  filter_upwards [hf_Indep S h_meas_s', hf_Indep T h_meas_t', hf_Indep (S ∪ T) h_meas_inter]
    with a h_indepS h_indepT h_indepST
  rw [h_eq_inter_S, h_eq_inter_T, h_indepS, h_indepT, h_Inter_inter, h_indepST,
    Finset.prod_union hST]
  congr 1
  · refine Finset.prod_congr rfl fun i hi => ?_
    rw [h_sets_t'_univ hi, Set.inter_univ]
  · refine Finset.prod_congr rfl fun i hi => ?_
    rw [h_sets_s'_univ hi, Set.univ_inter]