-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem map_prod_map {δ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} (μa : Measure α)
    (μc : Measure γ) [SFinite μa] [SFinite μc] (hf : Measurable f) (hg : Measurable g) :
    (map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc)

Proof state:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (fun p => (map f (sfiniteSeq μa p.1)).prod (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

Result:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
⊢ (map f (sfiniteSeq μa i.1)).prod (map g (sfiniteSeq μc i.2)) =
    map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
⊢ (map f (sfiniteSeq μa i.1)).prod (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 => ?_

Result:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))) (s ×ˢ t) =
    (map f (sfiniteSeq μa i.1)) s * (map g (sfiniteSeq μc i.2)) t

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) (Prod.map f g ⁻¹' s ×ˢ t) =
    (sfiniteSeq μa i.1) (f ⁻¹' s) * (sfiniteSeq μc i.2) (g ⁻¹' t)

Tactic:
exact prod_prod (f ⁻¹' s) (g ⁻¹' t)

Result:
no goals

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))) (s ×ˢ t) =
    (map f (sfiniteSeq μa i.1)) s * (map g (sfiniteSeq μc i.2)) t

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

Result:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) (Prod.map f g ⁻¹' s ×ˢ t) =
    (sfiniteSeq μa i.1) (f ⁻¹' s) * (sfiniteSeq μc i.2) (g ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (sum fun p => (map f (sfiniteSeq μa p.1)).prod (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

Result:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (fun p => (map f (sfiniteSeq μa p.1)).prod (map g (sfiniteSeq μc p.2))) = fun i =>
    map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f μa).prod (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.prod_map hg).aemeasurable]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (sum fun p => (map f (sfiniteSeq μa p.1)).prod (map g (sfiniteSeq μc p.2))) =
    sum fun i => map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))