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 : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
pos :
  ∀ (hs : s.Nonempty),
    Eq (α := ℝ≥0∞)
      ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                    (restrict₂ (π := X) ⋯) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                    (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have neg : ∀ (hs : ¬s.Nonempty),
  Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) sorry) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: by_cases hs : s.Nonempty
-- 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
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
hs : s.Nonempty
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have rw : IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (m0 :=
  MeasurableSpace.pi (X := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)))
  ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
        (restrict₂ (π := X) sorry) :
      (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    x)
Tactic: rw [Subsingleton.eq_univ_of_nonempty hs, @measure_univ .., measure_univ]
-- 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
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
hs : ¬s.Nonempty
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞)
  ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                (restrict₂ (π := X) sorry) :
              (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
            x :
          Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
        (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
      ∅ :
    ℝ≥0∞)
  ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
              (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
            x :
          Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
        (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
      ∅ :
    ℝ≥0∞)
Tactic: rw [Set.not_nonempty_iff_eq_empty.1 hs]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        const ((i : ↥(Iic a)) → X (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b))
have rw : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ
      Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
        (restrict₂ (π := X) sorry))
    (_root_.IicProdIoc (X := X) a b))
  (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ
      const ((i : ↥(Iic a)) → X (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a b))
Tactic: rw [partialTraj_eq_prod, partialTraj_const_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 : ℕ
rw :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
          (restrict₂ (π := X) ⋯))
      (_root_.IicProdIoc (X := X) a b))
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        const ((i : ↥(Iic a)) → X (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b))
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        const ((i : ↥(Iic a)) → X (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b))
have rw₁ : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ
      const ((i : ↥(Iic a)) → X (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a b))
  (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ
      const ((i : ↥(Iic a)) → X (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a b))
Tactic: rw [partialTraj_eq_prod, partialTraj_const_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)
I : Finset ℕ
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ℕ))) (map (I.restrict (π := X)) (infinitePiNat (X := X) μ))
    ((fun (I : Finset ℕ) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ℕ)) fun (i : ↥I) ↦ μ (↑i : ℕ) : Measure ((i : ↥I) → X (↑i : ℕ))))
      I)
have hf : Measurable.{u_1, u_1} (α := ((i : ↥(Iic 0)) → X (↑i : ℕ)) × ((i : ↥(Ioc 0 (I.sup id))) → X (↑i : ℕ)))
  (_root_.IicProdIoc (X := X) 0 (I.sup id))
Tactic: rw [isProjectiveMeasureFamily_pi μ _ _ I.subset_Iic_sup_id,
    ← restrict₂_comp_restrict I.subset_Iic_sup_id, ← map_map, ← frestrictLe, infinitePiNat,
    map_comp, traj_map_frestrictLe, partialTraj_const, ← map_comp, ← compProd_eq_comp_prod,
    compProd_const, pi_prod_map_IicProdIoc]
-- 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)
I : Finset ℕ
hf :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic 0)) → X (↑i : ℕ)) × ((i : ↥(Ioc 0 (I.sup id))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) 0 (I.sup id))
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ℕ))) (map (I.restrict (π := X)) (infinitePiNat (X := X) μ))
    ((fun (I : Finset ℕ) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ℕ)) fun (i : ↥I) ↦ μ (↑i : ℕ) : Measure ((i : ↥I) → X (↑i : ℕ))))
      I)
have hf₁ : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (frestrictLe (π := X) (I.sup id))
Tactic: rw [isProjectiveMeasureFamily_pi μ _ _ I.subset_Iic_sup_id,
    ← restrict₂_comp_restrict I.subset_Iic_sup_id, ← map_map, ← frestrictLe, infinitePiNat,
    map_comp, traj_map_frestrictLe, partialTraj_const, ← map_comp, ← compProd_eq_comp_prod,
    compProd_const, pi_prod_map_IicProdIoc]
-- 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)
I : Finset ℕ
hf :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic 0)) → X (↑i : ℕ)) × ((i : ↥(Ioc 0 (I.sup id))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) 0 (I.sup id))
hf₁ :
  Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ))
    (frestrictLe (π := X) (I.sup id))
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ℕ))) (map (I.restrict (π := X)) (infinitePiNat (X := X) μ))
    ((fun (I : Finset ℕ) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ℕ)) fun (i : ↥I) ↦ μ (↑i : ℕ) : Measure ((i : ↥I) → X (↑i : ℕ))))
      I)
have hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
Tactic: rw [isProjectiveMeasureFamily_pi μ _ _ I.subset_Iic_sup_id,
    ← restrict₂_comp_restrict I.subset_Iic_sup_id, ← map_map, ← frestrictLe, infinitePiNat,
    map_comp, traj_map_frestrictLe, partialTraj_const, ← map_comp, ← compProd_eq_comp_prod,
    compProd_const, pi_prod_map_IicProdIoc]
-- 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)
I : Finset ℕ
hf :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic 0)) → X (↑i : ℕ)) × ((i : ↥(Ioc 0 (I.sup id))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) 0 (I.sup id))
hf₁ :
  Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ))
    (frestrictLe (π := X) (I.sup id))
hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ℕ))) (map (I.restrict (π := X)) (infinitePiNat (X := X) μ))
    ((fun (I : Finset ℕ) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ℕ)) fun (i : ↥I) ↦ μ (↑i : ℕ) : Measure ((i : ↥I) → X (↑i : ℕ))))
      I)
have hf₂ : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Iic (I.sup id)).restrict (π := X))
Tactic: rw [isProjectiveMeasureFamily_pi μ _ _ I.subset_Iic_sup_id,
    ← restrict₂_comp_restrict I.subset_Iic_sup_id, ← map_map, ← frestrictLe, infinitePiNat,
    map_comp, traj_map_frestrictLe, partialTraj_const, ← map_comp, ← compProd_eq_comp_prod,
    compProd_const, pi_prod_map_IicProdIoc]
-- 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 : Set ((n : ℕ) → X n)
hA : A ∈ measurableCylinders X
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) A : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) A : ℝ≥0∞)
have obtain : ∀ (s : Finset ℕ) (S : Set ((i : ↥s) → X (↑i : ℕ))) (mS : MeasurableSet S)
  (hA : cylinder (α := X) s S ∈ measurableCylinders X),
  Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
Tactic: obtain ⟨s, S, mS, rfl⟩ : ∃ s S, MeasurableSet S ∧ A = cylinder s S := by
    simpa [mem_measurableCylinders] using hA
Cleared hypotheses: A, hA
-- 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)
s : Finset ℕ
S : Set ((i : ↥s) → X (↑i : ℕ))
mS : MeasurableSet S
hA : cylinder (α := X) s S ∈ measurableCylinders X
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
        (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
  ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
Tactic: rw [piContent_cylinder _ mS, cylinder, ← map_apply (measurable_restrict _) mS,
    infinitePiNat_map_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)
s : Finset ℕ
S : Set ((i : ↥s) → X (↑i : ℕ))
mS : MeasurableSet S
hA : cylinder (α := X) s S ∈ measurableCylinders X
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
        (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
  ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
Tactic: rw [piContent_cylinder _ mS, cylinder, ← map_apply (measurable_restrict _) mS,
    infinitePiNat_map_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)
s : Finset ℕ
S : Set ((i : ↥s) → X (↑i : ℕ))
mS : MeasurableSet S
hA : cylinder (α := X) s S ∈ measurableCylinders X
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞)
  (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
        (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
  (((map (s.restrict (π := X)) (infinitePiNat (X := X) μ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
        (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
Tactic: rw [piContent_cylinder _ mS, cylinder, ← map_apply (measurable_restrict _) mS,
    infinitePiNat_map_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)
s : Finset ℕ
S : Set ((i : ↥s) → X (↑i : ℕ))
mS : MeasurableSet S
hA : cylinder (α := X) s S ∈ measurableCylinders X
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    (((map (s.restrict (π := X)) (infinitePiNat (X := X) μ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞)
  (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
        (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
  (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
        (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
Tactic: rw [piContent_cylinder _ mS, cylinder, ← map_apply (measurable_restrict _) mS,
    infinitePiNat_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
s : Set ((i : ι) → X i)
hs : s ∈ measurableCylinders X
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : ℕ) → X ((e : (a : ℕ) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : ℕ) → X ((e : (a : ℕ) → ι) b)) → (a : ι) → X a)
            (infinitePiNat (X := fun (n : ℕ) ↦ X ((e : (a : ℕ) → ι) n)) fun (n : ℕ) ↦ μ ((e : (a : ℕ) → ι) n)) :
          (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
have obtain : ∀ (I : Finset ι) (S : Set ((i : ↥I) → X (↑i : ι))) (hS : MeasurableSet S)
  (hs : cylinder (α := X) I S ∈ measurableCylinders X),
  Eq (α := ℝ≥0∞)
    ((map (α := (b : ℕ) → X ((e : (a : ℕ) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : ℕ) → X ((e : (a : ℕ) → ι) b)) → (a : ι) → X a)
            (infinitePiNat (X := fun (n : ℕ) ↦ X ((e : (a : ℕ) → ι) n)) fun (n : ℕ) ↦ μ ((e : (a : ℕ) → ι) n)) :
          (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        (cylinder (α := X) I S) :
      ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) I S) : ℝ≥0∞)
Tactic: obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders s).1 hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq (α := Set ((i : ι) → X i)) (⋂ (n : ℕ), A n) ∅
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have this : ∀ (i : ι), Nonempty.{u_2 + 1} (X i)
Tactic: have : ∀ i, Nonempty (X i) := fun i ↦ nonempty_of_isProbabilityMeasure (μ i)
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq (α := Set ((i : ι) → X i)) (⋂ (n : ℕ), A n) ∅
this : ∀ (i : ι), Nonempty.{u_2 + 1} (X i)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have A_cyl : ∀ (n : ℕ), ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ A n = cylinder (α := X) s S
Tactic: have A_cyl n : ∃ s S, MeasurableSet S ∧ A n = cylinder s S :=
    (mem_measurableCylinders _).1 (A_mem n)