-- 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 (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter_1 :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
a : α
h_P_inter :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
ha1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1, f1 i) : ℝ≥0∞)
    (∏ i ∈ p1, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f1 i) : ℝ≥0∞)
ha2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p2, f2 i) : ℝ≥0∞)
    (∏ i ∈ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f2 i) : ℝ≥0∞)
h' : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)
h_μg :
  ∀ (n : ι),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (if n ∈ p1 then (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f1 n) else 1 : ℝ≥0∞)
        (if n ∈ p2 then (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f2 n) else 1 : ℝ≥0∞)
h :
  ∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have h₁ : ∏ x ∈ p1 ∪ p2,
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (if x ∈ p1 then (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f1 x) else 1 : ℝ≥0∞)
      (if x ∈ p2 then (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f2 x) else 1 : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: simp_rw [h_P_inter, h_μg, Finset.prod_mul_distrib,
    Finset.prod_ite_mem (p1 ∪ p2) p1 (fun x ↦ κ a (f1 x)), Finset.union_inter_cancel_left,
    Finset.prod_ite_mem (p1 ∪ p2) p2 (fun x => κ a (f2 x)), Finset.union_inter_cancel_right, ht1_eq,
      ← ha1, ht2_eq, ← ha2]