-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
rw rw₁ rw₂ :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
        (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
rw₃ :
  ∀
    (h₀ :
      ∀ {s : (i : ι) → Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)),
        Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
            (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i)) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) :
              ℝ≥0∞)),
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
        (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
      ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
        Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
          (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
rw₄ :
  ∀
    (h₀ :
      ∀ {s : (i : ι) → Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)),
        Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
            (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i)) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) :
              ℝ≥0∞))
    (h :
      Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
        (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ))
    (S : Finset ι) {s : (i : ι) → Set (β i)} (hs : ∀ i ∈ S, MeasurableSet (s i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
rw₅ :
  ∀
    (h :
      Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
        (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ))
    (S : Finset ι) {s : (i : ι) → Set (β i)} (hs : ∀ i ∈ S, MeasurableSet (s i))
    (h₀ :
      Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' if i ∈ S then s i else univ))
          (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (if i ∈ S then s i else univ)) ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' if i ∈ S then s i else univ) : ℝ≥0∞)
          ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞)
              (Set.pi (α := β) univ fun (i : ι) ↦ if i ∈ S then s i else univ) :
            ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
rw₆ :
  ∀
    (h :
      Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
        (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ))
    (S : Finset ι) {s : (i : ι) → Set (β i)} (hs : ∀ i ∈ S, MeasurableSet (s i))
    (h₀ :
      ∏ x ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) =
          HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
            (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ) ∧
        (μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) =
          HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
            (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    iIndepFun (β := β) f μ

Tactic:
classical
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
    constructor
    · congr with x
      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
      congr with x
      simp
  intro h S s hs
  specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
    fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
  simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
    Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
    Measure.pi_pi] at h₀
  rw [h₀.2, ← h₀.1]

Premises used: ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul, Set.inter_univ, Set.iInter_univ, Finset.filter_univ_mem, apply_ite, MeasureTheory.IsProbabilityMeasure.measure_univ, Finset.prod_ite, Finset.prod_ite_mem, Set.preimage_univ, Finset.univ_inter, MeasureTheory.Measure.pi_pi, Set.iInter_ite