awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ Eq (α := ℝ≥0∞)
    (∏ i : ι,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞))
    (∏ i : ι, if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1)

Tactic:
Finset.prod_congr rfl fun i _ ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
refine :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
        if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1
⊢ Eq (α := ℝ≥0∞)
    (∏ i : ι,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞))
    (∏ i : ι, if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1)

Tactic:
refine Finset.prod_congr rfl fun i _ ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
pos :
  ∀ (hi : i ∈ s),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
      if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1
neg :
  ∀ (hi : i ∉ s),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
      if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
    if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∈ s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
    if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1

Tactic:
simp only [hi, ↓reduceIte, g, cond_apply (hY i (ht i))]

Premises used: ProbabilityTheory.cond_apply, reduceIte
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∉ s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
    if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1

Tactic:
simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top μ _)]

Premises used: MeasureTheory.measure_ne_top, reduceIte, ENNReal.inv_mul_cancel
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i])

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
intro intro₁ :
  ∀ (val : Fintype ι),
    Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)

Tactic:
classical
  cases nonempty_fintype ι
  let g (i' : ι) := if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
  calc
    _ = (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) := by
      rw [cond_apply]; exact .iInter fun i ↦ hY i (ht i)
    _ = (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) := by
      congr
      calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          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, μ (Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) := by
      rw [hindep.meas_iInter]
      exact fun i ↦ ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
    _ = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * ∏ i, μ (g i) := by
      rw [hindep.meas_iInter]
      intro i
      by_cases hi : i ∈ s <;> simp only [hi, ↓reduceIte, g]
      · obtain ⟨A, hA, hA'⟩ := hf i hi
        exact .inter ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
          ⟨A ×ˢ Set.univ, hA.prod .univ, by ext; simp [← hA']⟩
      · exact ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
    _ = ∏ i, (μ (Y i ⁻¹' t i))⁻¹ * μ (g i) := by
      rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _
    _ = ∏ i, if i ∈ s then μ[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: Finset.univ, Set.iInter, Finset.prod, Inter.inter, nonempty_fintype, Set.preimage, DFunLike.coe
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
rw :
  ∀ (s : Finset ι) {f' : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f' i)),
    Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f' i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f' i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞)
⊢ iIndepFun (β := fun (x : ι) ↦ α) X μ[|⋂ (i : ι), Y i ⁻¹' t i]

Tactic:
rw [iIndepFun_iff]

Premises used: ProbabilityTheory.iIndepFun_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)

Tactic:
cond_iInter hY hindep hf (fun i _ ↦ hy _) ht

Premises used: ProbabilityTheory.cond_iInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
h : ∀ (i : ι) (hi : i ∈ s), Eq (α := ℝ≥0∞) (μ[f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞)

Tactic:
convert! cond_iInter hY hindep hf (fun i _ ↦ hy _) ht using 2 with i hi

Premises used: ProbabilityTheory.cond_iInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
i : ι
hi : i ∈ s
⊢ Eq (α := ℝ≥0∞) (μ[f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)

Tactic:
simpa using cond_iInter hY hindep (fun j hj ↦ hf _ <| Finset.mem_singleton.1 hj ▸ hi)
    (fun i _ ↦ hy _) ht

Premises used: Finset.mem_singleton, Eq.rec, ProbabilityTheory.cond_iInter, Iff.mp, Eq.symm
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := inst_1) (Measure.map f μ)
σg : SigmaFinite (m0 := inst_1) (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
change : (fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)
| f * g

Tactic:
change (fun x ↦ x.1 * x.2) ∘ (fun ω ↦ (f ω, g ω))

Premises used: HMul.hMul, Prod.mk
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := inst_1) (Measure.map f μ)
σg : SigmaFinite (m0 := inst_1) (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
conv :
  Eq (α := Measure M) (Measure.map ((fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.map f μ ∗ₘ Measure.map g μ)
⊢ Eq (α := Measure M) (Measure.map (f * g) μ) (Measure.map f μ ∗ₘ Measure.map g μ)

Tactic:
conv in f * g => change (fun x ↦ x.1 * x.2) ∘ (fun ω ↦ (f ω, g ω))

Premises used: HMul.hMul, Prod.mk
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := inst_1) (Measure.map f μ)
σg : SigmaFinite (m0 := inst_1) (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
rw :
  Eq (α := Measure M) (Measure.map (fun (p : M × M) ↦ p.1 * p.2) (Measure.map (fun (x : Ω) ↦ (f x, g x)) μ))
    (Measure.map f μ ∗ₘ Measure.map g μ)
rw₁ :
  Eq (α := Measure M) (Measure.map (fun (p : M × M) ↦ p.1 * p.2) (Measure.prod (Measure.map f μ) (Measure.map g μ)))
    (Measure.map f μ ∗ₘ Measure.map g μ)
rw₂ rw₃ :
  Eq (α := Measure M) (Measure.map (fun (p : M × M) ↦ p.1 * p.2) (Measure.prod (Measure.map f μ) (Measure.map g μ)))
    (Measure.map (fun (x : M × M) ↦ x.1 * x.2) (Measure.prod (Measure.map f μ) (Measure.map g μ)))
⊢ Eq (α := Measure M) (Measure.map ((fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.map f μ ∗ₘ Measure.map g μ)

Tactic:
rw [← measurable_mul.aemeasurable.map_map_of_aemeasurable (hf.prodMk hg),
    (indepFun_iff_map_prod_eq_prod_map_map' hf hg σf σg).mp hfg, Measure.mconv]

Premises used: Measurable.aemeasurable, MeasurableMul₂.measurable_mul, AEMeasurable.prodMk, Iff.mp, AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map', MeasureTheory.Measure.mconv
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
f g : Ω → M
hf : Measurable f
hg : Measurable g
σf : SigmaFinite (m0 := inst_1) (Measure.map f μ)
σg : SigmaFinite (m0 := inst_1) (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
⊢ Eq (α := Measure M) (Measure.map (f * g) μ) (Measure.map f μ ∗ₘ Measure.map g μ)

Tactic:
hfg.map_mul_eq_map_mconv_map₀' hf.aemeasurable hg.aemeasurable σf σg

Premises used: Measurable.aemeasurable, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀'
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
inst_3 : IsFiniteMeasure μ
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : f ⟂ᵢ[μ] g
σf : SigmaFinite (m0 := inst_1) (Measure.map f μ)
σg : SigmaFinite (m0 := inst_1) (Measure.map g μ)
⊢ Eq (α := Measure M) (Measure.map (f * g) μ) (Measure.map f μ ∗ₘ Measure.map g μ)

Tactic:
apply hfg.map_mul_eq_map_mconv_map₀' hf hg

Premises used: ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀'
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
inst_3 : IsFiniteMeasure μ
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : f ⟂ᵢ[μ] g
⊢ SigmaFinite (m0 := inst_1) (Measure.map f μ)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
inst_3 : IsFiniteMeasure μ
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : f ⟂ᵢ[μ] g
⊢ SigmaFinite (m0 := inst_1) (Measure.map g μ)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
inst_3 : IsFiniteMeasure μ
f g : Ω → M
hf : Measurable f
hg : Measurable g
hfg : f ⟂ᵢ[μ] g
⊢ Eq (α := Measure M) (Measure.map (f * g) μ) (Measure.map f μ ∗ₘ Measure.map g μ)

Tactic:
hfg.map_mul_eq_map_mconv_map₀ hf.aemeasurable hg.aemeasurable

Premises used: ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀, Measurable.aemeasurable
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
rw :
  ∀ (t1 t2 : Set Ω),
    Membership.mem (γ := Set (Set Ω)) {A} t1 →
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2 →
        (P : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ IndepSets {A} {s : Set Ω | MeasurableSet s} P

Tactic:
rw [IndepSets_iff]

Premises used: ProbabilityTheory.IndepSets_iff
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {A} s
t : Set 𝓧
ht : MeasurableSet t
rw :
  (P : (a : Set Ω) → ℝ≥0∞) (A ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)
⊢ (P : (a : Set Ω) → ℝ≥0∞) (s ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)

Tactic:
rw [Set.mem_singleton_iff.1 hs]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {A} s
t : Set 𝓧
ht : MeasurableSet t
h₁ : ∀ (x : Ω), x ∈ A ↔ x ∈ Set.preimage (β := ℝ) (A.indicator 1) {1}
⊢ A = Set.preimage (β := ℝ) (A.indicator 1) {1}

Tactic:
ext
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {A} s
t : Set 𝓧
ht : MeasurableSet t
x : Ω
⊢ x ∈ A ↔ x ∈ Set.preimage (β := ℝ) (A.indicator 1) {1}

Tactic:
simp [Set.indicator]

Premises used: Set.indicator
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {A} s
t : Set 𝓧
ht : MeasurableSet t
⊢ A = Set.preimage (β := ℝ) (A.indicator 1) {1}

Tactic:
have hA' : A = A.indicator (1 : Ω → ℝ) ⁻¹' {1} := by ext; simp [Set.indicator]
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {A} s
t : Set 𝓧
ht : MeasurableSet t
hA' : A = Set.preimage (β := ℝ) (A.indicator 1) {1}
rw :
  (P : (a : Set Ω) → ℝ≥0∞) (Set.preimage (β := ℝ) (A.indicator 1) {1} ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (Set.preimage (β := ℝ) (A.indicator 1) {1}) : ℝ≥0∞)
      ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)
⊢ (P : (a : Set Ω) → ℝ≥0∞) (A ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)

Tactic:
rw [hA']
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {A} s
t : Set 𝓧
ht : MeasurableSet t
hA' : A = Set.preimage (β := ℝ) (A.indicator 1) {1}
⊢ MeasurableSet (α := ℝ) {1}

Tactic:
simp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {A} s
t : Set 𝓧
ht : MeasurableSet t
hA' : A = Set.preimage (β := ℝ) (A.indicator 1) {1}
⊢ (P : (a : Set Ω) → ℝ≥0∞) (Set.preimage (β := ℝ) (A.indicator 1) {1} ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (Set.preimage (β := ℝ) (A.indicator 1) {1}) : ℝ≥0∞)
      ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)

Tactic:
exact h.measure_inter_preimage_eq_mul _ _ (by simp) ht

Premises used: ProbabilityTheory.IndepFun.measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
rw :
  Eq (α := Measure (((a : S) → E a) × ((a : T) → F a)))
    (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
    (Measure.prod (map (fun (c : Ω) (a : S) ↦ X a c) P) (map (fun (c : Ω) (a : T) ↦ Y a c) P))
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX)
    (aemeasurable_pi_lambda _ mY)]

Premises used: aemeasurable_pi_lambda, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map