no goals
α : Type u_1
α' : Type ?u.808243
β : Type u_2
β' : Type ?u.808249
γ : Type ?u.808252
E : Type ?u.808255
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst✝⁵
hD : generateFrom D = inst✝³
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
⊢ generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D) = Prod.instMeasurableSpace
rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]