-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_restrict (s : Set α) (t : Set β) :
    (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ (sum fun p => ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t)) =
    sum fun i => ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)

Tactic:
congr 1

Result:
case e_f
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ (fun p => ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t)) = fun i =>
    ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)

Tactic:
rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, restrict_sum_of_countable, restrict_sum_of_countable,
  prod_sum, prod_sum, restrict_sum_of_countable]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ (sum fun p => ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t)) =
    sum fun i => ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)

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

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

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

Proof state:
case e_f
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ (fun p => ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t)) = fun i =>
    ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)

Tactic:
ext1 i

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

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

Tactic:
rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
  restrict_apply ht']

Result:
no goals