awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)))
    (⇑(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)))
have 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 (α := α) μ)
Tactic: refine MeasurePreserving.symm e ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 (α := α) μ)
have 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∞)
Tactic: refine ⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ 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∞)
have 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∞)
Tactic: rw [e.map_apply, i.prod_univ_succAbove _, ← pi_pi, ← prod_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ 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∞)
have 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))
Tactic: congr 1 with ⟨x, f⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
have 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
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ 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
have 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∞)
Tactic: rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 (α := ℝ≥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∞)
have h : Eq (α := Set (X default)) (eval (β := X) default '' s) ((⇑e.symm : (a : X default) → (i : ι) → X i) ⁻¹' s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
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 (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
have simp_rw : Eq (α := Measure (X default))
  (Measure.map (⇑e : (a : (i : ι) → X i) → X default)
    (toMeasure (OuterMeasure.pi (α := X) fun (i : ι) ↦ (μ i).toOuterMeasure) sorry))
  (μ default)
Tactic: simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
have simp_rw₁ : Eq (α := Measure (X default))
  (Measure.map (⇑e : (a : (i : ι) → X i) → X default)
    (toMeasure (boundedBy (piPremeasure (α := X) fun (i : ι) ↦ (μ i).toOuterMeasure)) sorry))
  (μ default)
Tactic: simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
have 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∞))
      sorry))
  (μ default)
Tactic: simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
have 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∞))
      sorry))
  (μ default)
Tactic: simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
have 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)))
      sorry))
  (μ default)
Tactic: simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ Eq (α := Measure (X default)) (Measure.map (⇑e : (a : (i : ι) → X i) → X default) (Measure.pi (α := X) μ)) (μ default)
have 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)
Tactic: simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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))
have 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∞)
Tactic: refine ⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => ?_).symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ ((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∞)
have 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∞)
Tactic: rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod,
    Measure.pi_pi, Fin.prod_univ_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ) (Measure.dirac ())
have refine : Eq (α := Measure Unit) (Measure.map (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ)) (Measure.dirac ())
Tactic: refine ⟨e.measurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ Eq (α := Measure Unit) (Measure.map (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ)) (Measure.dirac ())
have rw : Eq (α := Measure Unit)
  (Measure.map (α := (i : ι) → α i) (⇑e : (a : (i : ι) → α i) → Unit)
    (Measure.dirac fun (a : ι) ↦ isEmptyElim (p := fun (x : ι) ↦ α x) a))
  (Measure.dirac ())
Tactic: rw [Measure.pi_of_empty, Measure.map_dirac' e.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
rw :
  Eq (α := Measure Unit)
    (Measure.map (α := (i : ι) → α i) (⇑e : (a : (i : ι) → α i) → Unit)
      (Measure.dirac fun (a : ι) ↦ isEmptyElim (p := fun (x : ι) ↦ α x) a))
    (Measure.dirac ())
⊢ Eq (α := Measure Unit) (Measure.map (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ)) (Measure.dirac ())
have rw₁ : Eq (α := Measure Unit)
  (Measure.dirac ((e : (a : (i : ι) → α i) → Unit) fun (a : ι) ↦ isEmptyElim (p := fun (x : ι) ↦ α x) a) : Measure Unit)
  (Measure.dirac () : Measure Unit)
Tactic: rw [Measure.pi_of_empty, Measure.map_dirac' e.measurable]