-- 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Ω
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec :
  ∀
    (_H :
      ∀ i ∈ S,
        Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
        (∏ i ∈ S, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
hf_m :
  ∀ i ∈ insert a S,
    Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π (↑S : Set ι)
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h :
  ∀ᵐ (a_1 : α) ∂μ,
    (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)
a' : α
ha' :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
    (∏ i ∈ S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
h' :
  (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ x ∈ S, f x) : ℝ≥0∞)
    (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
h₂ :
  (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ x ∈ S, f x) =
    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∞)
h₃ h₄ h₅ h₆ :
  (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ x ∈ S, f x) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ insert a S, f i) : ℝ≥0∞)
    (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']

Premises used: Finset.prod_insert, Finset.set_biInter_insert