awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Basic
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∞)
mp :
  ∀
    (h :
      ∀ (s : Set β) (t : Set β'),
        MeasurableSet s →
          MeasurableSet t →
            (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
                ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞))
    (s : Set β) (t : Set β') (hs : MeasurableSet s) (ht : MeasurableSet t),
    (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∞)
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) →
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))

Tactic:
refine fun h ↦ (Measure.prod_eq fun s t hs ht ↦ ?_).symm

Premises used: MeasureTheory.Measure.prod_eq, Eq.symm
-- Module: Mathlib.Probability.Independence.Basic
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 :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
mp :
  (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
mp₁ :
  (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
mp₂ mp₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
⊢ (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∞)

Tactic:
rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]

Premises used: And.right, And.left
-- Module: Mathlib.Probability.Independence.Basic
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∞)
mpr₃ 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∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)

Tactic:
rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]

Premises used: MeasureTheory.Measure.prod_prod, And.right, And.left
-- Module: Mathlib.Probability.Independence.Basic
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 μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
⊢ f ⟂ᵢ[μ] g ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))

Tactic:
apply indepFun_iff_map_prod_eq_prod_map_map' hf hg

Premises used: ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map'
-- Module: Mathlib.Probability.Independence.Basic
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 μ
⊢ SigmaFinite (m0 := mβ) (Measure.map f μ)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Independence.Basic
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 μ
⊢ SigmaFinite (m0 := mβ') (Measure.map g μ)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
x : MeasurableSpace β
x_1 : MeasurableSpace β'
hfg : f ⟂ᵢ[μ] g
⊢ g ⟂ᵢ[μ] f

Tactic:
hfg.symm

Premises used: ProbabilityTheory.Kernel.IndepFun.symm, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
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'

Tactic:
Kernel.IndepFun.congr' hfg ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.congr', ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
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'
refine_2 :
  ∀ᵐ (a : Unit) ∂Measure.dirac (),
    g =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω)] g'
⊢ f' ⟂ᵢ[μ] g'

Tactic:
refine Kernel.IndepFun.congr' hfg ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.congr'
-- Module: Mathlib.Probability.Independence.Basic
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'
⊢ ∀ᵐ (a : Unit) ∂Measure.dirac (),
    f =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω)] f'

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Basic
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'
⊢ ∀ᵐ (a : Unit) ∂Measure.dirac (),
    g =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω)] g'

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Basic
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
⊢ AEMeasurable (β := 𝓧) (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Basic
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
⊢ AEMeasurable (β := 𝓨) (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Basic
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
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 ν)))
⊢ (fun (ω : Ω × Ω') ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ Y ω.2

Tactic:
refine indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop) |>.2 ?_

Premises used: Iff.mpr, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.Independence.Basic
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 (Prod.map X Y) (μ.prod ν)) (Measure.prod (Measure.map X μ) (Measure.map Y ν))

Tactic:
Measure.map_prod_map μ ν mX mY |>.symm

Premises used: MeasureTheory.Measure.map_prod_map, Eq.symm
-- Module: Mathlib.Probability.Independence.Basic
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 μ)
h₁ : Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map 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 ν)))

Tactic:
convert! Measure.map_prod_map μ ν mX mY |>.symm

Premises used: MeasureTheory.Measure.map_prod_map, Eq.symm
-- Module: Mathlib.Probability.Independence.Basic
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 μ)
h₄ h₅ : Eq (α := Measure 𝓧) (Measure.map X μ) (Measure.map X μ)
⊢ Eq (α := Measure 𝓧) (Measure.map (fun (ω : Ω × Ω') ↦ X ω.1) (μ.prod ν)) (Measure.map X μ)

Tactic:
rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
      measure_univ, one_smul]

Premises used: MeasureTheory.Measure.map_fst_prod, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, Function.comp_def, MeasureTheory.Measure.map_map, measurable_fst
-- Module: Mathlib.Probability.Independence.Basic
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 ν)
h₄ h₅ : Eq (α := Measure 𝓨) (Measure.map Y ν) (Measure.map Y ν)
⊢ Eq (α := Measure 𝓨) (Measure.map (fun (ω : Ω × Ω') ↦ Y ω.2) (μ.prod ν)) (Measure.map Y ν)

Tactic:
rw [← Function.comp_def, ← Measure.map_map mY measurable_snd, Measure.map_snd_prod,
      measure_univ, one_smul]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, Function.comp_def, measurable_snd, MeasureTheory.Measure.map_map, MeasureTheory.Measure.map_snd_prod
-- Module: Mathlib.Probability.Independence.Basic
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 (ω : Ω × Ω') ↦ 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
-- Module: Mathlib.Probability.Independence.Basic
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

Tactic:
this.congr ?_ ?_

Premises used: ProbabilityTheory.IndepFun.congr
-- Module: Mathlib.Probability.Independence.Basic
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
refine_2 : (ae (μ.prod ν)).EventuallyEq (β := 𝓨) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2) fun (ω : Ω × Ω') ↦ Y ω.2
⊢ (fun (ω : Ω × Ω') ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ Y ω.2

Tactic:
refine this.congr ?_ ?_

Premises used: ProbabilityTheory.IndepFun.congr
-- Module: Mathlib.Probability.Independence.Basic
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.mk X mX ∘ Prod.fst =ᶠ[ae (μ.prod ν)] X ∘ Prod.fst
⊢ (ae (μ.prod ν)).EventuallyEq (β := 𝓧) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) fun (ω : Ω × Ω') ↦ X ω.1

Tactic:
rw [← Function.comp_def, ← Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Probability.Independence.Basic
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 ν)
refine_1₁ : AEMeasurable.mk X mX =ᶠ[ae (F := Measure Ω) (Measure.map Prod.fst (μ.prod ν))] X
⊢ AEMeasurable.mk X mX ∘ Prod.fst =ᶠ[ae (μ.prod ν)] X ∘ Prod.fst

Tactic:
apply ae_eq_comp

Premises used: MeasureTheory.ae_eq_comp
-- Module: Mathlib.Probability.Independence.Basic
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 Prod.fst (μ.prod ν)

Tactic:
measurable_fst.aemeasurable

Premises used: Measurable.aemeasurable, measurable_fst
-- Module: Mathlib.Probability.Independence.Basic
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 Prod.fst (μ.prod ν)

Tactic:
exact measurable_fst.aemeasurable

Premises used: Measurable.aemeasurable, measurable_fst
-- Module: Mathlib.Probability.Independence.Basic
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.mk X mX =ᶠ[ae μ] X
⊢ AEMeasurable.mk X mX =ᶠ[ae (F := Measure Ω) (Measure.map Prod.fst (μ.prod ν))] X

Tactic:
rw [measurePreserving_fst.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_fst
-- Module: Mathlib.Probability.Independence.Basic
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 μ] X

Tactic:
(AEMeasurable.ae_eq_mk mX).symm

Premises used: AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Basic
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 μ] X

Tactic:
exact (AEMeasurable.ae_eq_mk mX).symm

Premises used: AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Basic
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.mk Y mY ∘ Prod.snd =ᶠ[ae (μ.prod ν)] Y ∘ Prod.snd
⊢ (ae (μ.prod ν)).EventuallyEq (β := 𝓨) (fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2) fun (ω : Ω × Ω') ↦ Y ω.2

Tactic:
rw [← Function.comp_def, ← Function.comp_def]

Premises used: Function.comp_def