-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
have have₁ have₂ :
  ∀ (this : IsProbabilityMeasure μ),
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have₃ :
  ∀
    (h :
      ∀ (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∞))
    (this : IsProbabilityMeasure μ),
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have₄ :
  ∀
    (h :
      ∀ (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∞))
    (this : IsProbabilityMeasure μ)
    (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) μ)
have₅ :
  ∀
    (h :
      ∀ (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∞))
    (this : IsProbabilityMeasure μ)
    (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' : (i : ι) → Set (β i)) (hm : ∀ (i : ι), MeasurableSet (h' i)),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ h') :
        ℝ≥0∞)
      (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (h' i) : ℝ≥0∞)
have₆ :
  ∀
    (h :
      ∀ (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∞))
    (this : IsProbabilityMeasure μ)
    (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' : (i : ι) → Set (β i)) (hm : ∀ (i : ι), MeasurableSet (h' i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' h' i) : ℝ≥0∞)
      (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' h' i) : ℝ≥0∞)
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)

Tactic:
classical
  have := h.isProbabilityMeasure
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
  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
  refine (Measure.pi_eq fun h' hm ↦ ?_).symm
  rw [← (h₀ hm).1, ← (h₀ hm).2]
  simpa [hm] using h Finset.univ (sets := h')

Premises used: ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul, MeasureTheory.Measure.pi_eq, Eq.symm