awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) =
  (μ : (a : Set α) → ℝ≥0∞) s
Tactic: rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
Tactic: rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
have pos : ∀ (hX : AEMeasurable X μ), Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 μ)
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
have neg : ∀ (hX : ¬AEMeasurable X μ), Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 μ
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
have 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∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × γ) (fun (x : α) ↦ (X x, Y x)) (Prod.fst ⁻¹' s)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (X x, Y x)) ⁻¹' SProd.sprod (β := Set γ) s univ) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s ∩ Y ⁻¹' univ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s ∩ univ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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)) μ
have contrapose : ∀ (hX : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ), AEMeasurable X μ
Tactic: contrapose hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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 μ
⊢ Eq (α := Measure β) (fst.{u_2, u_3} (β := γ) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map X μ)
have this : ¬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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((map Prod.snd ρ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
Tactic: rw [snd, Measure.map_apply measurable_snd hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
  ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
Tactic: rw [snd, Measure.map_apply measurable_snd hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
⊢ Eq (α := ℝ≥0∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' univ) : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [snd_apply MeasurableSet.univ, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [snd_apply MeasurableSet.univ, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞) ((ρ.snd : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [snd_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 ρ
⊢ IsZeroOrProbabilityMeasure ρ.snd
have inl : ∀ (h : ρ = 0), IsZeroOrProbabilityMeasure ρ.snd
Tactic: rcases eq_zero_or_isProbabilityMeasure ρ with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ IsZeroOrProbabilityMeasure ρ.snd
have inr : ∀ (h : IsProbabilityMeasure ρ), IsZeroOrProbabilityMeasure ρ.snd
Tactic: rcases eq_zero_or_isProbabilityMeasure ρ with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 ρ.snd
have inl : IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := inst_1) 0
Tactic: simp only [h, snd_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure μ
⊢ (μ.prod ν).snd = ν
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ s) : ℝ≥0∞)
  ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
  (ν : (a : Set β) → ℝ≥0∞) s
Tactic: rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) = (ν : (a : Set β) → ℝ≥0∞) s
Tactic: rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₄ : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
have pos : ∀ (hY : AEMeasurable Y μ), Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
Tactic: by_cases hY : AEMeasurable Y μ