awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
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) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove α i)
refine :
  MeasurePreserving (α := α i × ((j : Fin n) → α (i.succAbove j)))
    (⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j)
    ((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j)))
    (Measure.pi (α := α) μ)
⊢ MeasurePreserving (β := α i × ((j : Fin n) → α (i.succAbove j)))
    (⇑(MeasurableEquiv.piFinSuccAbove α i) : (a : (j : Fin (n + 1)) → α j) → α i × ((j : Fin n) → α (i.succAbove j)))
    (Measure.pi (α := α) μ)
    ((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j)))

Tactic:
refine MeasurePreserving.symm e ?_

Premises used: MeasureTheory.MeasurePreserving.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
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) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove α i)
⊢ MeasurePreserving (α := α i × ((j : Fin n) → α (i.succAbove j)))
    (⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j)
    ((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j)))
    (Measure.pi (α := α) μ)

Tactic:
⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩

Premises used: MeasureTheory.MeasurePreserving.mk, MeasureTheory.Measure.pi_eq, MeasurableEquiv.measurable, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
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) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove α i)
refine :
  ∀ (s : (i : Fin (n + 1)) → Set (α i)),
    (∀ (i : Fin (n + 1)), MeasurableSet (s i)) →
      Eq (α := ℝ≥0∞)
        (((Measure.map (α := α i × ((j : Fin n) → α (i.succAbove j)))
                  (⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j)
                  ((μ i).prod
                    (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j))) :
                Measure ((j : Fin (n + 1)) → α j)) :
              (a : Set ((i : Fin (n + 1)) → α i)) → ℝ≥0∞)
            (Set.pi (α := α) univ s) :
          ℝ≥0∞)
        (∏ i : Fin (n + 1), (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ MeasurePreserving (α := α i × ((j : Fin n) → α (i.succAbove j)))
    (⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j)
    ((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j)))
    (Measure.pi (α := α) μ)

Tactic:
refine ⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
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) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove α i)
s : (i : Fin (n + 1)) → Set (α i)
h : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j)) :
            Measure (α i × ((j : Fin n) → α (i.succAbove j)))) :
          (a : Set (α i × ((j : Fin n) → α (i.succAbove j)))) → ℝ≥0∞)
        ((⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j) ⁻¹' Set.pi (α := α) univ s) :
      ℝ≥0∞)
    ((((μ i).prod (Measure.pi (α := fun (i_1 : Fin n) ↦ α (i.succAbove i_1)) fun (i_1 : Fin n) ↦ μ (i.succAbove i_1)) :
            Measure (α i × ((i_1 : Fin n) → α (i.succAbove i_1)))) :
          (a : Set (α i × ((i_1 : Fin n) → α (i.succAbove i_1)))) → ℝ≥0∞)
        (SProd.sprod (β := Set ((i_1 : Fin n) → α (i.succAbove i_1))) (s i)
          (Set.pi (α := fun (i_1 : Fin n) ↦ α (i.succAbove i_1)) univ fun (i_1 : Fin n) ↦ s (i.succAbove i_1))) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (α := α i × ((j : Fin n) → α (i.succAbove j)))
              (⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j)
              ((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j))) :
            Measure ((j : Fin (n + 1)) → α j)) :
          (a : Set ((i : Fin (n + 1)) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : Fin (n + 1), (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [e.map_apply, i.prod_univ_succAbove _, ← pi_pi, ← prod_prod]

Premises used: MeasurableEquiv.map_apply, Fin.prod_univ_succAbove, MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
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) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove α i)
s : (i : Fin (n + 1)) → Set (α i)
h_1 : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
h :
  ∀ (x : α i) (f : (j : Fin n) → α (i.succAbove j)),
    Membership.mem (γ := Set (α i × ((j : Fin n) → α (i.succAbove j))))
        ((⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j) ⁻¹' Set.pi (α := α) univ s)
        (x, f) ↔
      (x, f) ∈
        SProd.sprod (β := Set ((i_1 : Fin n) → α (i.succAbove i_1))) (s i)
          (Set.pi (α := fun (i_1 : Fin n) ↦ α (i.succAbove i_1)) univ fun (i_1 : Fin n) ↦ s (i.succAbove i_1))
⊢ Eq (α := ℝ≥0∞)
    ((((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j)) :
            Measure (α i × ((j : Fin n) → α (i.succAbove j)))) :
          (a : Set (α i × ((j : Fin n) → α (i.succAbove j)))) → ℝ≥0∞)
        ((⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j) ⁻¹' Set.pi (α := α) univ s) :
      ℝ≥0∞)
    ((((μ i).prod (Measure.pi (α := fun (i_1 : Fin n) ↦ α (i.succAbove i_1)) fun (i_1 : Fin n) ↦ μ (i.succAbove i_1)) :
            Measure (α i × ((i_1 : Fin n) → α (i.succAbove i_1)))) :
          (a : Set (α i × ((i_1 : Fin n) → α (i.succAbove i_1)))) → ℝ≥0∞)
        (SProd.sprod (β := Set ((i_1 : Fin n) → α (i.succAbove i_1))) (s i)
          (Set.pi (α := fun (i_1 : Fin n) ↦ α (i.succAbove i_1)) univ fun (i_1 : Fin n) ↦ s (i.succAbove i_1))) :
      ℝ≥0∞)

Tactic:
congr 1 with ⟨x, f⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
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) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove α i)
s : (i : Fin (n + 1)) → Set (α i)
h : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
x : α i
f : (j : Fin n) → α (i.succAbove j)
⊢ Membership.mem (γ := Set (α i × ((j : Fin n) → α (i.succAbove j))))
      ((⇑e : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j) ⁻¹' Set.pi (α := α) univ s)
      (x, f) ↔
    (x, f) ∈
      SProd.sprod (β := Set ((i_1 : Fin n) → α (i.succAbove i_1))) (s i)
        (Set.pi (α := fun (i_1 : Fin n) ↦ α (i.succAbove i_1)) univ fun (i_1 : Fin n) ↦ s (i.succAbove i_1))

Tactic:
simp [e, i.forall_iff_succAbove]

Premises used: Fin.forall_iff_succAbove
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
n : ℕ
α : Fin (n + 1) → Type u
inst : (i : Fin (n + 1)) → MeasureSpace (α i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite.{u} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
i : Fin (n + 1)
⊢ MeasurePreserving (α := (j : Fin (n + 1)) → α j) (β := α i × ((j : Fin n) → α (i.succAbove j)))
    (⇑(MeasurableEquiv.piFinSuccAbove α i) : (a : (j : Fin (n + 1)) → α j) → α i × ((j : Fin n) → α (i.succAbove j)))
    (volume : Measure ((j : Fin (n + 1)) → α j)) (volume : Measure (α i × ((j : Fin n) → α (i.succAbove j))))

Tactic:
measurePreserving_piFinSuccAbove (fun _ => volume) i

Premises used: MeasureTheory.measurePreserving_piFinSuccAbove, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
set :
  let e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X;
  Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
⊢ Eq (α := Measure (X default))
    (Measure.map (⇑(MeasurableEquiv.piUnique X) : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)

Tactic:
set e := MeasurableEquiv.piUnique X

Premises used: MeasurableEquiv.piUnique
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
h :
  ∀ (s : Set ((i : ι) → X i)),
    piPremeasure (α := X) (fun (i : ι) ↦ (μ i).toOuterMeasure) s =
      (Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        s
⊢ Eq (α := (s : Set ((i : ι) → X i)) → ℝ≥0∞) (piPremeasure (α := X) fun (i : ι) ↦ (μ i).toOuterMeasure)
    (⇑(Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default)) :
      (a : Set ((i : ι) → X i)) → ℝ≥0∞)

Tactic:
ext1 s
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
h :
  Eq (α := ℝ≥0∞)
    (((μ default : Measure (X default)) : (a : Set (X default)) → ℝ≥0∞) (eval (β := X) default '' s) : ℝ≥0∞)
    (((μ default : Measure (X default)) : (a : Set (X default)) → ℝ≥0∞)
        ((⇑e.symm : (a : X default) → (i : ι) → X i) ⁻¹' s) :
      ℝ≥0∞)
⊢ piPremeasure (α := X) (fun (i : ι) ↦ (μ i).toOuterMeasure) s =
    (Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      s

Tactic:
rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]

Premises used: MeasurableEquiv.map_apply, MeasureTheory.Measure.coe_toOuterMeasure, MeasurableEquiv.symm, MeasureTheory.piPremeasure, Fintype.prod_unique
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
h : Eq (α := Set (X default)) (eval (β := X) default '' s) ((⇑e.symm : (a : X default) → (i : ι) → X i) ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    (((μ default : Measure (X default)) : (a : Set (X default)) → ℝ≥0∞) (eval (β := X) default '' s) : ℝ≥0∞)
    (((μ default : Measure (X default)) : (a : Set (X default)) → ℝ≥0∞)
        ((⇑e.symm : (a : X default) → (i : ι) → X i) ⁻¹' s) :
      ℝ≥0∞)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ Eq (α := Set (X default)) (eval (β := X) default '' s) ((⇑e.symm : (a : X default) → (i : ι) → X i) ⁻¹' s)

Tactic:
e.toEquiv.image_eq_preimage_symm s

Premises used: MeasurableEquiv.toEquiv, Equiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ Eq (α := Set (X default)) (eval (β := X) default '' s) ((⇑e.symm : (a : X default) → (i : ι) → X i) ⁻¹' s)

Tactic:
exact e.toEquiv.image_eq_preimage_symm s

Premises used: MeasurableEquiv.toEquiv, Equiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
⊢ Eq (α := (s : Set ((i : ι) → X i)) → ℝ≥0∞) (piPremeasure (α := X) fun (i : ι) ↦ (μ i).toOuterMeasure)
    (⇑(Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default)) :
      (a : Set ((i : ι) → X i)) → ℝ≥0∞)

Tactic:
have : (piPremeasure fun i => (μ i).toOuterMeasure) = Measure.map e.symm (μ default) := by
      ext1 s
      rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]
      congr 1; exact e.toEquiv.image_eq_preimage_symm s
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
this :
  Eq (α := (s : Set ((i : ι) → X i)) → ℝ≥0∞) (piPremeasure (α := X) fun (i : ι) ↦ (μ i).toOuterMeasure)
    (⇑(Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default)) :
      (a : Set ((i : ι) → X i)) → ℝ≥0∞)
simp_rw :
  Eq (α := Measure (X default))
    (Measure.map (⇑e : (a : (i : ι) → X i) → X default)
      (toMeasure (OuterMeasure.pi (α := X) fun (i : ι) ↦ (μ i).toOuterMeasure) ⋯))
    (μ default)
simp_rw₁ :
  Eq (α := Measure (X default))
    (Measure.map (⇑e : (a : (i : ι) → X i) → X default)
      (toMeasure (boundedBy (piPremeasure (α := X) fun (i : ι) ↦ (μ i).toOuterMeasure)) ⋯))
    (μ default)
simp_rw₂ :
  Eq (α := Measure (X default))
    (Measure.map (⇑e : (a : (i : ι) → X i) → X default)
      (toMeasure
        (boundedBy
          (⇑(Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default)) :
            (a : Set ((i : ι) → X i)) → ℝ≥0∞))
        ⋯))
    (μ default)
simp_rw₃ :
  Eq (α := Measure (X default))
    (Measure.map (⇑e : (a : (i : ι) → X i) → X default)
      (toMeasure
        (boundedBy
          (⇑(toOuterMeasure (Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default))) :
            (a : Set ((i : ι) → X i)) → ℝ≥0∞))
        ⋯))
    (μ default)
simp_rw₄ :
  Eq (α := Measure (X default))
    (Measure.map (⇑e : (a : (i : ι) → X i) → X default)
      (toMeasure (toOuterMeasure (Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default)))
        ⋯))
    (μ default)
simp_rw₅ :
  Eq (α := Measure (X default))
    (Measure.map (α := (i : ι) → X i) (⇑e : (a : (i : ι) → X i) → X default)
      (Measure.map (α := X default) (⇑e.symm : (a : X default) → (i : ι) → X i) (μ default)))
    (μ default)
⊢ Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)

Tactic:
simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]

Premises used: MeasureTheory.OuterMeasure.pi, MeasureTheory.toOuterMeasure_toMeasure, MeasureTheory.Measure.coe_toOuterMeasure, MeasureTheory.OuterMeasure.boundedBy_eq_self, MeasurableEquiv.map_map_symm, MeasureTheory.Measure.pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
inst_1 : Unique ι
inst_2 : (i : ι) → MeasureSpace (X i)
⊢ MeasurePreserving (α := (i : ι) → X i) (β := X default)
    (⇑(MeasurableEquiv.piUnique X) : (a : (i : ι) → X i) → X default) volume volume

Tactic:
measurePreserving_piUnique _

Premises used: MeasureTheory.measurePreserving_piUnique
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
β : Type u
_m : MeasurableSpace β
μ : Measure β
α : Type v
inst : Unique α
⊢ MeasurePreserving (α := α → β) (⇑(MeasurableEquiv.funUnique α β) : (a : α → β) → β)
    (Measure.pi (α := fun (a : α) ↦ β) fun (x : α) ↦ μ) μ

Tactic:
measurePreserving_piUnique _

Premises used: MeasureTheory.measurePreserving_piUnique
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u
β : Type v
inst : Unique α
inst_1 : MeasureSpace β
⊢ MeasurePreserving (α := α → β) (β := β) (⇑(MeasurableEquiv.funUnique α β) : (a : α → β) → β) volume volume

Tactic:
measurePreserving_funUnique volume α

Premises used: MeasureTheory.measurePreserving_funUnique, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst : ∀ (i : Fin 2), SigmaFinite (μ i)
⊢ MeasurePreserving (β := α 0 × α 1) (⇑(MeasurableEquiv.piFinTwo α) : (a : (i : Fin 2) → α i) → α 0 × α 1)
    (Measure.pi (α := α) μ) (Measure.prod (μ 0) (μ 1))

Tactic:
⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => ?_).symm⟩

Premises used: MeasureTheory.Measure.prod_eq, MeasureTheory.MeasurePreserving.mk, MeasurableEquiv.measurable, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst : ∀ (i : Fin 2), SigmaFinite (μ i)
refine :
  ∀ (s : Set (α 0)) (t : Set (α 1)),
    MeasurableSet s →
      MeasurableSet t →
        ((Measure.map (⇑(MeasurableEquiv.piFinTwo α) : (a : (i : Fin 2) → α i) → α 0 × α 1) (Measure.pi (α := α) μ) :
                Measure (α 0 × α 1)) :
              (a : Set (α 0 × α 1)) → ℝ≥0∞)
            (s ×ˢ t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ 0 : Measure (α 0)) : (a : Set (α 0)) → ℝ≥0∞) s : ℝ≥0∞)
            (((μ 1 : Measure (α 1)) : (a : Set (α 1)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ MeasurePreserving (β := α 0 × α 1) (⇑(MeasurableEquiv.piFinTwo α) : (a : (i : Fin 2) → α i) → α 0 × α 1)
    (Measure.pi (α := α) μ) (Measure.prod (μ 0) (μ 1))

Tactic:
refine ⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => ?_).symm⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : 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)
h : MeasurableSet s
h_1 : MeasurableSet t
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ 0 : Measure (α 0)) : (a : Set (α 0)) → ℝ≥0∞)
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ Set (α i)) s
            (Fin.cons (α := fun (i : Fin 1) ↦ Set (α i.succ)) t
              (finZeroElim (α := fun (i : Fin 0) ↦ Set (α i.succ.succ))))
            0) :
        ℝ≥0∞)
      (((μ 1 : Measure (α 1)) : (a : Set (α 1)) → ℝ≥0∞)
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ Set (α i)) s
            (Fin.cons (α := fun (i : Fin 1) ↦ Set (α i.succ)) t
              (finZeroElim (α := fun (i : Fin 0) ↦ Set (α i.succ.succ))))
            1) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ 0 : Measure (α 0)) : (a : Set (α 0)) → ℝ≥0∞) s : ℝ≥0∞)
      (((μ 1 : Measure (α 1)) : (a : Set (α 1)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ((Measure.map (⇑(MeasurableEquiv.piFinTwo α) : (a : (i : Fin 2) → α i) → α 0 × α 1) (Measure.pi (α := α) μ) :
          Measure (α 0 × α 1)) :
        (a : Set (α 0 × α 1)) → ℝ≥0∞)
      (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ 0 : Measure (α 0)) : (a : Set (α 0)) → ℝ≥0∞) s : ℝ≥0∞)
      (((μ 1 : Measure (α 1)) : (a : Set (α 1)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod,
    Measure.pi_pi, Fin.prod_univ_two]

Premises used: MeasurableEquiv.map_apply, Fin.preimage_apply_01_prod, Fin.prod_univ_two, MeasurableEquiv.piFinTwo_apply, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : 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)
h : MeasurableSet s
h_1 : MeasurableSet t
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ 0 : Measure (α 0)) : (a : Set (α 0)) → ℝ≥0∞)
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ Set (α i)) s
            (Fin.cons (α := fun (i : Fin 1) ↦ Set (α i.succ)) t
              (finZeroElim (α := fun (i : Fin 0) ↦ Set (α i.succ.succ))))
            0) :
        ℝ≥0∞)
      (((μ 1 : Measure (α 1)) : (a : Set (α 1)) → ℝ≥0∞)
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ Set (α i)) s
            (Fin.cons (α := fun (i : Fin 1) ↦ Set (α i.succ)) t
              (finZeroElim (α := fun (i : Fin 0) ↦ Set (α i.succ.succ))))
            1) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ 0 : Measure (α 0)) : (a : Set (α 0)) → ℝ≥0∞) s : ℝ≥0∞)
      (((μ 1 : Measure (α 1)) : (a : Set (α 1)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Fin 2 → Type u
inst : (i : Fin 2) → MeasureSpace (α i)
inst_1 : ∀ (i : Fin 2), SigmaFinite.{u} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ MeasurePreserving (α := (i : Fin 2) → α i) (β := α 0 × α 1)
    (⇑(MeasurableEquiv.piFinTwo α) : (a : (i : Fin 2) → α i) → α 0 × α 1) volume volume

Tactic:
measurePreserving_piFinTwo _

Premises used: MeasureTheory.measurePreserving_piFinTwo
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u
x : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ MeasurePreserving (⇑MeasurableEquiv.finTwoArrow : (a : Fin 2 → α) → α × α)
    (Measure.pi (α := fun (a : Fin 2) ↦ α) ![μ, ν]) (μ.prod ν)

Tactic:
haveI : ∀ i, SigmaFinite (![μ, ν] i) := Fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩
  measurePreserving_piFinTwo _

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, MeasureTheory.measurePreserving_piFinTwo, Fin.induction, Matrix.vecEmpty, Fin.cases, Matrix.vecCons
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ MeasurePreserving (α := Fin 2 → α) (⇑MeasurableEquiv.finTwoArrow : (a : Fin 2 → α) → α × α)
    (Measure.pi (α := fun (a : Fin 2) ↦ α) fun (x : Fin 2) ↦ μ) (μ.prod μ)

Tactic:
simpa only [Matrix.vec_single_eq_const, Matrix.vecCons_const] using
    measurePreserving_finTwoArrow_vec μ μ

Premises used: MeasureTheory.measurePreserving_finTwoArrow_vec, Matrix.vecCons_const, Matrix.vec_single_eq_const
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u
inst : MeasureSpace α
inst_1 : SigmaFinite.{u} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ MeasurePreserving.{u, u} (α := Fin 2 → α) (β := α × α) (⇑MeasurableEquiv.finTwoArrow : (a : Fin 2 → α) → α × α) volume
    volume

Tactic:
measurePreserving_finTwoArrow volume

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.measurePreserving_finTwoArrow
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
set :
  let e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit;
  MeasurePreserving (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ) (Measure.dirac ())
⊢ MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit) : (a : (i : ι) → α i) → Unit)
    (Measure.pi (α := α) μ) (Measure.dirac ())

Tactic:
set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit

Premises used: Unit, MeasurableEquiv.ofUniqueOfUnique