-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α]
    [MeasurableSpace β] [Fintype γ] (μ : γ → Measure α) (ν : γ → Measure β) [∀ i, SigmaFinite (μ i)]
    [∀ i, SigmaFinite (ν i)] :
    MeasurePreserving (MeasurableEquiv.arrowProdEquivProdArrow α β γ)
      (.pi fun i ↦ (μ i).prod (ν i))
        ((Measure.pi fun i ↦ μ i).prod (Measure.pi fun i ↦ ν i)) where
  measurable := (MeasurableEquiv.arrowProdEquivProdArrow α β γ).measurable
  map_eq

Proof state:
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i => (μ i).prod (ν i)) =
    (Measure.pi fun i => μ i).prod (Measure.pi fun i => ν i)

Tactic:
refine (FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
  ((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
  (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn))) ?_).symm

Result:
case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ Prod.instMeasurableSpace =
    generateFrom
      (image2 (fun x1 x2 => x1 ×ˢ x2) (univ.pi '' univ.pi fun i => {s | MeasurableSet s})
        (univ.pi '' univ.pi fun i => {s | MeasurableSet s}))

case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ ∀
    s ∈
      image2 (fun x1 x2 => x1 ×ˢ x2) (univ.pi '' univ.pi fun i => {s | MeasurableSet s})
        (univ.pi '' univ.pi fun i => {s | MeasurableSet s}),
    ((Measure.pi μ).prod (Measure.pi ν)) s =
      (Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i => (μ i).prod (ν i))) s

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i => {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i => {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 => x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i => (μ i).prod (ν i))
      (⇑(Equiv.arrowProdEquivProdArrow γ (fun a => α) fun a => β) ⁻¹' (fun x1 x2 => x1 ×ˢ x2) (univ.pi s) (univ.pi t))

Tactic:
rw [show Equiv.arrowProdEquivProdArrow γ _ _ ⁻¹' (univ.pi s ×ˢ univ.pi t) =
    (univ.pi fun i ↦ s i ×ˢ t i) by
    ext; simp [Set.mem_pi, forall_and]]

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i => {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i => {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 => x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i => (μ i).prod (ν i)) (univ.pi fun i => s i ×ˢ t i)

Proof state:
case refine_1.refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (univ.pi '' univ.pi fun i => {s | MeasurableSet s})

Tactic:
exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning

Result:
no goals

Proof state:
case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ ∀
    s ∈
      image2 (fun x1 x2 => x1 ×ˢ x2) (univ.pi '' univ.pi fun i => {s | MeasurableSet s})
        (univ.pi '' univ.pi fun i => {s | MeasurableSet s}),
    ((Measure.pi μ).prod (Measure.pi ν)) s =
      (Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i => (μ i).prod (ν i))) s

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

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i => {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i => {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 => x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i => (μ i).prod (ν i)))
      ((fun x1 x2 => x1 ×ˢ x2) (univ.pi s) (univ.pi t))

Proof state:
case h
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i => {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i => {s | MeasurableSet s}
x✝ : γ → α × β
⊢ x✝ ∈ ⇑(Equiv.arrowProdEquivProdArrow γ (fun i => α) fun i => β) ⁻¹' univ.pi s ×ˢ univ.pi t ↔
    x✝ ∈ univ.pi fun i => s i ×ˢ t i

Tactic:
simp [Set.mem_pi, forall_and]

Result:
no goals

Proof state:
case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ Prod.instMeasurableSpace =
    generateFrom
      (image2 (fun x1 x2 => x1 ×ˢ x2) (univ.pi '' univ.pi fun i => {s | MeasurableSet s})
        (univ.pi '' univ.pi fun i => {s | MeasurableSet s}))

Tactic:
refine (generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm

Result:
case refine_1.refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (univ.pi '' univ.pi fun i => {s | MeasurableSet s})

case refine_1.refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (univ.pi '' univ.pi fun i => {s | MeasurableSet s})