ι : Type ?u.5928630
ι' : Type ?u.5928633
α✝ : ι → Type ?u.5928638
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(Measure.map (↑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = ↑↑(μ 0) s * ↑↑(μ 1) t
ι : Type ?u.5928630
ι' : Type ?u.5928633
α✝ : ι → Type ?u.5928638
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
⊢ MeasurePreserving ↑(MeasurableEquiv.piFinTwo α)
refine' ⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => _).symm⟩
ι : Type ?u.5928630
ι' : Type ?u.5928633
α✝ : ι → Type ?u.5928638
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * ↑↑(μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) =
    ↑↑(μ 0) s * ↑↑(μ 1) t
ι : Type ?u.5928630
ι' : Type ?u.5928633
α✝ : ι → Type ?u.5928638
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(Measure.map (↑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = ↑↑(μ 0) s * ↑↑(μ 1) t
rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod,
  Measure.pi_pi, Fin.prod_univ_two]
no goals
ι : Type ?u.5928630
ι' : Type ?u.5928633
α✝ : ι → Type ?u.5928638
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * ↑↑(μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) =
    ↑↑(μ 0) s * ↑↑(μ 1) t
rfl