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 μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) (if y ∈ t then s else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₂ : t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) (if y ∈ t then s else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₂ :
  t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₃ : t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (t.indicator 1 y : ℝ≥0∞)
Tactic: simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) (if y ∈ t then s else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₂ :
  t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₃ :
  t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (t.indicator 1 y : ℝ≥0∞)
⊢ (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₄ : Eq (α := ℝ≥0∞) (t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y)
  (t.indicator
    (fun (j : β) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 j : ℝ≥0∞)) y)
Tactic: simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) (if y ∈ t then s else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₂ :
  t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₃ :
  t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (t.indicator 1 y : ℝ≥0∞)
e_f₄ :
  Eq (α := ℝ≥0∞) (t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y)
    (t.indicator
      (fun (j : β) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 j : ℝ≥0∞)) y)
⊢ (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₅ : Eq (α := ℝ≥0∞) (t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y)
  (t.indicator
    (fun (j : β) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)) y)
Tactic: simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)
have rw : Eq (α := Measure (α × β)) ((sum (sfiniteSeq μ)).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
Tactic: classical
  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
rw : Eq (α := Measure (α × β)) ((sum (sfiniteSeq μ)).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)
have rw₁ : Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
  (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
Tactic: classical
  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
rw : Eq (α := Measure (α × β)) ((sum (sfiniteSeq μ)).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)
have rw₂ : Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
  (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
Tactic: classical
  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
rw : Eq (α := Measure (α × β)) ((sum (sfiniteSeq μ)).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₂ rw₃ rw₄ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)
have e_f : Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
  map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)
Tactic: classical
  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
rw : Eq (α := Measure (α × β)) ((sum (sfiniteSeq μ)).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₂ rw₃ rw₄ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
e_f :
  Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
    map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)
have e_f₁ : ∀ (i : ℕ), Eq (α := Measure (α × β)) ((sfiniteSeq μ i).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
Tactic: classical
  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 α
inst_2 : SFinite μ
y : β
rw : Eq (α := Measure (α × β)) ((sum (sfiniteSeq μ)).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₂ rw₃ rw₄ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
e_f :
  Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
    map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)
e_f₁ :
  ∀ (i : ℕ), Eq (α := Measure (α × β)) ((sfiniteSeq μ i).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)
have e_f₂ : ∀ (i : ℕ) (s : Set α) (t : Set β) (hs : MeasurableSet s) (ht : MeasurableSet t),
  (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: classical
  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, 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 β
inst_2 : SFinite ν
x : α
⊢ 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: rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
-- 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 (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (sum fun (i : ℕ) ↦ map (Prod.mk x) (sfiniteSeq ν i))
have e_f : Eq (α := ℕ → Measure (α × β)) (fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p)) fun (i : ℕ) ↦
  map (Prod.mk x) (sfiniteSeq ν i)
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 β
inst_2 : SFinite ν
x : α
⊢ Eq (α := ℕ → Measure (α × β)) (fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p)) fun (i : ℕ) ↦
    map (Prod.mk x) (sfiniteSeq ν i)
have e_f : ∀ (i : ℕ), Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sfiniteSeq ν i)) (map (Prod.mk x) (sfiniteSeq ν i))
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 β
inst_2 : SFinite ν
x : α
i : ℕ
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sfiniteSeq ν i)) (map (Prod.mk x) (sfiniteSeq ν i))
have e_f : ∀ (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: refine prod_eq fun s t hs ht => ?_
-- 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
⊢ (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 : (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∞)
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 : α
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∞)
⊢ (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₁ : (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∞)
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 : α
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∞)
⊢ (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₂ : 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∞)
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 : α
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∞)
⊢ (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₃ : 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∞)
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 : α
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∞)
⊢ (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 j : ℝ≥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]