awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have B_anti : Antitone B
Tactic: have B_anti : Antitone B := fun m n hmn ↦ Set.preimage_mono <| A_anti hmn
-- 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
simp_rw : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), f ⁻¹' A n) ∅
⊢ Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
have simp_rw₁ : f ⁻¹' ⋂ (i : ℕ), A i = ∅
Tactic: simp_rw [B, ← Set.preimage_iInter, A_inter, Set.preimage_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
simp_rw : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), f ⁻¹' A n) ∅
simp_rw₁ : f ⁻¹' ⋂ (i : ℕ), A i = ∅
⊢ Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
have simp_rw₂ : f ⁻¹' ∅ = ∅
Tactic: simp_rw [B, ← Set.preimage_iInter, A_inter, Set.preimage_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
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
Tactic: have B_inter : ⋂ n, B n = ∅ := by
    simp_rw [B, ← Set.preimage_iInter, A_inter, Set.preimage_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) ∅
| Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have enter : fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A 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) ∅
| fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)
have h : ∀ (n : ℕ), ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A 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)
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) ∅
n : ℕ
| ((Measure.pi (α := fun (i : ↥(t n)) ↦ X (↑(↑i : (↑u : Type u_1)) : ι)) fun (i : ↥(t n)) ↦
          μ (↑(↑i : (↑u : Type u_1)) : ι) :
        (a : Set ((i : ↥(t n)) → X (↑(↑i : (↑u : Type u_1)) : ι))) → ℝ≥0∞)
      (T n) :
    ℝ≥0∞)
have h : ((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: 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 := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
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: 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]