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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := X) I S ∈ measurableCylinders X
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦ X ((e : (a : ℕ) → ι) (↑i : ℕ)))
              fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦ μ ((e : (a : ℕ) → ι) (↑i : ℕ)) :
            Measure ((i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → X ((e : (a : ℕ) → ι) (↑i : ℕ)))) :
          (a :
              Set
                ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι))) →
            ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft.{u_2 + 1, 1, u_1 + 1} (fun (b : ↥I) ↦ X (↑b : ι)) (e.restrictPreimageFinset I) :
                ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                    X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) ≃
                  ((b : ↥I) → X (↑b : ι))) :
            (a :
                (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) →
              (b : ↥I) → X (↑b : ι)) ⁻¹'
          S) :
      ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) i) : ι))
              fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦
              μ (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) i) : ι) :
            Measure
              ((i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) i) : ι))) :
          (a :
              Set
                ((b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι))) →
            ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft.{u_2 + 1, 1, u_1 + 1} (fun (i : ↥I) ↦ X (↑i : ι)) (e.restrictPreimageFinset I) :
                ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                    X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) ≃
                  ((b : ↥I) → X (↑b : ι))) :
            (a :
                (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) →
              (b : ↥I) → X (↑b : ι)) ⁻¹'
          S) :
      ℝ≥0∞)

Tactic:
simp
-- 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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := X) I S ∈ measurableCylinders X
⊢ Measurable (α :=
    (b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
      X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι))
    (β := (i : ↥I) → X (↑i : ι))
    (⇑(piCongrLeft.{0, u_1, u_2} (fun (i : ↥I) ↦ X (↑i : ι)) (e.restrictPreimageFinset I) :
          ((b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι)) ≃ᵐ
            ((a : ↥I) → X (↑a : ι))) :
      (a :
          (b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
            X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι)) →
        (a : ↥I) → X (↑a : ι))

Tactic:
fun_prop
-- 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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := X) I S ∈ measurableCylinders X
⊢ Measurable.{u_2, u_2} (α := (n : ℕ) → X ((e : (a : ℕ) → ι) n))
    ((I.preimage (⇑e : (a : ℕ) → ι) ⋯).restrict (π := fun (i : ℕ) ↦ X ((e : (a : ℕ) → ι) i)))

Tactic:
fun_prop
-- 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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := X) I S ∈ measurableCylinders X
⊢ Measurable (α := (b : ℕ) → X ((e : (a : ℕ) → ι) b)) (β := (i : ι) → X i)
    (⇑(piCongrLeft X e) : (a : (b : ℕ) → X ((e : (a : ℕ) → ι) b)) → (a : ι) → X a)

Tactic:
fun_prop
-- 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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := X) I S ∈ measurableCylinders X
⊢ Measurable (α :=
    (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
      X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι))
    (β := (i : ↥I) → X (↑i : ι))
    (⇑(Equiv.piCongrLeft.{u_2 + 1, 1, u_1 + 1} (fun (b : ↥I) ↦ X (↑b : ι)) (e.restrictPreimageFinset I) :
          ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) ≃
            ((b : ↥I) → X (↑b : ι))) :
      (a :
          (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
            X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) →
        (b : ↥I) → X (↑b : ι))

Tactic:
fun_prop
-- 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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := X) I S ∈ measurableCylinders X
⊢ MeasurableSet.{u_2} (α :=
    (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
      X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι))
    ((⇑(Equiv.piCongrLeft.{u_2 + 1, 1, u_1 + 1} (fun (b : ↥I) ↦ X (↑b : ι)) (e.restrictPreimageFinset I) :
            ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) ≃
              ((b : ↥I) → X (↑b : ι))) :
        (a :
            (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) →
          (b : ↥I) → X (↑b : ι)) ⁻¹'
      S)

Tactic:
exact hS.preimage (by fun_prop)

Premises used: MeasurableSet.preimage
-- 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)
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) ∅
⊢ ∀ (i : ι), Nonempty.{u_2 + 1} (X i)

Tactic:
have : ∀ i, Nonempty (X i) := fun i ↦ nonempty_of_isProbabilityMeasure (μ i)
-- 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)
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)
⊢ ∀ (n : ℕ), ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ A n = cylinder (α := X) s S

Tactic:
have A_cyl n : ∃ s S, MeasurableSet S ∧ A n = cylinder s S :=
    (mem_measurableCylinders _).1 (A_mem n)
-- 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)
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
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)
⊢ 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
-- 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)
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
n : ℕ
i : ↥(t n)
⊢ (fun (i : ↥(s n)) ↦
        (Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯ :
          ↥(t n)))
      ((fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯) i) =
    i

Tactic:
simp
-- 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)
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
n : ℕ
i : ↥(s n)
⊢ (fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯)
      ((fun (i : ↥(s n)) ↦
          (Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯ :
            ↥(t n)))
        i) =
    i

Tactic:
simp
-- 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)
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 : ℕ
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
⊢ (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:
ext x i
-- 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)
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)
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 : ι) ⋯) : X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) : ι))
⊢ ((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:
simp only [Function.comp_apply, Finset.restrict,
      Equiv.piCongrLeft_apply, Equiv.coe_fn_symm_mk, f, aux, g, t]

Premises used: Equiv.piCongrLeft_apply, Equiv.coe_fn_symm_mk, Finset.restrict, Function.comp_apply
-- 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)
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)
h h₁ :
  Eq (α := X (↑i : ι))
    (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) : X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) : ι))
    (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯))
⊢ 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 : ι) ⋯) : ι))

Tactic:
rw [dif_pos (Set.mem_iUnion.2 ⟨n, i.2⟩)]

Premises used: Iff.mpr, Set.mem_iUnion, dif_pos, Exists.intro
-- 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)
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))

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⟩)]
-- 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)
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 : ℕ
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)
⊢ B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)

Tactic:
simp_rw [B, A_eq, cylinder, ← Set.preimage_comp, r_comp_f]

Premises used: Set.preimage_comp, MeasureTheory.cylinder