awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
inr :
  ∀
    (this :
      ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i))
        [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Set ι} (hs : Countable.{u_1 + 1} (↑s : Type u_1))
        {t : (i : ι) → Set (X i)} (mt : ∀ i ∈ s, MeasurableSet (t i)) (s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)),
        Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
          (∏' (i : (↑s : Type u_1)),
              ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
            ℝ≥0∞))
    (s_ne : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)),
    Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
      (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
    (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
      ℝ≥0∞)
have wlog : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i))
  [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Set ι} (hs : Countable.{u_1 + 1} (↑s : Type u_1))
  {t : (i : ι) → Set (X i)} (mt : ∀ i ∈ s, MeasurableSet (t i)) (s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)),
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
    (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
      ℝ≥0∞)
Tactic: wlog s_ne : Nonempty s
Cleared hypotheses: hμ, s, hs, t, mt
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
    (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
      ℝ≥0∞)
have ha : Tendsto (β := ℝ≥0∞)
  (fun (s' : Finset (↑s : Type u_1)) ↦
    (∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥0∞))
  atTop (𝓝 ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t)) : Filter ℝ≥0∞)
Tactic: apply tendsto_nhds_unique (f := fun s' : Finset s ↦ ∏ i ∈ s', μ i (t i)) (l := atTop)
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
ha :
  Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      (∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥0∞))
    atTop (𝓝 ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t)) : Filter ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
    (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
      ℝ≥0∞)
have hb : Tendsto (β := ℝ≥0∞)
  (fun (s' : Finset (↑s : Type u_1)) ↦
    ∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
  atTop
  (𝓝 (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι))))
Tactic: apply tendsto_nhds_unique (f := fun s' : Finset s ↦ ∏ i ∈ s', μ i (t i)) (l := atTop)
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
s' : Finset (↑s : Type u_1)
| (∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥0∞)
have rw : ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
    ((↑(image (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) s') : Set ι).pi (α := X) fun (i : ι) ↦
      if h : i ∈ s then t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι) else Set.univ) :
  ℝ≥0∞)
Tactic: rw [← infinitePi_pi _ (by measurability), ← infinitePi_map_restrict', map_apply
        (by fun_prop) (by apply MeasurableSet.pi (countable_toSet _) (by measurability)),
        restrict_preimage]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
s' : Finset (↑s : Type u_1)
| ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
      ((↑(image (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) s') : Set ι).pi (α := X) fun (i : ι) ↦
        if h : i ∈ s then t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι) else Set.univ) :
    ℝ≥0∞)
have simp : ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
    ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
      if i ∈ s then t i else Set.univ) :
  ℝ≥0∞)
Tactic: simp only [coe_image, dite_eq_ite]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
s' : Finset (↑s : Type u_1)
| (∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥0∞)
have rw : ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
    ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
      if i ∈ s then t i else Set.univ) :
  ℝ≥0∞)
Tactic: rw [← infinitePi_pi _ (by measurability), ← infinitePi_map_restrict', map_apply
        (by fun_prop) (by apply MeasurableSet.pi (countable_toSet _) (by measurability)),
        restrict_preimage]
      simp only [coe_image, dite_eq_ite]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      (∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥0∞))
    atTop (𝓝 ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t)) : Filter ℝ≥0∞)
have ha : Tendsto (β := ℝ≥0∞)
  (fun (s' : Finset (↑s : Type u_1)) ↦
    ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
          if i ∈ s then t i else Set.univ) :
      ℝ≥0∞))
  atTop (𝓝 ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t)) : Filter ℝ≥0∞)
Tactic: conv in ∏ _ ∈ _, _ =>
      rw [← infinitePi_pi _ (by measurability), ← infinitePi_map_restrict', map_apply
        (by fun_prop) (by apply MeasurableSet.pi (countable_toSet _) (by measurability)),
        restrict_preimage]
      simp only [coe_image, dite_eq_ite]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
have rw : s.pi (α := X) t = s.pi (α := X) fun (i : ι) ↦ if i ∈ s then t i else Set.univ
Tactic: rw [← Set.pi_iUnion_eq_iInter_pi, Set.iUnion_finset_eq_set]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
          ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
            if i ∈ s then t i else Set.univ) :
        ℝ≥0∞))
    atTop (𝓝 ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t)) : Filter ℝ≥0∞)
have this : s.pi (α := X) t =
  ⋂ (s' : Finset (↑s : Type u_1)),
    (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
      if i ∈ s then t i else Set.univ
Tactic: have : s.pi t
      = ⋂ s' : Finset s,
        (Subtype.val '' (s' : Set s)).pi (fun i ↦ if i ∈ s then t i else Set.univ) := by
      rw [← Set.pi_iUnion_eq_iInter_pi, Set.iUnion_finset_eq_set]
      grind
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
this :
  s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
          ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
            if i ∈ s then t i else Set.univ) :
        ℝ≥0∞))
    atTop (𝓝 ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t)) : Filter ℝ≥0∞)
have ha : Tendsto (β := ℝ≥0∞)
  (fun (s' : Finset (↑s : Type u_1)) ↦
    ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
          if i ∈ s then t i else Set.univ) :
      ℝ≥0∞))
  atTop
  (𝓝
      ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (⋂ (s' : Finset (↑s : Type u_1)),
          (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
            if i ∈ s then t i else Set.univ)) :
    Filter ℝ≥0∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
this :
  s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
          ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
            if i ∈ s then t i else Set.univ) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
          (⋂ (s' : Finset (↑s : Type u_1)),
            (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
              if i ∈ s then t i else Set.univ)) :
      Filter ℝ≥0∞)
have ha : ∀ (i : Finset (↑s : Type u_1)),
  NullMeasurableSet
    ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑i : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
      if i ∈ s then t i else Set.univ)
    (infinitePi (X := X) μ)
Tactic: apply tendsto_measure_iInter_atTop
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
this :
  s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
ha :
  ∀ (i : Finset (↑s : Type u_1)),
    NullMeasurableSet
      ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑i : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ)
      (infinitePi (X := X) μ)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
          ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
            if i ∈ s then t i else Set.univ) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
          (⋂ (s' : Finset (↑s : Type u_1)),
            (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
              if i ∈ s then t i else Set.univ)) :
      Filter ℝ≥0∞)
have ha₁ : Antitone (β := Set ((i : ι) → X i)) fun (s' : Finset (↑s : Type u_1)) ↦
  (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
    if i ∈ s then t i else Set.univ
Tactic: apply tendsto_measure_iInter_atTop
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
this :
  s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
ha :
  ∀ (i : Finset (↑s : Type u_1)),
    NullMeasurableSet
      ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑i : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ)
      (infinitePi (X := X) μ)
ha₁ :
  Antitone (β := Set ((i : ι) → X i)) fun (s' : Finset (↑s : Type u_1)) ↦
    (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
      if i ∈ s then t i else Set.univ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
          ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
            if i ∈ s then t i else Set.univ) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
          (⋂ (s' : Finset (↑s : Type u_1)),
            (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
              if i ∈ s then t i else Set.univ)) :
      Filter ℝ≥0∞)
have ha₂ : ∃ (i : Finset (↑s : Type u_1)),
  Ne (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑i : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
          if i ∈ s then t i else Set.univ) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: apply tendsto_measure_iInter_atTop
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
this :
  s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
⊢ ∀ (i : Finset (↑s : Type u_1)),
    NullMeasurableSet
      ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑i : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ)
      (infinitePi (X := X) μ)
have ha : ∀ (s' : Finset (↑s : Type u_1)), (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).Countable
Tactic: refine fun s' ↦ MeasurableSet.nullMeasurableSet (MeasurableSet.pi ?_ (by measurability))
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    atTop
    (𝓝 (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι))))
have hb : Tendsto (β := ℝ≥0∞)
  (fun (s' : Finset (↑s : Type u_1)) ↦
    ∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
  atTop
  (𝓝
    (⨅ (s_1 : Finset (↑s : Type u_1)),
      ∏ i ∈ s_1, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι))))
Tactic: rw [ENNReal.tprod_eq_iInf_prod (by simp [prob_le_one])]
-- 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)
inst : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ t) : ℝ≥0∞)
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hs : Countable.{u_1 + 1} (↑Set.univ : Type u_1)
Tactic: rw [infinitePi_pi_of_countable, tprod_univ (f := fun i ↦ μ i (t i))]
-- 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)
inst : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
hs : Countable.{u_1 + 1} (↑Set.univ : Type u_1)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ t) : ℝ≥0∞)
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have mt₁ : ∀ (i : ι), Membership.mem (γ := Set ι) Set.univ i → MeasurableSet (t i)
Tactic: rw [infinitePi_pi_of_countable, tprod_univ (f := fun i ↦ μ i (t i))]
-- 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)
inst : Countable ι
inst_1 : ∀ (i : ι), MeasurableSingletonClass.{u_2} (X i)
f : (i : ι) → X i
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) {f})
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i})
have rw : Eq (α := ℝ≥0∞)
  ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ fun (i : ι) ↦ {f i}) : ℝ≥0∞)
  (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i} : ℝ≥0∞)
Tactic: rw [← Set.univ_pi_singleton, infinitePi_pi_univ _ (by measurability)]
-- 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)
inst : Countable ι
inst_1 : ∀ (i : ι), MeasurableSingletonClass.{u_2} (X i)
f : (i : ι) → X i
rw :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ fun (i : ι) ↦ {f i}) : ℝ≥0∞)
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) {f})
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i})
have rw₁ : Eq (α := ℝ≥0∞) (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i}) (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i})
Tactic: rw [← Set.univ_pi_singleton, infinitePi_pi_univ _ (by measurability)]
-- 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)
i : ι
⊢ map (Function.eval (β := X) i) (infinitePi (X := X) μ) = μ i
have h : ∀ (s : Set (X i)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((map (Function.eval (β := X) i) (infinitePi (X := X) μ) : Measure (X i)) : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ i : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs