awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : α) ↦ f a0
funProp₂ : map (fun (a : α × β) ↦ a.1) (μ.prod ν) ≪ μ
funProp₃ : inst_1 ≤ inst_1
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : β) ↦ g a0
funProp₅ : map (fun (a : α × β) ↦ a.2) (μ.prod ν) ≪ ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
rw : ∫⁻ (x : α), ∫⁻ (y : β), f (x, y).1 * g (x, y).2 ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
⊢ ∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
rw [lintegral_prod _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y).1 * g (x, y).2 ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
simp [lintegral_lintegral_mul hf hg]

Premises used: MeasureTheory.lintegral_lintegral_mul
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((map Prod.fst ρ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [fst, Measure.map_apply measurable_fst hs]

Premises used: MeasureTheory.Measure.map_apply, measurable_fst, MeasureTheory.Measure.fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
rw :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' univ) : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [fst_apply MeasurableSet.univ, preimage_univ]

Premises used: MeasureTheory.Measure.fst_apply, Set.preimage_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Eq.{u_1 + 1} (α := Measure α) (fst.{u_1, u_2} (β := β) 0) 0

Tactic:
simp [fst]

Premises used: MeasureTheory.Measure.fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : SFinite ρ
⊢ SFinite (m0 := inst) (map Prod.fst ρ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsFiniteMeasure ρ
⊢ IsFiniteMeasure (m0 := inst) (map Prod.fst ρ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsProbabilityMeasure ρ
rw : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [fst_univ]

Premises used: MeasureTheory.Measure.fst_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsProbabilityMeasure ρ
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsProbabilityMeasure ρ
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
exact measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
inl : ∀ (h : ρ = 0), IsZeroOrProbabilityMeasure ρ.fst
inr : ∀ (h : IsProbabilityMeasure ρ), IsZeroOrProbabilityMeasure ρ.fst
⊢ IsZeroOrProbabilityMeasure ρ.fst

Tactic:
rcases eq_zero_or_isProbabilityMeasure ρ with h | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
inl : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := inst) 0
⊢ IsZeroOrProbabilityMeasure ρ.fst

Tactic:
simp only [h, fst_zero]

Premises used: MeasureTheory.Measure.fst_zero
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
⊢ IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := inst) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
h : IsProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.fst

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ.prod ν).fst = μ

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s
h₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
h₄ h₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]

Premises used: Set.prod_univ, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.fst_apply, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
pos :
  ∀ (hX : AEMeasurable X μ), Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
neg :
  ∀ (hX : ¬AEMeasurable X μ), Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)

Tactic:
by_cases hX : AEMeasurable X μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
pos :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((map X μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
s : Set β
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞) ((map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    (((map X μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × γ) (fun (x : α) ↦ (X x, Y x)) (Prod.fst ⁻¹' s)) : ℝ≥0∞)
    (((map X μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
pos₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × γ) (fun (x : α) ↦ (X x, Y x)) (Prod.fst ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
pos₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (X x, Y x)) ⁻¹' SProd.sprod (β := Set γ) s univ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
pos₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s ∩ Y ⁻¹' univ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
pos₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s ∩ univ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
pos₆ pos₇ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((map X μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.fst_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_fst hs),
      Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ,
      inter_univ]

Premises used: Set.inter_univ, Set.prod_univ, MeasureTheory.Measure.fst_apply, AEMeasurable.prodMk, MeasureTheory.Measure.map_apply_of_aemeasurable, Set.preimage_univ, measurable_fst, Set.mk_preimage_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : ¬AEMeasurable X μ
contrapose : ∀ (hX : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ), AEMeasurable X μ
⊢ ¬AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ

Tactic:
contrapose hX
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ
⊢ AEMeasurable X μ

Tactic:
measurable_fst.comp_aemeasurable hX

Premises used: Measurable.comp_aemeasurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ
⊢ AEMeasurable X μ

Tactic:
exact measurable_fst.comp_aemeasurable hX

Premises used: Measurable.comp_aemeasurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ

Tactic:
have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
      contrapose hX
      exact measurable_fst.comp_aemeasurable hX
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : ¬AEMeasurable X μ
this : ¬AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)

Tactic:
simp [map_of_not_aemeasurable, hX, this]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : Measurable Y
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)

Tactic:
fst_map_prodMk₀ hY.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.fst_map_prodMk₀
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ ν : Measure (α × β)
⊢ (μ + ν).fst = μ.fst + ν.fst

Tactic:
Measure.map_add _ _ measurable_fst

Premises used: MeasureTheory.Measure.map_add, measurable_fst, MeasureTheory.Measure.fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
⊢ (sum μ).fst = sum fun (n : ι) ↦ (μ n).fst

Tactic:
Measure.map_sum measurable_fst.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_sum, measurable_fst, MeasureTheory.Measure.fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ μ : Measure (α × β)
h : ρ ≤ μ
⊢ ρ.fst ≤ μ.fst

Tactic:
map_mono h measurable_fst

Premises used: MeasureTheory.Measure.map_mono, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((map Prod.snd ρ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [snd, Measure.map_apply measurable_snd hs]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.snd, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
rw :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' univ) : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [snd_apply MeasurableSet.univ, preimage_univ]

Premises used: Set.preimage_univ, MeasureTheory.Measure.snd_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Eq.{u_2 + 1} (α := Measure β) (snd.{u_1, u_2} (α := α) 0) 0

Tactic:
simp [snd]

Premises used: MeasureTheory.Measure.snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : SFinite ρ
⊢ SFinite (m0 := inst_1) (map Prod.snd ρ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsFiniteMeasure ρ
⊢ IsFiniteMeasure (m0 := inst_1) (map Prod.snd ρ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsProbabilityMeasure ρ
rw : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [snd_univ]

Premises used: MeasureTheory.Measure.snd_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
inl : ∀ (h : ρ = 0), IsZeroOrProbabilityMeasure ρ.snd
inr : ∀ (h : IsProbabilityMeasure ρ), IsZeroOrProbabilityMeasure ρ.snd
⊢ IsZeroOrProbabilityMeasure ρ.snd

Tactic:
rcases eq_zero_or_isProbabilityMeasure ρ with h | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
inl : IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := inst_1) 0
⊢ IsZeroOrProbabilityMeasure ρ.snd

Tactic:
simp only [h, snd_zero]

Premises used: MeasureTheory.Measure.snd_zero
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := inst_1) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
h : IsProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.snd

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure μ
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ.prod ν).snd = ν

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
    (ν : (a : Set β) → ℝ≥0∞) s
h₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) = (ν : (a : Set β) → ℝ≥0∞) s
h₄ h₅ : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]

Premises used: Set.univ_prod, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.snd_apply, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
pos :
  ∀ (hY : AEMeasurable Y μ), Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
neg :
  ∀ (hY : ¬AEMeasurable Y μ), Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)

Tactic:
by_cases hY : AEMeasurable Y μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
pos :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)

Tactic:
ext1 s hs