-- 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)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i => {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i => {s | MeasurableSet s}
⊢ ⇑(Equiv.arrowProdEquivProdArrow γ (fun i => α) fun i => β) ⁻¹' univ.pi s ×ˢ univ.pi t = univ.pi fun i => s i ×ˢ t i

Tactic:
ext

Result:
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

Proof state:
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})

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

Result:
no goals

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.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i => (μ i).prod (ν i)))
      ((fun x1 x2 => x1 ×ˢ x2) (univ.pi s) (univ.pi t))

Tactic:
rw [MeasurableEquiv.map_apply, MeasurableEquiv.arrowProdEquivProdArrow,
  MeasurableEquiv.coe_mk]

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))
      (⇑(Equiv.arrowProdEquivProdArrow γ (fun a => α) fun a => β) ⁻¹' (fun x1 x2 => x1 ×ˢ x2) (univ.pi s) (univ.pi t))

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)) (univ.pi fun i => s i ×ˢ t i)

Tactic:
simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]

Result:
no goals