-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_add (ν' : Measure β) [SFinite ν'] : μ.prod (ν + ν') = μ.prod ν + μ.prod ν'

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : 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:
refine prod_eq fun s t _ _ => ?_

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
i : ℕ × ℕ
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2)) (s ×ˢ t) =
    (sfiniteSeq μ i.1) s * (sfiniteSeq ν i.2 + sfiniteSeq ν' i.2) t

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ (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

Result:
case e_f
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ (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)

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
i : ℕ × ℕ
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2)) (s ×ˢ t) =
    (sfiniteSeq μ i.1) s * (sfiniteSeq ν i.2 + sfiniteSeq ν' i.2) t

Tactic:
simp_rw [add_apply, prod_prod, left_distrib]

Result:
no goals

Proof state:
case e_f
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ (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

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : 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)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ μ.prod (ν + ν') = μ.prod ν + μ.prod ν'

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

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ (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)