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 : ℕ
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 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)) ⋯ s i))
          1 x)
have inl : Eq (α := ℝ≥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 ∈ 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)
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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
inl :
  Eq (α := ℝ≥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 ∈ 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)
⊢ 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)) ⋯ s i))
          1 x)
have inl₁ : Eq (α := ℝ≥0∞)
  (∏ 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)
  (∏ 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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ Eq (α := ℝ≥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 ∈ 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)
have inl : ∀ (x : ℕ) (hx : x ∈ Iic a),
  Eq (α := ℝ≥0∞)
    (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)
    (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)
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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    (∏ 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)
    (∏ 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 inl : ∀ (x : ℕ) (hx : x ∈ Ioc a b),
  Eq (α := ℝ≥0∞)
    (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)
    (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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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)
have inl : Eq (α := ℝ≥0∞)
  (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 :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Iic_subset_Iic.2 hab hx),
        frestrictLe₂, 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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
inl :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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)
have inl₁ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Iic_subset_Iic.2 hab hx),
        frestrictLe₂, 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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
inl :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
      ℝ≥0∞)
inl₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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)
have inl₂ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry)) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
        (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
      (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) sorry s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
    ℝ≥0∞)
Tactic: rw [Function.extend_val_apply hx, Function.extend_val_apply (Iic_subset_Iic.2 hab hx),
        frestrictLe₂, 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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ Eq (α := ℝ≥0∞)
    (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)
    (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 inl : Eq (α := ℝ≥0∞)
  (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 :
    ℝ≥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_Iic_self 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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
inl :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥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 ∈ Iic b))
      (fun (i : ↥(Iic b)) ↦ ((μ (↑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 inl₁ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) 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_Iic_self 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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
inl :
  Eq (α := ℝ≥0∞)
    (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 :
      ℝ≥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∞)
inl₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) 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 ∈ Iic b))
      (fun (i : ↥(Iic b)) ↦ ((μ (↑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 inl₂ : Eq (α := ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x sorry) : ℕ))) :
        (a : Set (X (↑⟨x, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) 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 ∈ Iic b) (↑(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_Iic_self 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 : ℕ
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 : ℕ))
have inr : Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (map (frestrictLe₂ (π := X) hba) (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ)))
  (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
Tactic: rw [IicProdIoc_le hba, ← Measure.map_map, ← Measure.fst, Measure.fst_prod]
-- 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 : ℕ
hba : b ≤ a
inr :
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (map (frestrictLe₂ (π := X) hba)
      (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑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₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) hba)
Tactic: rw [IicProdIoc_le hba, ← Measure.map_map, ← Measure.fst, Measure.fst_prod]
-- 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 : ℕ
hba : b ≤ a
inr :
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (map (frestrictLe₂ (π := X) hba)
      (Measure.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic a)) ↦ μ (↑i : ℕ)))
    (Measure.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic b)) ↦ μ (↑i : ℕ))
inr₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) hba)
⊢ 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₂ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) Prod.fst
Tactic: rw [IicProdIoc_le hba, ← Measure.map_map, ← Measure.fst, Measure.fst_prod]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
⊢ Eq (α := Measure ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (map (α := X (n + 1)) (⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
      (μ (n + 1)))
    (Measure.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc n (n + 1))) ↦ μ (↑i : ℕ))
have refine : ∀ (s : (i : ↥(Ioc n (n + 1))) → Set (X (↑i : ℕ))) (hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞)
    (((map (α := X (n + 1)) (⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
              (μ (n + 1)) :
            Measure ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥(Ioc n (n + 1)), ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine (Measure.pi_eq fun s hs ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X (↑i : ℕ))
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
⊢ Subsingleton ↥(Ioc n (n + 1))
have rw : Subsingleton ↥{n + 1}
Tactic: rw [Nat.Ioc_succ_singleton]