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

Tactic:
simp [Set.not_nonempty_iff_eq_empty'.mp s_ne]

Premises used: Set.not_nonempty_iff_eq_empty', Iff.mp
-- Module: Mathlib.Probability.ProductMeasure
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∞)
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 : ι))))
⊢ 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:
apply tendsto_nhds_unique (f := fun s' : Finset s ↦ ∏ i ∈ s', μ i (t i)) (l := atTop)

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Probability.ProductMeasure
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', MeasurableSet (α := X (↑i : ι)) (t (↑i : ι))

Tactic:
measurability
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ Measurable (α := (a : ι) → X a) (s.restrict (π := X))

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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' : Set (↑s : Type u_1)), MeasurableSet (α := X (↑i : ι)) (t (↑i : ι))

Tactic:
measurability
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ MeasurableSet (α := (a : (↑s : Type u_1)) → X (↑a : ι))
    ((↑s' : Set (↑s : Type u_1)).pi (α := fun (i : (↑s : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑s : Type u_1)) ↦
      t (↑i : ι))

Tactic:
apply MeasurableSet.pi (countable_toSet _) (by measurability)

Premises used: Finset.countable_toSet, MeasurableSet.pi
-- Module: Mathlib.Probability.ProductMeasure
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)
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∞)
| (∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥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]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.infinitePi_pi, Finset.restrict_preimage, MeasureTheory.Measure.infinitePi_map_restrict'
-- Module: Mathlib.Probability.ProductMeasure
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)
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∞)
| ((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:
simp only [coe_image, dite_eq_ite]

Premises used: Finset.coe_image, dite_eq_ite
-- Module: Mathlib.Probability.ProductMeasure
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)
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∞)
| (∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥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]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.infinitePi_pi, Finset.coe_image, Finset.restrict_preimage, dite_eq_ite, MeasureTheory.Measure.infinitePi_map_restrict'
-- Module: Mathlib.Probability.ProductMeasure
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)) ↦
      ((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∞)
⊢ 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:
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]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.infinitePi_pi, Finset.coe_image, Finset.restrict_preimage, dite_eq_ite, MeasureTheory.Measure.infinitePi_map_restrict'
-- Module: Mathlib.Probability.ProductMeasure
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)
rw : s.pi (α := X) t = s.pi (α := X) fun (i : ι) ↦ if i ∈ s then t i else Set.univ
⊢ 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:
rw [← Set.pi_iUnion_eq_iInter_pi, Set.iUnion_finset_eq_set]

Premises used: Set.iUnion_finset_eq_set, Set.pi_iUnion_eq_iInter_pi
-- Module: Mathlib.Probability.ProductMeasure
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.pi (α := X) fun (i : ι) ↦ if i ∈ s then t i else Set.univ

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

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
-- Module: Mathlib.Probability.ProductMeasure
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 :
  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∞)
⊢ 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:
rw [this]
-- Module: Mathlib.Probability.ProductMeasure
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
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∞)
⊢ 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:
apply tendsto_measure_iInter_atTop

Premises used: MeasureTheory.tendsto_measure_iInter_atTop
-- Module: Mathlib.Probability.ProductMeasure
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
s' : Finset (↑s : Type u_1)
⊢ ∀ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s }),
    MeasurableSet (if i ∈ s then t i else Set.univ)

Tactic:
measurability
-- Module: Mathlib.Probability.ProductMeasure
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 :
  ∀ (s' : Finset (↑s : Type u_1)), (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).Countable
⊢ ∀ (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:
refine fun s' ↦ MeasurableSet.nullMeasurableSet (MeasurableSet.pi ?_ (by measurability))

Premises used: MeasurableSet.nullMeasurableSet, MeasurableSet.pi
-- Module: Mathlib.Probability.ProductMeasure
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
s' : Finset (↑s : Type u_1)
⊢ (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).Countable

Tactic:
(Finset.countable_toSet _).image _

Premises used: Set.Countable.image, Finset.countable_toSet
-- Module: Mathlib.Probability.ProductMeasure
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
s' : Finset (↑s : Type u_1)
⊢ (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set { x : ι // x ∈ s })).Countable

Tactic:
exact (Finset.countable_toSet _).image _

Premises used: Set.Countable.image, Finset.countable_toSet
-- Module: Mathlib.Probability.ProductMeasure
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
a : Finset (↑s : Type u_1)
ha :
  ∀ ⦃b : Finset (↑s : Type u_1)⦄,
    a ≤ b →
      LE.le (α := 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 :
              Set ((i : ι) → X i)))
          b)
        ((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 :
              Set ((i : ι) → X i)))
          a)
⊢ ∀ ⦃b : Finset (↑s : Type u_1)⦄,
    a ≤ b →
      LE.le (α := 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 :
              Set ((i : ι) → X i)))
          b)
        ((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 :
              Set ((i : ι) → X i)))
          a)

Tactic:
_
-- Module: Mathlib.Probability.ProductMeasure
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
a b : Finset (↑s : Type u_1)
h : a ≤ b
⊢ ∀ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑a : Set (↑s : Type u_1)),
    (if i ∈ s then t i else Set.univ) ⊆ if i ∈ s then t i else Set.univ

Tactic:
simp
-- Module: Mathlib.Probability.ProductMeasure
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
a b : Finset (↑s : Type u_1)
h : a ≤ b
⊢ LE.le (α := 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 :
          Set ((i : ι) → X i)))
      b)
    ((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 :
          Set ((i : ι) → X i)))
      a)

Tactic:
simpa using Set.pi_mono' (by simp) (Set.image_mono h)

Premises used: Set.image_mono, Set.pi_mono'