no goals
ι : Type u_2
ι' : Type ?u.865740
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
h : (i : ι) → MeasurableSpace (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = h i
h2C : ∀ (i : ι), IsCountablySpanning (C i)
⊢ generateFrom (Set.pi univ '' Set.pi univ C) = MeasurableSpace.pi
rw [← funext hC, generateFrom_pi_eq h2C]