awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
    (∏ 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)
have e_a : ∀ (x : ℕ) (hx : x ∈ Ioc a b),
  Eq (α := ℝ≥0∞)
    (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)
    (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: refine prod_congr rfl fun x hx ↦ ?_
-- 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∞)
    (∏ 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)) ⋯ s i))
        1 x)
have e_a : ∀ (x : ℕ) (hx : x ∈ Ioc b c),
  Eq (α := ℝ≥0∞)
    (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)
    (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: refine prod_congr rfl fun x hx ↦ ?_
-- 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)
x : ℕ
hx : x ∈ Ioc a b
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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)
have e_a : Eq (α := ℝ≥0∞)
  (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 :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_right hbc hx),
      restrict₂]
-- 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)
x : ℕ
hx : x ∈ Ioc a b
e_a :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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)
have e_a₁ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_right hbc hx),
      restrict₂]
-- 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)
x : ℕ
hx : x ∈ Ioc a b
e_a :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx)) :
      ℝ≥0∞)
e_a₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x ⋯) : ℕ))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x ⋯)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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)
have e_a₂ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) x hx) : ℕ) sorry)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_right hbc hx),
      restrict₂]
-- 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)
x : ℕ
hx : x ∈ Ioc b c
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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∞)
  (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 :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_left hab hx),
      restrict₂]
-- 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)
x : ℕ
hx : x ∈ Ioc b c
e_a :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_left hab hx),
      restrict₂]
-- 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)
x : ℕ
hx : x ∈ Ioc b c
e_a :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx)) :
      ℝ≥0∞)
e_a₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x ⋯) : ℕ))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x ⋯)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) x sorry)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) x hx) : ℕ) sorry)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_left hab hx),
      restrict₂]
-- 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 : ℕ
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
      (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))))
    (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
have inl : ∀ (hab : a ≤ b),
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
      (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))))
    (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
Tactic: obtain hab | hba := le_total a b
-- 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 : ℕ
inl :
  ∀ (hab : a ≤ b),
    Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      (map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
        (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))))
      (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
      (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))))
    (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
have inr : ∀ (hba : b ≤ a),
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
      (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))))
    (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
Tactic: obtain hab | hba := le_total a b
-- 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 : ℕ
hab : a ≤ b
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
      (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))))
    (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
have inl : ∀ (s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))) (ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞)
    (((map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
              (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
                (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))) :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥(Iic b), ((μ (↑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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    (((map (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
              (Measure.prod (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ))
                (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))) :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥(Iic b), ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have inl : HMul.hMul (α := ℝ≥0∞)
    (∏ x ∈ Iic a,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic a))
        (fun (i : ↥(Iic a)) ↦
          ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
            (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab 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) =
  ∏ x ∈ Iic b,
    Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic b))
      (fun (i : ↥(Iic b)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x
Tactic: simp_rw [Measure.map_apply measurable_IicProdIoc (.univ_pi ms), IicProdIoc_preimage hab,
      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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x ∈ Iic a,
        Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic a))
          (fun (i : ↥(Iic a)) ↦
            ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
              (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab 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) =
    ∏ x ∈ Iic b,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic b))
        (fun (i : ↥(Iic b)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x
have inl : HMul.hMul (α := ℝ≥0∞)
    (∏ x ∈ Iic a,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic b))
        (fun (i : ↥(Iic b)) ↦ ((μ (↑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 ∈ Iic b))
        (fun (i : ↥(Iic b)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x) =
  HMul.hMul (α := ℝ≥0∞)
    (∏ x ∈ Iic a,
      Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic a))
        (fun (i : ↥(Iic a)) ↦
          ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
            (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab 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: nth_rw 1 [Eq.comm, ← Iic_union_Ioc_eq_Iic hab, prod_union (Iic_disjoint_Ioc le_rfl)]