awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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
⊢ 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
have 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
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
have _ : μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) : ℝ≥0∞)
Tactic: 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
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
have _₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), g i) : ℝ≥0∞)
Tactic: 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
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 μ
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
have intro : ∀ (val : Fintype ι),
  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
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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)
⊢ iIndepFun (β := fun (x : ι) ↦ α) X μ[|⋂ (i : ι), Y i ⁻¹' t i]
have 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∞)
Tactic: rw [iIndepFun_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞)
have h : ∀ (i : ι) (hi : i ∈ s), Eq (α := ℝ≥0∞) (μ[f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
Tactic: convert! cond_iInter hY hindep hf (fun i _ ↦ hy _) ht using 2 with i hi
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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
| f * g
have change : (fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)
Tactic: change (fun x ↦ x.1 * x.2) ∘ (fun ω ↦ (f ω, g ω))
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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
⊢ Eq (α := Measure M) (Measure.map (f * g) μ) (Measure.map f μ ∗ₘ Measure.map g μ)
have conv : Eq (α := Measure M) (Measure.map ((fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)) μ)
  (Measure.map f μ ∗ₘ Measure.map g μ)
Tactic: conv in f * g => change (fun x ↦ x.1 * x.2) ∘ (fun ω ↦ (f ω, g ω))
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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
⊢ Eq (α := Measure M) (Measure.map ((fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.map f μ ∗ₘ Measure.map g μ)
have 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 μ)
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 μ)
⊢ Eq (α := Measure M) (Measure.map ((fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.map f μ ∗ₘ Measure.map g μ)
have 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 μ)
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 μ)
⊢ Eq (α := Measure M) (Measure.map ((fun (x : M × M) ↦ x.1 * x.2) ∘ fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.map f μ ∗ₘ Measure.map g μ)
have 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 μ)))
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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
⊢ Eq (α := Measure M) (Measure.map (f * g) μ) (Measure.map f μ ∗ₘ Measure.map g μ)
have σf : SigmaFinite (m0 := inst_1) (Measure.map f μ)
Tactic: apply hfg.map_mul_eq_map_mconv_map₀' hf hg
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 μ)
⊢ Eq (α := Measure M) (Measure.map (f * g) μ) (Measure.map f μ ∗ₘ Measure.map g μ)
have σg : SigmaFinite (m0 := inst_1) (Measure.map g μ)
Tactic: apply hfg.map_mul_eq_map_mconv_map₀' hf hg
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
⊢ IndepSets {A} {s : Set Ω | MeasurableSet s} P
have 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∞)
Tactic: rw [IndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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
⊢ (P : (a : Set Ω) → ℝ≥0∞) (s ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)
have 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∞)
Tactic: rw [Set.mem_singleton_iff.1 hs]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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}
have h₁ : ∀ (x : Ω), x ∈ A ↔ x ∈ Set.preimage (β := ℝ) (A.indicator 1) {1}
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (hypothesis)
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
⊢ (P : (a : Set Ω) → ℝ≥0∞) (A ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)
have hA' : A = Set.preimage (β := ℝ) (A.indicator 1) {1}
Tactic: have hA' : A = A.indicator (1 : Ω → ℝ) ⁻¹' {1} := by ext; simp [Set.indicator]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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∞) (A ∩ X ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞)
have 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∞)
Tactic: rw [hA']
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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)
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
have 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))
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX)
    (aemeasurable_pi_lambda _ mY)]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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)
⊢ 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))
have refine : ∀ (f : (i : S) → E i →ᵇ ℝ) (g : (j : T) → F j →ᵇ ℝ),
  (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ (MeasurableSpace.pi (X := E)) (map (fun (c : Ω) (a : S) ↦ X a c) P) fun (x : (i : S) → E i) ↦
        ∏ i : S, (f i : (a : E i) → ℝ) (x i))
      (@integral _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
Tactic: refine eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_