awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
h :
  Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.prod (Measure.map f μ) (Measure.map g μ))
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
mpr :
  (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
mpr₁ :
  (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
mpr₂ :
  (Measure.prod (Measure.map f μ) (Measure.map g μ) : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
have mpr₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ f ⟂ᵢ[μ] g ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
have σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
Tactic: apply indepFun_iff_map_prod_eq_prod_map_map' hf hg
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
⊢ f ⟂ᵢ[μ] g ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
have σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
Tactic: apply indepFun_iff_map_prod_eq_prod_map_map' hf hg
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : f ⟂ᵢ[μ] g
hf : f =ᶠ[ae μ] f'
hg : g =ᶠ[ae μ] g'
⊢ f' ⟂ᵢ[μ] g'
have refine_1 : ∀ᵐ (a : Unit) ∂Measure.dirac (),
  f =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω)] f'
Tactic: refine Kernel.IndepFun.congr' hfg ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : f ⟂ᵢ[μ] g
hf : f =ᶠ[ae μ] f'
hg : g =ᶠ[ae μ] g'
refine_1 :
  ∀ᵐ (a : Unit) ∂Measure.dirac (),
    f =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω)] f'
⊢ f' ⟂ᵢ[μ] g'
have refine_2 : ∀ᵐ (a : Unit) ∂Measure.dirac (),
  g =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω)] g'
Tactic: refine Kernel.IndepFun.congr' hfg ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ (fun (ω : Ω × Ω') ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ Y ω.2
have refine : Eq (α := Measure (𝓧 × 𝓨)) (Measure.map (fun (ω : Ω × Ω') ↦ (X ω.1, Y ω.2)) (μ.prod ν))
  (Measure.prod (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)))
Tactic: refine indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop) |>.2 ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Eq (α := Measure (𝓧 × 𝓨)) (Measure.map (fun (ω : Ω × Ω') ↦ (X ω.1, Y ω.2)) (μ.prod ν))
    (Measure.prod (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν))
      (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)))
have h : Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)
Tactic: convert! Measure.map_prod_map μ ν mX mY |>.symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)
⊢ Eq (α := Measure (𝓧 × 𝓨)) (Measure.map (fun (ω : Ω × Ω') ↦ (X ω.1, Y ω.2)) (μ.prod ν))
    (Measure.prod (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν))
      (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)))
have h₁ : Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map Y ν)
Tactic: convert! Measure.map_prod_map μ ν mX mY |>.symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)
have h : Eq (α := Measure 𝓧) (Measure.map (X ∘ Prod.fst) (μ.prod ν)) (Measure.map X μ)
Tactic: rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓧) (Measure.map (X ∘ Prod.fst) (μ.prod ν)) (Measure.map X μ)
⊢ Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)
have h₁ : Eq (α := Measure 𝓧) (Measure.map X (Measure.map Prod.fst (μ.prod ν))) (Measure.map X μ)
Tactic: rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓧) (Measure.map (X ∘ Prod.fst) (μ.prod ν)) (Measure.map X μ)
h₁ : Eq (α := Measure 𝓧) (Measure.map X (Measure.map Prod.fst (μ.prod ν))) (Measure.map X μ)
⊢ Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)
have h₂ : Eq (α := Measure 𝓧) (Measure.map X (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞) μ))
  (Measure.map X μ)
Tactic: rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓧) (Measure.map (X ∘ Prod.fst) (μ.prod ν)) (Measure.map X μ)
h₁ : Eq (α := Measure 𝓧) (Measure.map X (Measure.map Prod.fst (μ.prod ν))) (Measure.map X μ)
h₂ :
  Eq (α := Measure 𝓧) (Measure.map X (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞) μ))
    (Measure.map X μ)
⊢ Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)
have h₃ : Eq (α := Measure 𝓧) (Measure.map X (HSMul.hSMul (α := ℝ≥0∞) 1 μ)) (Measure.map X μ)
Tactic: rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓧) (Measure.map (X ∘ Prod.fst) (μ.prod ν)) (Measure.map X μ)
h₁ : Eq (α := Measure 𝓧) (Measure.map X (Measure.map Prod.fst (μ.prod ν))) (Measure.map X μ)
h₂ :
  Eq (α := Measure 𝓧) (Measure.map X (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞) μ))
    (Measure.map X μ)
h₃ : Eq (α := Measure 𝓧) (Measure.map X (HSMul.hSMul (α := ℝ≥0∞) 1 μ)) (Measure.map X μ)
⊢ Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)
have h₄ : Eq (α := Measure 𝓧) (Measure.map X μ) (Measure.map X μ)
Tactic: rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map Y ν)
have h : Eq (α := Measure 𝓨) (Measure.map (Y ∘ Prod.snd) (μ.prod ν)) (Measure.map Y ν)
Tactic: rw [← Function.comp_def, ← Measure.map_map mY measurable_snd, Measure.map_snd_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓨) (Measure.map (Y ∘ Prod.snd) (μ.prod ν)) (Measure.map Y ν)
⊢ Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map Y ν)
have h₁ : Eq (α := Measure 𝓨) (Measure.map Y (Measure.map Prod.snd (μ.prod ν))) (Measure.map Y ν)
Tactic: rw [← Function.comp_def, ← Measure.map_map mY measurable_snd, Measure.map_snd_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓨) (Measure.map (Y ∘ Prod.snd) (μ.prod ν)) (Measure.map Y ν)
h₁ : Eq (α := Measure 𝓨) (Measure.map Y (Measure.map Prod.snd (μ.prod ν))) (Measure.map Y ν)
⊢ Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map Y ν)
have h₂ : Eq (α := Measure 𝓨) (Measure.map Y (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ν)) (Measure.map Y ν)
Tactic: rw [← Function.comp_def, ← Measure.map_map mY measurable_snd, Measure.map_snd_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓨) (Measure.map (Y ∘ Prod.snd) (μ.prod ν)) (Measure.map Y ν)
h₁ : Eq (α := Measure 𝓨) (Measure.map Y (Measure.map Prod.snd (μ.prod ν))) (Measure.map Y ν)
h₂ :
  Eq (α := Measure 𝓨) (Measure.map Y (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ν))
    (Measure.map Y ν)
⊢ Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map Y ν)
have h₃ : Eq (α := Measure 𝓨) (Measure.map Y (HSMul.hSMul (α := ℝ≥0∞) 1 ν)) (Measure.map Y ν)
Tactic: rw [← Function.comp_def, ← Measure.map_map mY measurable_snd, Measure.map_snd_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
h : Eq (α := Measure 𝓨) (Measure.map (Y ∘ Prod.snd) (μ.prod ν)) (Measure.map Y ν)
h₁ : Eq (α := Measure 𝓨) (Measure.map Y (Measure.map Prod.snd (μ.prod ν))) (Measure.map Y ν)
h₂ :
  Eq (α := Measure 𝓨) (Measure.map Y (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ν))
    (Measure.map Y ν)
h₃ : Eq (α := Measure 𝓨) (Measure.map Y (HSMul.hSMul (α := ℝ≥0∞) 1 ν)) (Measure.map Y ν)
⊢ Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map Y ν)
have h₄ : Eq (α := Measure 𝓨) (Measure.map Y ν) (Measure.map Y ν)
Tactic: rw [← Function.comp_def, ← Measure.map_map mY measurable_snd, Measure.map_snd_prod,
      measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (hypothesis)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
⊢ (fun (ω : Ω × Ω') ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ Y ω.2
have this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
Tactic: have : (fun ω ↦ mX.mk X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ mY.mk Y ω.2) :=
    indepFun_prod mX.measurable_mk mY.measurable_mk
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ (fun (ω : Ω × Ω') ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ Y ω.2
have refine_1 : (ae (μ.prod ν)).EventuallyEq (β := 𝓧) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) fun (ω : Ω × Ω') ↦ X ω.1
Tactic: refine this.congr ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
refine_1 : (ae (μ.prod ν)).EventuallyEq (β := 𝓧) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) fun (ω : Ω × Ω') ↦ X ω.1
⊢ (fun (ω : Ω × Ω') ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ Y ω.2
have refine_2 : (ae (μ.prod ν)).EventuallyEq (β := 𝓨) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2) fun (ω : Ω × Ω') ↦ Y ω.2
Tactic: refine this.congr ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ (ae (μ.prod ν)).EventuallyEq (β := 𝓧) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) fun (ω : Ω × Ω') ↦ X ω.1
have refine_1 : AEMeasurable.mk X mX ∘ Prod.fst =ᶠ[ae (μ.prod ν)] X ∘ Prod.fst
Tactic: rw [← Function.comp_def, ← Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk X mX ∘ Prod.fst =ᶠ[ae (μ.prod ν)] X ∘ Prod.fst
have refine_1 : AEMeasurable Prod.fst (μ.prod ν)
Tactic: apply ae_eq_comp
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
refine_1 : AEMeasurable Prod.fst (μ.prod ν)
⊢ AEMeasurable.mk X mX ∘ Prod.fst =ᶠ[ae (μ.prod ν)] X ∘ Prod.fst
have refine_1₁ : AEMeasurable.mk X mX =ᶠ[ae (F := Measure Ω) (Measure.map Prod.fst (μ.prod ν))] X
Tactic: apply ae_eq_comp
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk X mX =ᶠ[ae (F := Measure Ω) (Measure.map Prod.fst (μ.prod ν))] X
have refine_1 : AEMeasurable.mk X mX =ᶠ[ae μ] X
Tactic: rw [measurePreserving_fst.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ (ae (μ.prod ν)).EventuallyEq (β := 𝓨) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2) fun (ω : Ω × Ω') ↦ Y ω.2
have refine_2 : AEMeasurable.mk Y mY ∘ Prod.snd =ᶠ[ae (μ.prod ν)] Y ∘ Prod.snd
Tactic: rw [← Function.comp_def, ← Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY ∘ Prod.snd =ᶠ[ae (μ.prod ν)] Y ∘ Prod.snd
have refine_2 : AEMeasurable Prod.snd (μ.prod ν)
Tactic: apply ae_eq_comp
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
refine_2 : AEMeasurable Prod.snd (μ.prod ν)
⊢ AEMeasurable.mk Y mY ∘ Prod.snd =ᶠ[ae (μ.prod ν)] Y ∘ Prod.snd
have refine_2₁ : AEMeasurable.mk Y mY =ᶠ[ae (F := Measure Ω') (Measure.map Prod.snd (μ.prod ν))] Y
Tactic: apply ae_eq_comp
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY =ᶠ[ae (F := Measure Ω') (Measure.map Prod.snd (μ.prod ν))] Y
have refine_2 : AEMeasurable.mk Y mY =ᶠ[ae ν] Y
Tactic: rw [measurePreserving_snd.map_eq]