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 : ℕ
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 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)
⊢ 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

Tactic:
nth_rw 1 [Eq.comm, ← Iic_union_Ioc_eq_Iic hab, prod_union (Iic_disjoint_Ioc le_rfl)]

Premises used: le_rfl, Finset.Iic_union_Ioc_eq_Iic, Finset.prod_union, Finset.Iic_disjoint_Ioc, 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 : ℕ
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)
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)) ⋯ 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)

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 : ℕ
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)

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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
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)
⊢ 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:
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 : ℕ
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)

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 : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
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)) ⋯ s i))
        1 x)
⊢ 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)

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 : ℕ
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∞)
inl₂ 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∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) (↑(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)

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

Premises used: Finset.Ioc_subset_Iic_self, Finset.restrict₂, Function.extend_val_apply
-- Module: Mathlib.Probability.ProductMeasure
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)
inr₂ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) Prod.fst
⊢ 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:
rw [IicProdIoc_le hba, ← Measure.map_map, ← Measure.fst, Measure.fst_prod]

Premises used: MeasureTheory.Measure.fst_prod, MeasureTheory.Measure.map_map, IicProdIoc_le, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.ProductMeasure
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 (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:
isProjectiveMeasureFamily_pi μ (Iic a) (Iic b) (Iic_subset_Iic.2 hba) |>.symm

Premises used: Iff.mpr, Set.Mem, setOf, MeasureTheory.isProjectiveMeasureFamily_pi, Finset.Iic_subset_Iic, Preorder.frestrictLe₂, Finset.Iic, 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 : ℕ
hba : b ≤ a
⊢ 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:
exact isProjectiveMeasureFamily_pi μ (Iic a) (Iic b) (Iic_subset_Iic.2 hba) |>.symm

Premises used: Iff.mpr, MeasureTheory.isProjectiveMeasureFamily_pi, Finset.Iic_subset_Iic, Finset.Iic, 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 : ℕ
hba : b ≤ a
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) hba)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) Prod.fst

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

Tactic:
(Measure.pi_eq fun s hs ↦ ?_).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)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
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∞)
⊢ 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 : ℕ))

Tactic:
refine (Measure.pi_eq fun s hs ↦ ?_).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)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X (↑i : ℕ))
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
rw : Subsingleton ↥{n + 1}
⊢ Subsingleton ↥(Ioc n (n + 1))

Tactic:
rw [Nat.Ioc_succ_singleton]

Premises used: Nat.Ioc_succ_singleton
-- Module: Mathlib.Probability.ProductMeasure
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 ↥{n + 1}

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

Tactic:
have : Subsingleton (Ioc n (n + 1)) := by rw [Nat.Ioc_succ_singleton]; infer_instance
-- Module: Mathlib.Probability.ProductMeasure
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)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ n < n + 1 ∧ n + 1 ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Probability.ProductMeasure
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)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ Measurable.{u_1, u_1} (α := X (n + 1)) (β := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
    (⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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)
this : Subsingleton ↥(Ioc n (n + 1))
rw :
  Eq (α := ℝ≥0∞)
    (((μ (n + 1) : Measure (X (n + 1))) : (a : Set (X (n + 1))) → ℝ≥0∞)
        ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
          Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ))) :
          (a : Set (X (↑⟨n + 1, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯)) :
      ℝ≥0∞)
⊢ 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:
rw [Fintype.prod_subsingleton _ ⟨n + 1, mem_Ioc.2 (by lia)⟩,
    Measure.map_apply (by fun_prop) (.univ_pi hs)]

Premises used: MeasureTheory.Measure.map_apply, Fintype.prod_subsingleton, MeasurableSet.univ_pi
-- Module: Mathlib.Probability.ProductMeasure
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)
this : Subsingleton ↥(Ioc n (n + 1))
h :
  ∀ (x : X (n + 1)),
    Membership.mem (γ := Set (X (n + 1)))
        ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
          Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s)
        x ↔
      Membership.mem (γ := Set (X (n + 1)))
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) :
          Set (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ)))
        x
⊢ Eq (α := ℝ≥0∞)
    (((μ (n + 1) : Measure (X (n + 1))) : (a : Set (X (n + 1))) → ℝ≥0∞)
        ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
          Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ))) :
          (a : Set (X (↑⟨n + 1, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯)) :
      ℝ≥0∞)

Tactic:
congr 1 with x
-- Module: Mathlib.Probability.ProductMeasure
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)
this : Subsingleton ↥(Ioc n (n + 1))
x : X (n + 1)
h :
  (∀ (a : ℕ) (b : a = n + 1),
      Membership.mem (α := X a) (γ := Set (X a))
        (s (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) :
          Set (X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) : ℕ)))
        ((piSingleton (X := X) n : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) x
            (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) :
          X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) : ℕ))) ↔
    Membership.mem (γ := Set (X (n + 1)))
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) :
        Set (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ)))
      x
⊢ Membership.mem (γ := Set (X (n + 1)))
      ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
        Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s)
      x ↔
    Membership.mem (γ := Set (X (n + 1)))
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) :
        Set (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ)))
      x

Tactic:
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, forall_const, Subtype.forall,
    Nat.Ioc_succ_singleton, mem_singleton]

Premises used: Finset.mem_singleton, Nat.Ioc_succ_singleton, Subtype.forall, Set.mem_pi, Set.mem_univ, forall_const, Set.mem_preimage