awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
simp_rw simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI) (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw₂ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
      (restrict₂ (π := X) hJI ⁻¹' Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
    ℝ≥0∞)
  (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: classical
  simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
  refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
  · rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
simp_rw simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI) (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        (restrict₂ (π := X) hJI ⁻¹' Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw₃ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
      (Set.pi (α := fun (i : ↥I) ↦ X (↑i : ι)) Set.univ fun (j : ↥I) ↦
        if h : (↑j : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑j : ι) h) else Set.univ) :
    ℝ≥0∞)
  (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: classical
  simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
  refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
  · rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
simp_rw simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI) (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        (restrict₂ (π := X) hJI ⁻¹' Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₃ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥I) ↦ X (↑i : ι)) Set.univ fun (j : ↥I) ↦
          if h : (↑j : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑j : ι) h) else Set.univ) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw₄ : Eq (α := ℝ≥0∞)
  (∏ i : ↥I,
    ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
      (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
  (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i))
Tactic: classical
  simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
  refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
  · rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
simp_rw simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI) (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        (restrict₂ (π := X) hJI ⁻¹' Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₃ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥I) ↦ X (↑i : ι)) Set.univ fun (j : ↥I) ↦
          if h : (↑j : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑j : ι) h) else Set.univ) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₄ :
  Eq (α := ℝ≥0∞)
    (∏ i : ↥I,
      ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
        (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i))
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw₅ : Eq (α := ℝ≥0∞)
  (∏ x ∈ I,
    Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
  (∏ x ∈ J,
    Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
Tactic: classical
  simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
  refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
  · rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
have this : s =
  cylinder (α := X) univ ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
Tactic: have : s = cylinder univ (MeasurableEquiv.piCongrLeft X e ⁻¹' s) := rfl
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
this :
  s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
have nth_rw : Eq (α := ℝ≥0∞)
  ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      (cylinder (α := X) univ
        ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)) :
    ℝ≥0∞)
  ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: nth_rw 1 [this]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
this :
  s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (cylinder (α := X) univ
          ((⇑(piCongrLeft X
                  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
                    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯,
                    left_inv := ⋯, right_inv := ⋯ }) :
              (a : (b : ↥univ) → X (↑b : ι)) → (a : ι) → X a) ⁻¹'
            s)) :
      ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((Measure.map (α := (i : ↥univ) → X (↑i : ι))
          (⇑(piCongrLeft X
                { toFun := fun (i : ↥univ) ↦ (↑i : ι),
                  invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i sorry,
                  left_inv := sorry, right_inv := sorry }) :
            (a : (b : ↥univ) → X (↑b : ι)) → (a : ι) → X a)
          (Measure.pi (α := fun (i : ↥univ) ↦ X (↑i : ι)) fun (i : ↥univ) ↦ μ (↑i : ι)) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((Measure.map (α := (b : ↥univ) → X ((e : (a : ↥univ) → ι) b))
          (⇑(piCongrLeft (fun (i : ι) ↦ X i) e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a)
          (Measure.pi (α := fun (i : ↥univ) ↦ X ((e : (a : ↥univ) → ι) i)) fun (i : ↥univ) ↦
            μ ((e : (a : ↥univ) → ι) i)) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← Measure.pi_map_piCongrLeft e,
    ← Measure.map_apply (by fun_prop) hs]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Ioc a c)) → X (↑i : ℕ)))
    (map (IocProdIoc (X := X) a b c)
      (Measure.prod (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc b c)) ↦ μ (↑i : ℕ))))
    (Measure.pi (α := fun (i : ↥(Ioc a c)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a c)) ↦ μ (↑i : ℕ))
have refine : ∀ (s : (i : ↥(Ioc a c)) → Set (X (↑i : ℕ))) (ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞)
    (((map (IocProdIoc (X := X) a b c)
              (Measure.prod (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))
                (Measure.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc b c)) ↦ μ (↑i : ℕ))) :
            Measure ((i : ↥(Ioc a c)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a c)) → X (↑i : ℕ))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥(Ioc a c)) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥(Ioc a c), ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine (Measure.pi_eq fun s ms ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    (((map (IocProdIoc (X := X) a b c)
              (Measure.prod (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))
                (Measure.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc b c)) ↦ μ (↑i : ℕ))) :
            Measure ((i : ↥(Ioc a c)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a c)) → X (↑i : ℕ))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥(Ioc a c)) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥(Ioc a c), ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw : HMul.hMul (α := ℝ≥0∞)
    (∏ x ∈ Ioc a b,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a b))
        (fun (i : ↥(Ioc a b)) ↦
          ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
            (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s i))
        1 x)
    (∏ x ∈ Ioc b c,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc b c))
        (fun (i : ↥(Ioc b c)) ↦
          ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
            (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s i))
        1 x) =
  ∏ x ∈ Ioc a c,
    Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
      (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x
Tactic: simp_rw [Measure.map_apply measurable_IocProdIoc (.univ_pi ms), IocProdIoc_preimage hab hbc,
    Measure.prod_prod, Measure.pi_pi, prod_eq_prod_extend]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x ∈ Ioc a b,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a b))
          (fun (i : ↥(Ioc a b)) ↦
            ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
              (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s i))
          1 x)
      (∏ x ∈ Ioc b c,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc b c))
          (fun (i : ↥(Ioc b c)) ↦
            ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
              (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s i))
          1 x) =
    ∏ x ∈ Ioc a c,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
        (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x
have nth_rw : HMul.hMul (α := ℝ≥0∞)
    (∏ x ∈ Ioc a b,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
        (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x)
    (∏ x ∈ Ioc b c,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
        (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x) =
  HMul.hMul (α := ℝ≥0∞)
    (∏ x ∈ Ioc a b,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a b))
        (fun (i : ↥(Ioc a b)) ↦
          ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
            (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s i))
        1 x)
    (∏ x ∈ Ioc b c,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc b c))
        (fun (i : ↥(Ioc b c)) ↦
          ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
            (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s i))
        1 x)
Tactic: nth_rw 1 [Eq.comm, ← Ioc_union_Ioc_eq_Ioc hab hbc, prod_union (Ioc_disjoint_Ioc_of_le le_rfl)]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x ∈ Ioc a b,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
          (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x)
      (∏ x ∈ Ioc b c,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
          (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x ∈ Ioc a b,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a b))
          (fun (i : ↥(Ioc a b)) ↦
            ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
              (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s i))
          1 x)
      (∏ x ∈ Ioc b c,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc b c))
          (fun (i : ↥(Ioc b c)) ↦
            ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
              (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s i))
          1 x)
have e_a : Eq (α := ℝ≥0∞)
  (∏ x ∈ Ioc a b,
    Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
      (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x)
  (∏ x ∈ Ioc a b,
    Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a b))
      (fun (i : ↥(Ioc a b)) ↦
        ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
          (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s i))
      1 x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
e_a :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ Ioc a b,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
        (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x)
    (∏ x ∈ Ioc a b,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a b))
        (fun (i : ↥(Ioc a b)) ↦
          ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
            (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s i))
        1 x)
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x ∈ Ioc a b,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
          (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x)
      (∏ x ∈ Ioc b c,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
          (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x ∈ Ioc a b,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a b))
          (fun (i : ↥(Ioc a b)) ↦
            ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
              (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s i))
          1 x)
      (∏ x ∈ Ioc b c,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc b c))
          (fun (i : ↥(Ioc b c)) ↦
            ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
              (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s i))
          1 x)
have e_a₁ : Eq (α := ℝ≥0∞)
  (∏ x ∈ Ioc b c,
    Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc a c))
      (fun (i : ↥(Ioc a c)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x)
  (∏ x ∈ Ioc b c,
    Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Ioc b c))
      (fun (i : ↥(Ioc b c)) ↦
        ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
          (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s i))
      1 x)
Tactic: congr 1