ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
⊢ MeasurePreserving ↑(MeasurableEquiv.piFinSuccAboveEquiv α i)
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
⊢ MeasurePreserving ↑(MeasurableEquiv.piFinSuccAboveEquiv α i)
set e := (MeasurableEquiv.piFinSuccAboveEquiv α i).symm
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
⊢ MeasurePreserving ↑e
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
⊢ MeasurePreserving ↑(MeasurableEquiv.piFinSuccAboveEquiv α i)
refine' MeasurePreserving.symm e _
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ↑↑(Measure.map (↑e) (Measure.prod (μ i) (Measure.pi fun j => μ (↑(Fin.succAbove i) j)))) (Set.pi univ s) =
    ∏ i : Fin (n + 1), ↑↑(μ i) (s i)
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
⊢ MeasurePreserving ↑e
refine' ⟨e.measurable, (pi_eq fun s _ => _).symm⟩
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ↑↑(Measure.prod (μ i) (Measure.pi fun j => μ (↑(Fin.succAbove i) j))) (↑e ⁻¹' Set.pi univ s) =
    ↑↑(Measure.prod (μ i) (Measure.pi fun i_1 => μ (↑(Fin.succAbove i) i_1)))
      (s i ×ˢ Set.pi univ fun i_1 => s (↑(Fin.succAbove i) i_1))
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ↑↑(Measure.map (↑e) (Measure.prod (μ i) (Measure.pi fun j => μ (↑(Fin.succAbove i) j)))) (Set.pi univ s) =
    ∏ i : Fin (n + 1), ↑↑(μ i) (s i)
rw [e.map_apply, i.prod_univ_succAbove _, ← pi_pi, ← prod_prod]
case e_a.h.mk
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
x : α i
f : (j : Fin n) → α (↑(Fin.succAbove i) j)
⊢ (x, f) ∈ ↑e ⁻¹' Set.pi univ s ↔ (x, f) ∈ s i ×ˢ Set.pi univ fun i_1 => s (↑(Fin.succAbove i) i_1)
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ↑↑(Measure.prod (μ i) (Measure.pi fun j => μ (↑(Fin.succAbove i) j))) (↑e ⁻¹' Set.pi univ s) =
    ↑↑(Measure.prod (μ i) (Measure.pi fun i_1 => μ (↑(Fin.succAbove i) i_1)))
      (s i ×ˢ Set.pi univ fun i_1 => s (↑(Fin.succAbove i) i_1))
congr 1 with ⟨x, f⟩
no goals
case e_a.h.mk
ι : Type ?u.5778373
ι' : Type ?u.5778376
α✝ : ι → Type ?u.5778381
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (↑(Fin.succAbove i) j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
x : α i
f : (j : Fin n) → α (↑(Fin.succAbove i) j)
⊢ (x, f) ∈ ↑e ⁻¹' Set.pi univ s ↔ (x, f) ∈ s i ×ˢ Set.pi univ fun i_1 => s (↑(Fin.succAbove i) i_1)
simp [i.forall_iff_succAbove]