awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (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 μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
x : Ω
⊢ Membership.mem (γ := Set Ω) (⋂ (i : ι), f i ⁻¹' s i) x ↔
    Membership.mem (γ := Set Ω) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) x

Tactic:
simp
-- 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 :
  ∀ (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 μ
⊢ ∀ {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∞)

Tactic:
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
-- 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 :
  ∀ (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) μ)

Tactic:
(Measure.pi_eq fun h' hm ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- 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 :
  ∀ (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∞)
refine :
  ∀ (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∞)
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)

Tactic:
refine (Measure.pi_eq fun h' hm ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- 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 :
  ∀ (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)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' h' i) : ℝ≥0∞)
    (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' h' i) : ℝ≥0∞)
⊢ 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∞)

Tactic:
rw [← (h₀ hm).1, ← (h₀ hm).2]

Premises used: And.right, And.left
-- 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 :
  ∀ (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∞)

Tactic:
simpa [hm] using h Finset.univ (sets := h')

Premises used: Finset.univ
-- 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) μ
⊢ iIndepFun (β := β) f μ ↔
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)

Tactic:
⟨iIndepFun.map_fun_eq_pi_map hf, ?_⟩

Premises used: Iff.intro, ProbabilityTheory.iIndepFun.map_fun_eq_pi_map
-- 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) μ
refine :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    iIndepFun (β := β) f μ
⊢ iIndepFun (β := β) f μ ↔
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)

Tactic:
refine ⟨iIndepFun.map_fun_eq_pi_map hf, ?_⟩
-- 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 :
  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∞)
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    iIndepFun (β := β) f μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul]

Premises used: ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul
-- 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) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
left :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))
right :
  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 (α := ℝ≥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∞)

Tactic:
constructor
-- 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) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
left :
  ∀ (x : ι),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
      (((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))

Tactic:
congr with x
-- 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) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
x : ι
left left₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
    (((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x) : ℝ≥0∞)

Tactic:
rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- 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) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
right :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) : ℝ≥0∞)
⊢ 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∞)

Tactic:
rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]

Premises used: aemeasurable_pi_lambda, MeasureTheory.Measure.map_apply_of_aemeasurable, MeasurableSet.univ_pi
-- 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) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
right :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) (⋂ (i : ι), f i ⁻¹' s i) x ↔
      Membership.mem (γ := Set Ω) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) : ℝ≥0∞)

Tactic:
congr with x
-- 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) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
x : Ω
⊢ Membership.mem (γ := Set Ω) (⋂ (i : ι), f i ⁻¹' s i) x ↔
    Membership.mem (γ := Set Ω) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) x

Tactic:
simp
-- 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) μ
⊢ ∀ {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∞)

Tactic:
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
-- 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) μ
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)
i : ι
pos : ∀ (hiS : i ∈ S), MeasurableSet (s i)
neg : ∀ (hiS : i ∉ S), MeasurableSet.{u_11} (α := β i) univ
⊢ MeasurableSet (if i ∈ S then s i else univ)

Tactic:
split_ifs with hiS
-- 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) μ
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)
i : ι
hiS : i ∈ S
⊢ MeasurableSet (s i)

Tactic:
simp [hiS, hs]
-- 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) μ
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)
i : ι
hiS : i ∉ S
⊢ MeasurableSet.{u_11} (α := β i) univ

Tactic:
simp [hiS, hs]
-- 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) μ
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∞) (∏ 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∞)

Tactic:
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]
-- 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) μ
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∞)
⊢ ∏ 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)

Tactic:
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₀

Premises used: 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
-- 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) μ
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)
rw :
  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) =
    ∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∏ x ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x)) (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
    (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)

Tactic:
rw [h₀.2, ← h₀.1]

Premises used: And.right, And.left