-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
intro :
  ∀ (val : Fintype ι),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
        (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
intro₁ :
  ∀ (val : Fintype ι),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
        (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
intro₂ :
  ∀ (val : Fintype ι) (hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
        (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
intro₃ :
  ∀ (val : Fintype ι),
    let g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i';
    ∀ (hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)) (hg : ∀ (i : ι), MeasurableSet (g i)),
      ∀ᵐ (a : α) ∂μ,
        Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
          (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
h :
  ∀ (val : Fintype ι),
    let g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i';
    ∀ (hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)) (hg : ∀ (i : ι), MeasurableSet (g i)) (a : α)
      (hy :
        ∀ i ∉ s,
          Ne (α := ENNReal)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
            (0 : ENNReal)),
      IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a) →
        ∀
          (hYt :
            Eq (α := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i) : ENNReal)
              (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal))
          (hg :
            Eq (α := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
              (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)),
          Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
            (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
      (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)

Tactic:
classical
  cases nonempty_fintype ι
  let g (i' : ι) := if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
  have hYt i : MeasurableSet[(mα.prod mβ).comap fun ω ↦ (X i ω, Y i ω)] (Y i ⁻¹' t i) :=
    ⟨.univ ×ˢ t i, .prod .univ (ht _), by ext; simp⟩
  have hg i : MeasurableSet[(mα.prod mβ).comap fun ω ↦ (X i ω, Y i ω)] (g i) := by
    by_cases hi : i ∈ s <;> simp only [hi, ↓reduceIte, g]
    · obtain ⟨A, hA, hA'⟩ := hf i hi
      exact (hYt _).inter ⟨A ×ˢ .univ, hA.prod .univ, by ext; simp [← hA']⟩
    · exact hYt _
  filter_upwards [hy, hindep.ae_isProbabilityMeasure, hindep.meas_iInter hYt, hindep.meas_iInter hg]
    with a hy _ hYt hg
  calc
    _ = (κ a (⋂ i, Y i ⁻¹' t i))⁻¹ * κ a ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) := by
      rw [cond_apply]; exact .iInter fun i ↦ hY i (ht i)
    _ = (κ a (⋂ i, Y i ⁻¹' t i))⁻¹ * κ a (⋂ i, g i) := by
      congr 2
      calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          congr 1
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]
    _ = (∏ i, κ a (Y i ⁻¹' t i))⁻¹ * κ a (⋂ i, g i) := by
      rw [hYt]
    _ = (∏ i, κ a (Y i ⁻¹' t i))⁻¹ * ∏ i, κ a (g i) := by
      rw [hg]
    _ = ∏ i, (κ a (Y i ⁻¹' t i))⁻¹ * κ a (g i) := by
      rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _
    _ = ∏ i, if i ∈ s then (κ a)[f i | Y i ⁻¹' t i] else 1 := by
      refine Finset.prod_congr rfl fun i _ ↦ ?_
      by_cases hi : i ∈ s
      · simp only [hi, ↓reduceIte, g, cond_apply (hY i (ht i))]
      · simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top _ _)]
    _ = _ := by simp

Premises used: nonempty_fintype, ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure