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 β
inst_2 : SFinite ν
x : α
e_f :
  Eq (α := ℕ → Measure (α × β)) (fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p)) fun (i : ℕ) ↦
    map (Prod.mk x) (sfiniteSeq ν i)
⊢ Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (sum fun (i : ℕ) ↦ map (Prod.mk x) (sfiniteSeq ν i))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
x : α
e_f : ∀ (i : ℕ), Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sfiniteSeq ν i)) (map (Prod.mk x) (sfiniteSeq ν i))
⊢ Eq (α := ℕ → Measure (α × β)) (fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p)) fun (i : ℕ) ↦
    map (Prod.mk x) (sfiniteSeq ν i)

Tactic:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
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))

Tactic:
prod_eq fun s t hs ht => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
x : α
i : ℕ
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∞)
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) (sfiniteSeq ν i)) (map (Prod.mk x) (sfiniteSeq ν i))

Tactic:
refine prod_eq fun s t hs ht => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
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)
⊢ (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:
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]

Premises used: MeasureTheory.Measure.map_apply, Pi.one_apply, MeasureTheory.Measure.dirac_apply', Set.mk_preimage_prod_right_eq_if, MeasurableSet.prod, MeasureTheory.measure_if, Set.indicator_mul_left, DFunLike.coe, one_mul, measurable_prodMk_left, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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))
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∞)
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)

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]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.prod_eq, Pi.one_apply, MeasureTheory.Measure.map_sum, Set.mk_preimage_prod_right_eq_if, MeasureTheory.sum_sfiniteSeq, MeasureTheory.measure_if, MeasureTheory.Measure.prod_sum_right, one_mul, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
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))
rw₁ rw₂ : Eq (α := Measure (α × β)) (dirac (x, y)) (dirac (x, y))
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) (dirac y)) (dirac (x, y))

Tactic:
rw [prod_dirac, map_dirac' measurable_prodMk_right]

Premises used: measurable_prodMk_right, MeasureTheory.Measure.map_dirac', MeasureTheory.Measure.prod_dirac
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
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))
⊢ μ.prod (ν + ν') = μ.prod ν + μ.prod ν'

Tactic:
simp_rw [← sum_sfiniteSeq ν, ← sum_sfiniteSeq ν', sum_add_sum, ← sum_sfiniteSeq μ, prod_sum,
    sum_add_sum]

Premises used: MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.sum_add_sum, MeasureTheory.Measure.prod_sum
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
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)
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
ν' : Measure β
inst_4 : SFinite ν'
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)
⊢ 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:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)

Tactic:
prod_eq fun s t _ _ => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : ℕ × ℕ
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∞)
⊢ (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:
refine prod_eq fun s t _ _ => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞))
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∞))
⊢ ((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:
simp_rw [add_apply, prod_prod, left_distrib]

Premises used: MeasureTheory.Measure.add_apply, MeasureTheory.Measure.prod_prod, left_distrib
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
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))
⊢ (μ + μ').prod ν = μ.prod ν + μ'.prod ν

Tactic:
simp_rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq μ', sum_add_sum, ← sum_sfiniteSeq ν, prod_sum,
    sum_add_sum]

Premises used: MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.sum_add_sum, MeasureTheory.Measure.prod_sum
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
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)
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
μ' : Measure α
inst_4 : SFinite μ'
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)
⊢ 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:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)

Tactic:
prod_eq fun s t _ _ => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : ℕ × ℕ
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∞)
⊢ (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:
refine prod_eq fun s t _ _ => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
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∞)
⊢ ((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:
simp_rw [add_apply, prod_prod, right_distrib]

Premises used: MeasureTheory.Measure.add_apply, MeasureTheory.Measure.prod_prod, right_distrib
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
rw : Eq (α := Measure (α × β)) (bind (mα := inst) 0 fun (x : α) ↦ map (Prod.mk x) ν) 0
⊢ Eq (α := Measure (α × β)) (Measure.prod 0 ν) 0

Tactic:
rw [Measure.prod]

Premises used: MeasureTheory.Measure.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
⊢ Eq (α := Measure (α × β)) (bind (mα := inst) 0 fun (x : α) ↦ map (Prod.mk x) ν) 0

Tactic:
bind_zero_left _

Premises used: MeasureTheory.Measure.bind_zero_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
⊢ Eq (α := Measure (α × β)) (bind (mα := inst) 0 fun (x : α) ↦ map (Prod.mk x) ν) 0

Tactic:
exact bind_zero_left _

Premises used: MeasureTheory.Measure.bind_zero_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
⊢ Eq (α := Measure (α × β)) (μ.prod 0) 0

Tactic:
simp [Measure.prod]

Premises used: MeasureTheory.Measure.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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)))
⊢ Eq (α := Measure (β × δ)) (Measure.prod (map f μa) (map g μc)) (map (Prod.map f g) (μa.prod μc))

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]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_sum, MeasureTheory.sum_sfiniteSeq, Measurable.prodMap, MeasureTheory.Measure.prod_sum
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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))
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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)))
⊢ 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:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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:
prod_eq fun s t hs ht => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
i : ℕ × ℕ
e_f :
  ∀ (s : Set β) (t : Set δ) (hs : MeasurableSet s) (ht : MeasurableSet t),
    (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map f (sfiniteSeq μa i.1) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((map g (sfiniteSeq μc i.2) : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ 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:
refine prod_eq fun s t hs ht => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2) : (a : Set (α × γ)) → ℝ≥0∞) (Prod.map f g ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μa i.1 : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((sfiniteSeq μc i.2 : (a : Set γ) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
⊢ (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map f (sfiniteSeq μa i.1) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((map g (sfiniteSeq μc i.2) : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [map_apply (hf.prodMap hg) (hs.prod ht), map_apply hf hs, map_apply hg ht]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.prod, Measurable.prodMap