-- 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 α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : (n : ι) → Set Ω := fun (n : ι) ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h_t2 : t2 = f a
h_μ_inter :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
has : a ∉ s
a' : α
ha1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
ha2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h :
  ∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
h₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
      (∏ x ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f x) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
h₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
      (∏ x ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f x) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
h₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (∏ x ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f x) : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥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₄ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
    (∏ x ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f x) : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
    (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
Tactic: rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]