awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
have : SigmaFinite (μ.trim hτ.measurableSpace_le) :=
    sigmaFiniteTrim_mono _ (hτ.measurableSpace_min hσ ▸ inf_le_left)
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[f | hτ.measurableSpace]

Tactic:
(condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min hσ).measurableSpace_le (hτ.measurableSet_le_stopping_time hσ) fun t => ?_).symm

Premises used: MeasureTheory.IsStoppingTime.min, MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.IsStoppingTime.measurableSpace_le, Filter.EventuallyEq.symm, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
refine : ∀ (t : Set Ω), MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[f | hτ.measurableSpace]

Tactic:
refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min hσ).measurableSpace_le (hτ.measurableSet_le_stopping_time hσ) fun t => ?_).symm

Premises used: MeasureTheory.IsStoppingTime.min, MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.IsStoppingTime.measurableSpace_le, Filter.EventuallyEq.symm, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_7 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
rw : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
rw₁ rw₂ : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
⊢ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)

Tactic:
rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_iff hσ]

Premises used: MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff, Set.inter_comm
-- 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)
⊢ IsProjectiveMeasureFamily (α := X) fun (I : Finset ι) ↦
    Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)

Tactic:
fun I J hJI ↦ Measure.pi_eq (fun s ms ↦ ?_)

Premises used: MeasureTheory.Measure.pi_eq, MeasureTheory.IsProjectiveMeasureFamily
-- 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)
refine :
  ∀ (I J : Finset ι) (hJI : J ⊆ I) (s : (i : ↥J) → Set (X (↑i : ι))) (ms : ∀ (i : ↥J), MeasurableSet (s i)),
    Eq (α := ℝ≥0∞)
      ((Measure.map (restrict₂ (π := X) hJI)
              ((fun (I : Finset ι) ↦
                  (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                    Measure ((i : ↥I) → X (↑i : ι))))
                I) :
            (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
          (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
        ℝ≥0∞)
      (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ IsProjectiveMeasureFamily (α := X) fun (I : Finset ι) ↦
    Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)

Tactic:
refine fun I J hJI ↦ Measure.pi_eq (fun s ms ↦ ?_)

Premises used: MeasureTheory.Measure.pi_eq
-- 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)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
simp_rw :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ I,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
    (∏ x ∈ J,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
        (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]

Premises used: Finset.prod_eq_prod_extend, Finset.measurable_restrict₂, MeasureTheory.Measure.map_apply, Finset.restrict₂_preimage, MeasureTheory.Measure.pi_pi, MeasurableSet.univ_pi
-- 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)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ I,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
    (∏ x ∈ J,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
        (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)

Tactic:
(prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm

Premises used: Eq.symm, Finset.prod_subset_one_on_sdiff
-- 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)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
refine_1 :
  ∀ (x : ι) (hx : x ∈ I \ J),
    Eq (α := ℝ≥0∞)
      (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
      1
refine_2 :
  ∀ (x : ι) (hx : x ∈ J),
    Eq (α := ℝ≥0∞)
      (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
        (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
      (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ I,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
    (∏ x ∈ J,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
        (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)

Tactic:
refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm

Premises used: Eq.symm, Finset.prod_subset_one_on_sdiff
-- 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)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ I \ J
refine_1 :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
          Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
        (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
      (if h : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) ∈ J then
        s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) h)
      else Set.univ))
    1
refine_1₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
        Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
refine_1₂ refine_1₃ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
    1

Tactic:
rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, dif_neg, Finset.mem_sdiff, And.right, And.left, Iff.mp, Function.extend_val_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)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
refine_2 :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
          (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
      ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x :
      ℝ≥0∞)
refine_2₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
          (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
        (if h : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) ∈ J then
          s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) h)
        else Set.univ) :
      ℝ≥0∞)
refine_2₂ refine_2₃ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx) : ι))) :
          (a : Set (X (↑⟨x, hx⟩ : ι))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) x hx)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) :
            Measure (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ι))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) x ⋯) : ι) hx)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)

Tactic:
rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]

Premises used: dif_pos, Function.extend_val_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)
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) I S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥I) ↦ X (↑i : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)

Tactic:
projectiveFamilyContent_cylinder _ hS

Premises used: MeasureTheory.projectiveFamilyContent_cylinder
-- 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)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
⊢ s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)

Tactic:
have : s = cylinder univ (MeasurableEquiv.piCongrLeft X e ⁻¹' s) := rfl
-- 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)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
this :
  s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
nth_rw :
  Eq (α := ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (cylinder (α := X) univ
          ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)) :
      ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
nth_rw 1 [this]
-- 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)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
this :
  s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
dsimp :
  Eq (α := ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (cylinder (α := X) univ
          ((⇑(piCongrLeft X
                  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
                    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯,
                    left_inv := ⋯, right_inv := ⋯ }) :
              (a : (b : ↥univ) → X (↑b : ι)) → (a : ι) → X a) ⁻¹'
            s)) :
      ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (cylinder (α := X) univ
          ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)) :
      ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
dsimp [e]
-- 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)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
this :
  s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
⊢ Measurable (α := (i : ↥univ) → X (↑i : ι)) (β := (i : ι) → X i)
    (⇑(piCongrLeft X
          { toFun := fun (i : ↥univ) ↦ (↑i : ι),
            invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯,
            left_inv := ⋯, right_inv := ⋯ }) :
      (a : (b : ↥univ) → X (↑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)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
this :
  s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.map (α := (i : ↥univ) → X (↑i : ι))
            (⇑(piCongrLeft X
                  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
                    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯,
                    left_inv := ⋯, right_inv := ⋯ }) :
              (a : (b : ↥univ) → X (↑b : ι)) → (a : ι) → X a)
            (Measure.pi (α := fun (i : ↥univ) ↦ X (↑i : ι)) fun (i : ↥univ) ↦ μ (↑i : ι)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.map (α := (b : ↥univ) → X ((e : (a : ↥univ) → ι) b))
            (⇑(piCongrLeft (fun (i : ι) ↦ X i) e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a)
            (Measure.pi (α := fun (i : ↥univ) ↦ X ((e : (a : ↥univ) → ι) i)) fun (i : ↥univ) ↦
              μ ((e : (a : ↥univ) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (cylinder (α := X) univ
          ((⇑(piCongrLeft X
                  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
                    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯,
                    left_inv := ⋯, right_inv := ⋯ }) :
              (a : (b : ↥univ) → X (↑b : ι)) → (a : ι) → X a) ⁻¹'
            s)) :
      ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← Measure.pi_map_piCongrLeft e,
    ← Measure.map_apply (by fun_prop) hs]

Premises used: MeasurableSet.preimage, MeasureTheory.Measure.pi_map_piCongrLeft, MeasureTheory.piContent_cylinder, MeasureTheory.Measure.map_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)
inst : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι :=
  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯, left_inv := ⋯,
    right_inv := ⋯ }
this :
  s =
    cylinder (α := X) univ
      ((⇑(piCongrLeft X e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a) ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := (i : ↥univ) → X (↑i : ι))
            (⇑(piCongrLeft X
                  { toFun := fun (i : ↥univ) ↦ (↑i : ι),
                    invFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯,
                    left_inv := ⋯, right_inv := ⋯ }) :
              (a : (b : ↥univ) → X (↑b : ι)) → (a : ι) → X a)
            (Measure.pi (α := fun (i : ↥univ) ↦ X (↑i : ι)) fun (i : ↥univ) ↦ μ (↑i : ι)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.map (α := (b : ↥univ) → X ((e : (a : ↥univ) → ι) b))
            (⇑(piCongrLeft (fun (i : ι) ↦ X i) e) : (a : (b : ↥univ) → X ((e : (a : ↥univ) → ι) b)) → (a : ι) → X a)
            (Measure.pi (α := fun (i : ↥univ) ↦ X ((e : (a : ↥univ) → ι) i)) fun (i : ↥univ) ↦
              μ ((e : (a : ↥univ) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
⊢ IsProbabilityMeasure.{u_1} (α := (n : ℕ) → X n) (m0 := MeasurableSpace.pi (X := X))
    (bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.pi (α := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) fun (i : ↥(Iic 0)) ↦ μ (↑i : ℕ))
      (⇑(traj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) 0) :
        (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)))

Tactic:
infer_instance
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Ioc a c)) → X (↑i : ℕ)))
    (map (IocProdIoc (X := X) a b c)
      (Measure.prod (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc b c)) ↦ μ (↑i : ℕ))))
    (Measure.pi (α := fun (i : ↥(Ioc a c)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a c)) ↦ μ (↑i : ℕ))

Tactic:
(Measure.pi_eq fun s ms ↦ ?_).symm

Premises used: Set.Mem, setOf, MeasureTheory.Measure.pi_eq, Eq.symm