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)
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)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have conv : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦
    (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
        (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
      (B n))
  atTop (𝓝 0)
Tactic: conv =>
    enter [1]; ext n
    rw [A_eq, piContent_cylinder μ (mS n), ← pi_map_piCongrLeft (aux n),
      map_apply (by fun_prop) (mS n)]
    change (Measure.pi (fun i : t n ↦ μ i)) (T n)
    rw [← piContent_cylinder (fun i : u ↦ μ i) (mT n), ← B_eq n]
-- 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)
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)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (B n))
    atTop (𝓝 0)
have inl : ∀ (u_fin : Finite.{u_1 + 1} (↑u : Type u_1)),
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (B n))
    atTop (𝓝 0)
Tactic: obtain u_fin | u_inf := finite_or_infinite u
-- 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)
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)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_fin : Finite.{u_1 + 1} (↑u : Type u_1)
x : Fintype (↑u : Type u_1) := Fintype.ofFinite (↑u : Type u_1)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((Measure.pi (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (⋂ (n : ℕ), B n) :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) 0
  ((Measure.pi (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
      (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
    ∅)
Tactic: rw [B_inter, measure_empty]
-- 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)
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)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_fin : Finite.{u_1 + 1} (↑u : Type u_1)
x : Fintype (↑u : Type u_1) := Fintype.ofFinite (↑u : Type u_1)
h :
  Eq (α := ℝ≥0∞) 0
    ((Measure.pi (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
        (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
      ∅)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((Measure.pi (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (⋂ (n : ℕ), B n) :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [B_inter, measure_empty]
-- 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)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_inf : Infinite.{u_1 + 1} (↑u : Type u_1)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (B n))
    atTop (𝓝 0)
have count_u : Countable.{u_1 + 1} (↑u : Type u_1)
Tactic: have count_u : Countable u := Set.countable_iUnion (fun n ↦ (s n).countable_toSet)
-- 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)
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)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_inf : Infinite.{u_1 + 1} (↑u : Type u_1)
count_u : Countable.{u_1 + 1} (↑u : Type u_1)
φ : ℕ ≃ (↑u : Type u_1)
| Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (B n))
    atTop (𝓝 0)
have enter : fun (n : ℕ) ↦
  (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
      (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
    (B n)
Tactic: enter [1]
-- 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)
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)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_inf : Infinite.{u_1 + 1} (↑u : Type u_1)
count_u : Countable.{u_1 + 1} (↑u : Type u_1)
φ : ℕ ≃ (↑u : Type u_1)
| fun (n : ℕ) ↦
    (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
        (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
      (B n)
have h : ∀ (n : ℕ),
  ((piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
        (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
      (B n) :
    ℝ≥0∞)
Tactic: ext n
-- 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)
⊢ (piContent (X := X) μ).IsSigmaSubadditive (C := measurableCylinders X)
have refine : ∀ (f : ℕ → Set ((i : ι) → X i)) (hf : ∀ (i : ℕ), f i ∈ measurableCylinders X)
  (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X) (hf' : Pairwise (Function.onFun Disjoint f)),
  Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)
-- 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 : Finset ι
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ι))) (map (I.restrict (π := X)) (infinitePi (X := X) μ))
    ((fun (I : Finset ι) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : Measure ((i : ↥I) → X (↑i : ι))))
      I)
have h : ∀ (s : Set ((i : ↥I) → X (↑i : ι))) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞) s : ℝ≥0∞)
    (((fun (I : Finset ι) ↦
              (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : Measure ((i : ↥I) → X (↑i : ι))))
            I :
          (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s hs