awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProductMeasure
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
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∞)
⊢ 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 : ℕ))

Tactic:
refine (Measure.pi_eq fun s ms ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.Probability.ProductMeasure
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)
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)) ⋯ 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
⊢ 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:
simp_rw [Measure.map_apply measurable_IocProdIoc (.univ_pi ms), IocProdIoc_preimage hab hbc,
    Measure.prod_prod, Measure.pi_pi, prod_eq_prod_extend]

Premises used: IocProdIoc_preimage, Finset.prod_eq_prod_extend, MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod_prod, measurable_IocProdIoc, MeasureTheory.Measure.pi_pi, MeasurableSet.univ_pi
-- Module: Mathlib.Probability.ProductMeasure
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)
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)) ⋯ 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)
⊢ 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

Tactic:
nth_rw 1 [Eq.comm, ← Ioc_union_Ioc_eq_Ioc hab hbc, prod_union (Ioc_disjoint_Ioc_of_le le_rfl)]

Premises used: Finset.Ioc_union_Ioc_eq_Ioc, le_rfl, Finset.prod_union, Finset.Ioc_disjoint_Ioc_of_le, Eq.comm
-- Module: Mathlib.Probability.ProductMeasure
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)
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)) ⋯ 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)

Tactic:
congr 1
-- Module: Mathlib.Probability.ProductMeasure
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)

Tactic:
prod_congr rfl fun x hx ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.ProductMeasure
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 :
  ∀ (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)
⊢ 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)

Tactic:
refine prod_congr rfl fun x hx ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.ProductMeasure
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)

Tactic:
prod_congr rfl fun x hx ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.ProductMeasure
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 :
  ∀ (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)
⊢ 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)

Tactic:
refine prod_congr rfl fun x hx ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.ProductMeasure
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∞)
e_a₂ 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∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) (↑(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)

Tactic:
rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_right hbc hx),
      restrict₂]

Premises used: Finset.restrict₂, Function.extend_val_apply, Finset.Ioc_subset_Ioc_right
-- Module: Mathlib.Probability.ProductMeasure
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∞)
e_a₂ 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∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a c) (↑(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)

Tactic:
rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_left hab hx),
      restrict₂]

Premises used: Finset.restrict₂, Function.extend_val_apply, Finset.Ioc_subset_Ioc_left
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ))
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 : ℕ))
⊢ 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

Premises used: le_total
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ))

Tactic:
(Measure.pi_eq fun s ms ↦ ?_).symm

Premises used: Set.Mem, setOf, MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
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∞)
⊢ 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:
refine (Measure.pi_eq fun s ms ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.Probability.ProductMeasure
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 :
  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
⊢ 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:
simp_rw [Measure.map_apply measurable_IicProdIoc (.univ_pi ms), IicProdIoc_preimage hab,
      Measure.prod_prod, Measure.pi_pi, prod_eq_prod_extend]

Premises used: Finset.prod_eq_prod_extend, MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod_prod, measurable_IicProdIoc, IicProdIoc_preimage, MeasureTheory.Measure.pi_pi, MeasurableSet.univ_pi