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)
A_cyl : ∀ (n : ℕ), ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ A n = cylinder (α := X) s S
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have choose : ∀ (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)),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
Tactic: choose s S mS A_eq using A_cyl
Cleared hypotheses: A_cyl
-- 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)
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))
have h : ∀ (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(s n)),
  ((s n).restrict (π := X) ∘ f) x i =
    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))) x i
Tactic: ext x 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)
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)
n : ℕ
x : (i : (↑u : Type u_1)) → X (↑i : ι)
i : ↥(s n)
⊢ ((s n).restrict (π := X) ∘ f) x i =
    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))) x i
have h : Eq (α := X (↑i : ι))
  (if hi : (↑i : ι) ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) hi) else Classical.ofNonempty :
    X (↑i : ι))
  (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) sorry) : X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) sorry) : ι))
Tactic: simp only [Function.comp_apply, Finset.restrict,
      Equiv.piCongrLeft_apply, Equiv.coe_fn_symm_mk, f, aux, g, t]
-- 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)
n : ℕ
x : (i : (↑u : Type u_1)) → X (↑i : ι)
i : ↥(s n)
⊢ Eq (α := X (↑i : ι))
    (if hi : (↑i : ι) ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) hi) else Classical.ofNonempty :
      X (↑i : ι))
    (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) : X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) : ι))
have h : Eq (α := X (↑i : ι))
  (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) sorry) : X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) sorry) : ι))
  (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) sorry))
Tactic: rw [dif_pos (Set.mem_iUnion.2 ⟨n, i.2⟩)]
-- 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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have 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))
Tactic: have r_comp_f n : (s n).restrict ∘ f = (g n) ∘ (fun (x : Π i : u, X i) i ↦ x i) := by
    ext x i
    simp only [Function.comp_apply, Finset.restrict,
      Equiv.piCongrLeft_apply, Equiv.coe_fn_symm_mk, f, aux, g, t]
    rw [dif_pos (Set.mem_iUnion.2 ⟨n, i.2⟩)]
-- 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
n : ℕ
⊢ B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
have simp_rw : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι)))
  ((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))) ⁻¹'
    S n)
  ((t n).restrict (π := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) ⁻¹' T n)
Tactic: simp_rw [B, A_eq, cylinder, ← Set.preimage_comp, r_comp_f]
-- 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
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
Tactic: have B_eq n : B n = cylinder (t n) (T n) := by
    simp_rw [B, A_eq, cylinder, ← Set.preimage_comp, r_comp_f]; rfl
-- 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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have mT : ∀ (n : ℕ), MeasurableSet (T n)
Tactic: have mT n : MeasurableSet (T n) := (mS n).preimage (by fun_prop)
-- 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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have 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)
Tactic: have B_mem n : B n ∈ measurableCylinders (fun i : u ↦ X i) :=
    (mem_measurableCylinders (B n)).2 ⟨t n, T n, mT n, B_eq n⟩
-- 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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have mB : ∀ (n : ℕ), MeasurableSet (B n)
Tactic: have mB n : MeasurableSet (B n) := .of_mem_measurableCylinders (B_mem n)