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)
i : ι
s : Set (X i)
hs : MeasurableSet s
⊢ Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))
have h : ∀ (x : (x : ι) → X x),
  Function.eval (β := X) i x =
    Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry))
      (Finset.restrict (π := X) {i}) x
Tactic: ext
-- 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)
i : ι
s : Set (X i)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((map (Function.eval (β := X) i) (infinitePi (X := X) μ) : Measure (X i)) : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ i : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
have this : Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
  (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
    (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
      (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry))
    (Finset.restrict (π := X) {i}))
Tactic: have : @Function.eval ι X i =
        (@Function.eval ({i} : Finset ι) (fun j ↦ X j) ⟨i, by simp⟩) ∘
        (Finset.restrict {i}) := by ext; simp
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
this :
  Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))
⊢ Eq (α := ℝ≥0∞)
    (((map (Function.eval (β := X) i) (infinitePi (X := X) μ) : Measure (X i)) : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ i : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
have h : Measurable (α := (x : ↥{i}) → X (↑x : ι))
  (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
    (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry))
Tactic: rw [this, ← map_map, infinitePi_map_restrict, (measurePreserving_eval _ _).map_eq]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
this :
  Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))
h :
  Measurable (α := (x : ↥{i}) → X (↑x : ι))
    (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
      (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
⊢ Eq (α := ℝ≥0∞)
    (((map (Function.eval (β := X) i) (infinitePi (X := X) μ) : Measure (X i)) : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ i : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Measurable (α := (x : ι) → X x) (β := (x : ↥{i}) → X (↑x : ι)) (Finset.restrict (π := X) {i})
Tactic: rw [this, ← map_map, infinitePi_map_restrict, (measurePreserving_eval _ _).map_eq]
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ))
    (infinitePi (X := Y) fun (i : ι) ↦ map (f i) (μ i))
have this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
Tactic: have (i : ι) : IsProbabilityMeasure ((μ i).map (f i)) :=
    isProbabilityMeasure_map (hf i).aemeasurable
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ))
    (infinitePi (X := Y) fun (i : ι) ↦ map (f i) (μ i))
have refine : ∀ (s : Finset ι) (t : (i : ι) → Set (Y i)) (ht : ∀ (i : ι), MeasurableSet (t i)),
  Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := Y) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: refine eq_infinitePi _ fun s t ht ↦ ?_
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := Y) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      (Set.preimage (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i))
        ((↑s : Set ι).pi (α := fun (i : ι) ↦ Y i) fun (x : ι) ↦ t x)) :
    ℝ≥0∞)
  (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: rw [map_apply (by fun_prop) (.pi s.countable_toSet fun _ _ ↦ ht _)]
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)
have h : ∀ (x : (i : ι) → X i),
  Membership.mem (γ := Set ((i : ι) → X i))
      ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t) x ↔
    Membership.mem (γ := Set ((i : ι) → X i)) ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i) x
Tactic: ext x
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i))
          ((↑s : Set ι).pi (α := fun (i : ι) ↦ Y i) fun (x : ι) ↦ t x)) :
      ℝ≥0∞)
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have this₁ : Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
  ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)
Tactic: have : (fun (x : Π i, X i) i ↦ f i (x i)) ⁻¹' ((s : Set ι).pi t) =
      (s : Set ι).pi (fun i ↦ (f i) ⁻¹' (t i)) := by ext x; simp
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this_1 : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)
⊢ Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i))
          ((↑s : Set ι).pi (α := fun (i : ι) ↦ Y i) fun (x : ι) ↦ t x)) :
      ℝ≥0∞)
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i))
  (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i))
Tactic: rw [this, infinitePi_pi _ (fun i _ ↦ hf i (ht 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this_1 : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i))
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i))
have a : ∀ (i : ι) (hi : i ∈ s),
  Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i) : ℝ≥0∞)
    (((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: congr! with i hi
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this_1 : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)
i : ι
hi : i ∈ s
⊢ Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i) : ℝ≥0∞)
    (((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have a : Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i) : ℝ≥0∞)
  ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i) : ℝ≥0∞)
Tactic: rw [map_apply (by fun_prop) (ht 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)
α : Type u_3
e : α ≃ ι
⊢ map (α := (b : α) → X ((e : (a : α) → ι) b))
      (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
      (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) =
    infinitePi (X := X) μ
have refine : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)) (ht : ∀ (i : ι), MeasurableSet (t i)),
  Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := X) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: refine eq_infinitePi μ fun s t ht ↦ ?_
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
| ((map (α := (b : α) → X ((e : (a : α) → ι) b))
          (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
          (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      ((↑s : Set ι).pi (α := X) t) :
    ℝ≥0∞)
have enter : (↑s : Set ι)
Tactic: enter [2, 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
| (↑s : Set ι)
have rw : (⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) sorry) : Set α)
Tactic: rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
| ((map (α := (b : α) → X ((e : (a : α) → ι) b))
          (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
          (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      ((↑s : Set ι).pi (α := X) t) :
    ℝ≥0∞)
have enter : (⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) sorry) : Set α)
Tactic: enter [2, 1]; rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := X) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have conv_lhs : Eq (α := ℝ≥0∞)
  ((map (α := (b : α) → X ((e : (a : α) → ι) b))
          (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
          (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) sorry) : Set α)) t) :
    ℝ≥0∞)
  (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: conv_lhs => enter [2, 1]; rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hst : ∀ (i : α), i ∈ s.preimage (⇑e : (a : α) → ι) sorry ↔ Membership.mem (α := ι) s ((e : (a : α) → ι) i : ι)
Tactic: rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
hst : ∀ (i : α), i ∈ s.preimage (⇑e : (a : α) → ι) ⋯ ↔ Membership.mem (α := ι) s ((e : (a : α) → ι) i : ι)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hfg : ∀ i ∈ s.preimage (⇑e : (a : α) → ι) sorry,
  Eq (α := ℝ≥0∞)
    (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
        (t ((e : (a : α) → ι) i)) :
      ℝ≥0∞)
    (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
        (t ((e : (a : α) → ι) i)) :
      ℝ≥0∞)
Tactic: rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
hst : ∀ (i : α), i ∈ s.preimage (⇑e : (a : α) → ι) ⋯ ↔ Membership.mem (α := ι) s ((e : (a : α) → ι) i : ι)
hfg :
  ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯,
    Eq (α := ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have mt : ∀ i ∈ s.preimage (⇑e : (a : α) → ι) sorry, MeasurableSet (α := X ((e : (a : α) → ι) i)) (t ((e : (a : α) → ι) i))
Tactic: rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
hst : ∀ (i : α), i ∈ s.preimage (⇑e : (a : α) → ι) ⋯ ↔ Membership.mem (α := ι) s ((e : (a : α) → ι) i : ι)
hfg :
  ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯,
    Eq (α := ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
mt : ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯, MeasurableSet (α := X ((e : (a : α) → ι) i)) (t ((e : (a : α) → ι) i))
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hf : Measurable (α := (b : α) → X ((e : (a : α) → ι) b)) (β := (a : ι) → X a)
  (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
Tactic: rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
hst : ∀ (i : α), i ∈ s.preimage (⇑e : (a : α) → ι) ⋯ ↔ Membership.mem (α := ι) s ((e : (a : α) → ι) i : ι)
hfg :
  ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯,
    Eq (α := ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
mt : ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯, MeasurableSet (α := X ((e : (a : α) → ι) i)) (t ((e : (a : α) → ι) i))
hf :
  Measurable (α := (b : α) → X ((e : (a : α) → ι) b)) (β := (a : ι) → X a)
    (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hs : MeasurableSet (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) sorry) : Set α)) t)
Tactic: rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]
-- 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)
inst : Fintype ι
⊢ infinitePi (X := X) μ = Measure.pi (α := X) μ
have refine : ∀ (s : (i : ι) → Set (X i)) (hs : ∀ (i : ι), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine (pi_eq fun s hs ↦ ?_).symm