-- Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
theorem generateFrom_prod_eq {α β} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
    (hD : IsCountablySpanning D) :
    @Prod.instMeasurableSpace _ _ (generateFrom C) (generateFrom D) =
      generateFrom (image2 (· ×ˢ ·) C D)

Proof state:
case a.refine_1.h.intro.intro.intro.intro.h
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ ∀ (b : ℕ), MeasurableSet (s ×ˢ t b)

Tactic:
intro n

Result:
case a.refine_1.h.intro.intro.intro.intro.h
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
n : ℕ
⊢ MeasurableSet (s ×ˢ t n)

Proof state:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet t

Tactic:
exact measurableSet_generateFrom ht

Result:
no goals

Proof state:
case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) C D) ≤ Prod.instMeasurableSpace

Tactic:
apply generateFrom_le

Result:
case a.h
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ t ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D, MeasurableSet t

Proof state:
case a.h
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ t ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D, MeasurableSet t

Tactic:
rintro _ ⟨s, hs, t, ht, rfl⟩

Result:
case a.h.intro.intro.intro.intro
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet ((fun x1 x2 => x1 ×ˢ x2) s t)

Proof state:
case a.refine_2.h.intro.intro.intro.intro
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
rw [← univ_prod, ← h2t, iUnion_prod_const]

Result:
case a.refine_2.h.intro.intro.intro.intro
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (⋃ i, t i ×ˢ s)

Proof state:
case a.refine_2.h.intro.intro.intro.intro.h.ht
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
n : ℕ
⊢ t n ×ˢ s ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D

Tactic:
exact mem_image2_of_mem (h1t n) hs

Result:
no goals

Proof state:
case a.refine_1.h.intro.intro.intro.intro.h
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
n : ℕ
⊢ MeasurableSet (s ×ˢ t n)

Tactic:
apply measurableSet_generateFrom

Result:
case a.refine_1.h.intro.intro.intro.intro.h.ht
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
n : ℕ
⊢ s ×ˢ t n ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D