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 β
inst_2 : SFinite ν
x : α
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) (if x ∈ s then t else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₂ :
  s.indicator (fun (x : α) ↦ (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t) x =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₃ :
  s.indicator (fun (x : α) ↦ (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t) x =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (s.indicator 1 x : ℝ≥0∞) ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₄ :
  Eq (α := ℝ≥0∞) (s.indicator (fun (x : α) ↦ (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t) x)
    (s.indicator
      (fun (j : α) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 j : ℝ≥0∞) ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)) x)
⊢ (map (Prod.mk x) (sfiniteSeq ν i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₅ : Eq (α := ℝ≥0∞) (s.indicator (fun (x : α) ↦ (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t) x)
  (s.indicator
    (fun (j : α) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)) x)
Tactic: simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, 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 β
inst_2 : SFinite ν
x : α
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)
have rw : Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sum (sfiniteSeq ν))) (map (Prod.mk x) (sum (sfiniteSeq ν)))
Tactic: classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, 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 β
inst_2 : SFinite ν
x : α
rw : Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sum (sfiniteSeq ν))) (map (Prod.mk x) (sum (sfiniteSeq ν)))
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)
have rw₁ : Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
  (map (Prod.mk x) (sum (sfiniteSeq ν)))
Tactic: classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, 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 β
inst_2 : SFinite ν
x : α
rw : Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sum (sfiniteSeq ν))) (map (Prod.mk x) (sum (sfiniteSeq ν)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (map (Prod.mk x) (sum (sfiniteSeq ν)))
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)
have rw₂ : Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
  (sum fun (i : ℕ) ↦ map (Prod.mk x) (sfiniteSeq ν i))
Tactic: classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, 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 β
inst_2 : SFinite ν
x : α
rw : Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sum (sfiniteSeq ν))) (map (Prod.mk x) (sum (sfiniteSeq ν)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (map (Prod.mk x) (sum (sfiniteSeq ν)))
rw₂ rw₃ rw₄ :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (sum fun (i : ℕ) ↦ map (Prod.mk x) (sfiniteSeq ν i))
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)
have e_f : Eq (α := ℕ → Measure (α × β)) (fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p)) fun (i : ℕ) ↦
  map (Prod.mk x) (sfiniteSeq ν i)
Tactic: classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, 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 β
inst_2 : SFinite ν
x : α
rw : Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sum (sfiniteSeq ν))) (map (Prod.mk x) (sum (sfiniteSeq ν)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (map (Prod.mk x) (sum (sfiniteSeq ν)))
rw₂ rw₃ rw₄ :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (sum fun (i : ℕ) ↦ map (Prod.mk x) (sfiniteSeq ν i))
e_f :
  Eq (α := ℕ → Measure (α × β)) (fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p)) fun (i : ℕ) ↦
    map (Prod.mk x) (sfiniteSeq ν i)
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)
have e_f₁ : ∀ (i : ℕ), Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sfiniteSeq ν i)) (map (Prod.mk x) (sfiniteSeq ν i))
Tactic: classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, 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 β
inst_2 : SFinite ν
x : α
rw : Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sum (sfiniteSeq ν))) (map (Prod.mk x) (sum (sfiniteSeq ν)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (map (Prod.mk x) (sum (sfiniteSeq ν)))
rw₂ rw₃ rw₄ :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (sum fun (i : ℕ) ↦ map (Prod.mk x) (sfiniteSeq ν i))
e_f :
  Eq (α := ℕ → Measure (α × β)) (fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p)) fun (i : ℕ) ↦
    map (Prod.mk x) (sfiniteSeq ν i)
e_f₁ : ∀ (i : ℕ), Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sfiniteSeq ν i)) (map (Prod.mk x) (sfiniteSeq ν i))
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)
have e_f₂ : ∀ (i : ℕ) (s : Set α) (t : Set β) (hs : MeasurableSet s) (ht : MeasurableSet t),
  (map (Prod.mk x) (sfiniteSeq ν i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
x : α
y : β
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) (dirac y)) (dirac (x, y))
have rw : Eq (α := Measure (α × β)) (map (fun (x : α) ↦ (x, y)) (dirac x)) (dirac (x, y))
Tactic: rw [prod_dirac, map_dirac' measurable_prodMk_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
x : α
y : β
rw : Eq (α := Measure (α × β)) (map (fun (x : α) ↦ (x, y)) (dirac x)) (dirac (x, y))
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) (dirac y)) (dirac (x, y))
have rw₁ : Eq (α := Measure (α × β)) (dirac (x, y)) (dirac (x, y))
Tactic: rw [prod_dirac, map_dirac' measurable_prodMk_right]
-- 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 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
⊢ μ.prod (ν + ν') = μ.prod ν + μ.prod ν'
have simp_rw : Eq (α := Measure (α × β)) (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2 + sfiniteSeq ν' p.2))
  (sum fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ n.1).prod (sfiniteSeq ν' n.2))
Tactic: simp_rw [← sum_sfiniteSeq ν, ← sum_sfiniteSeq ν', sum_add_sum, ← sum_sfiniteSeq μ, prod_sum,
    sum_add_sum]
-- 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 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
⊢ Eq (α := Measure (α × β)) (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2 + sfiniteSeq ν' p.2))
    (sum fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ n.1).prod (sfiniteSeq ν' n.2))
have e_f : Eq (α := ℕ × ℕ → Measure (α × β)) (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2 + sfiniteSeq ν' p.2))
  fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ n.1).prod (sfiniteSeq ν' n.2)
Tactic: congr
-- 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 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
⊢ Eq (α := ℕ × ℕ → Measure (α × β)) (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2 + sfiniteSeq ν' p.2))
    fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ n.1).prod (sfiniteSeq ν' n.2)
have e_f : ∀ (i : ℕ × ℕ),
  (sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2 + sfiniteSeq ν' i.2) =
    (sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2)
Tactic: ext1 i
-- 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 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
i : ℕ × ℕ
⊢ (sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2 + sfiniteSeq ν' i.2) =
    (sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2)
have e_f : ∀ (s : Set α) (t : Set β),
  MeasurableSet s →
    MeasurableSet t →
      ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2) :
            (a : Set (α × β)) → ℝ≥0∞)
          (s ×ˢ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
          ((sfiniteSeq ν i.2 + sfiniteSeq ν' i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine prod_eq fun s t _ _ => ?_
-- 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 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
i : ℕ × ℕ
s : Set α
t : Set β
h : MeasurableSet s
h_1 : MeasurableSet t
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2) : (a : Set (α × β)) → ℝ≥0∞)
      (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i.2 + sfiniteSeq ν' i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    (((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    (((sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
      ((sfiniteSeq ν' i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: simp_rw [add_apply, prod_prod, left_distrib]
-- 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 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
i : ℕ × ℕ
s : Set α
t : Set β
h : MeasurableSet s
h_1 : MeasurableSet t
e_f :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
      (((sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
        ((sfiniteSeq ν' i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞))
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2) : (a : Set (α × β)) → ℝ≥0∞)
      (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i.2 + sfiniteSeq ν' i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) +
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν' i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
      ((sfiniteSeq ν' i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: simp_rw [add_apply, prod_prod, left_distrib]
-- 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 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
⊢ (μ + μ').prod ν = μ.prod ν + μ'.prod ν
have simp_rw : Eq (α := Measure (α × β)) (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1 + sfiniteSeq μ' p.1).prod (sfiniteSeq ν p.2))
  (sum fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ' n.1).prod (sfiniteSeq ν n.2))
Tactic: simp_rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq μ', sum_add_sum, ← sum_sfiniteSeq ν, prod_sum,
    sum_add_sum]
-- 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 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
⊢ Eq (α := Measure (α × β)) (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1 + sfiniteSeq μ' p.1).prod (sfiniteSeq ν p.2))
    (sum fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ' n.1).prod (sfiniteSeq ν n.2))
have e_f : Eq (α := ℕ × ℕ → Measure (α × β)) (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1 + sfiniteSeq μ' p.1).prod (sfiniteSeq ν p.2))
  fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ' n.1).prod (sfiniteSeq ν n.2)
Tactic: congr
-- 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 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
⊢ Eq (α := ℕ × ℕ → Measure (α × β)) (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1 + sfiniteSeq μ' p.1).prod (sfiniteSeq ν p.2))
    fun (n : ℕ × ℕ) ↦ (sfiniteSeq μ n.1).prod (sfiniteSeq ν n.2) + (sfiniteSeq μ' n.1).prod (sfiniteSeq ν n.2)
have e_f : ∀ (i : ℕ × ℕ),
  (sfiniteSeq μ i.1 + sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2) =
    (sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2)
Tactic: ext1 i
-- 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 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
i : ℕ × ℕ
⊢ (sfiniteSeq μ i.1 + sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2) =
    (sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2)
have e_f : ∀ (s : Set α) (t : Set β),
  MeasurableSet s →
    MeasurableSet t →
      ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2) :
            (a : Set (α × β)) → ℝ≥0∞)
          (s ×ˢ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 + sfiniteSeq μ' i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
          ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine prod_eq fun s t _ _ => ?_
-- 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 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
i : ℕ × ℕ
s : Set α
t : Set β
h : MeasurableSet s
h_1 : MeasurableSet t
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞)
      (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 + sfiniteSeq μ' i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    (((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    (((sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ' i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [add_apply, prod_prod, right_distrib]
-- 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 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
i : ℕ × ℕ
s : Set α
t : Set β
h : MeasurableSet s
h_1 : MeasurableSet t
e_f :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
      (((sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((sfiniteSeq μ' i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞)
      (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 + sfiniteSeq μ' i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) +
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ' i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ' i.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [add_apply, prod_prod, right_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
⊢ Eq (α := Measure (α × β)) (Measure.prod 0 ν) 0
have rw : Eq (α := Measure (α × β)) (bind (mα := inst) 0 fun (x : α) ↦ map (Prod.mk x) ν) 0
Tactic: rw [Measure.prod]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst_4 : SFinite μa
inst_5 : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ Eq (α := Measure (β × δ)) (Measure.prod (map f μa) (map g μc)) (map (Prod.map f g) (μa.prod μc))
have simp_rw : Eq (α := Measure (β × δ)) (sum fun (p : ℕ × ℕ) ↦ Measure.prod (map f (sfiniteSeq μa p.1)) (map g (sfiniteSeq μc p.2)))
  (sum fun (i : ℕ × ℕ) ↦ map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)))
Tactic: simp_rw [← sum_sfiniteSeq μa, ← sum_sfiniteSeq μc, map_sum hf.aemeasurable,
    map_sum hg.aemeasurable, prod_sum, map_sum (hf.prodMap hg).aemeasurable]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst_4 : SFinite μa
inst_5 : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ Eq (α := Measure (β × δ)) (sum fun (p : ℕ × ℕ) ↦ Measure.prod (map f (sfiniteSeq μa p.1)) (map g (sfiniteSeq μc p.2)))
    (sum fun (i : ℕ × ℕ) ↦ map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)))
have e_f : Eq (α := ℕ × ℕ → Measure (β × δ))
  (fun (p : ℕ × ℕ) ↦ Measure.prod (map f (sfiniteSeq μa p.1)) (map g (sfiniteSeq μc p.2))) fun (i : ℕ × ℕ) ↦
  map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))
Tactic: congr
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst_4 : SFinite μa
inst_5 : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ Eq (α := ℕ × ℕ → Measure (β × δ))
    (fun (p : ℕ × ℕ) ↦ Measure.prod (map f (sfiniteSeq μa p.1)) (map g (sfiniteSeq μc p.2))) fun (i : ℕ × ℕ) ↦
    map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))
have e_f : ∀ (i : ℕ × ℕ),
  Eq (α := Measure (β × δ)) (Measure.prod (map f (sfiniteSeq μa i.1)) (map g (sfiniteSeq μc i.2)))
    (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)))
Tactic: ext1 i