awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have lt_top_of_isCompact : LT.lt (α := ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      (Set.pi (α := α) univ fun (j : ι) ↦ eval (β := α) j '' K) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: suffices Measure.pi μ (Set.univ.pi fun j => Function.eval j '' K) < ⊤ by
    exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (j : ι) ↦ eval (β := α) j '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have lt_top_of_isCompact : LT.lt (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K)) ∞
Tactic: rw [Measure.pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K)) ∞
have lt_top_of_isCompact : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    LT.lt (α := WithTop NNReal) ((μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K) : ℝ≥0∞) (⊤ : WithTop NNReal)
Tactic: refine WithTop.prod_lt_top ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
⊢ MeasurePreserving (β := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p) :
      (a : (i : ι) → α i) → ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (Measure.pi (α := α) μ)
    (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))
have refine : MeasurePreserving (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
  (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
  (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
    (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))
  (Measure.pi (α := α) μ)
Tactic: refine MeasurePreserving.symm e ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
⊢ MeasurePreserving (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
    (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))
    (Measure.pi (α := α) μ)
have refine : ∀ (s : (i : ι) → Set (α i)),
  (∀ (i : ι), MeasurableSet (s i)) →
    Eq (α := ℝ≥0∞)
      ((Measure.map (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
              (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
              (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
                (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι))) :
            (a : Set ((i : ι) → α i)) → ℝ≥0∞)
          (Set.pi (α := α) univ s) :
        ℝ≥0∞)
      (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine ⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
            (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
            (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
              (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι))) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this : (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i) ⁻¹'
    Set.pi (α := α) univ s =
  SProd.sprod (α := Set ((i : { i : ι // p i }) → α (↑i : ι))) (β := Set ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (Set.pi (α := fun (i : { i : ι // p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // p i }) ↦ s (↑i : ι))
    (Set.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // ¬p i }) ↦ s (↑i : ι))
Tactic: have : e ⁻¹' pi univ s =
      (pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i :=
    Equiv.preimage_piEquivPiSubtypeProd_symm_pi p s
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
this :
  (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i) ⁻¹'
      Set.pi (α := α) univ s =
    SProd.sprod (α := Set ((i : { i : ι // p i }) → α (↑i : ι))) (β := Set ((i : { i : ι // ¬p i }) → α (↑i : ι)))
      (Set.pi (α := fun (i : { i : ι // p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // p i }) ↦ s (↑i : ι))
      (Set.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // ¬p i }) ↦ s (↑i : ι))
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
            (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
            (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
              (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι))) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞)
    (∏ i : Subtype p, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι)))
    (∏ i : { i : ι // ¬p i }, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι))) =
  ∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)
Tactic: rw [e.map_apply, this, prod_prod, pi_pi, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
⊢ Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
      (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
      (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) =
    Measure.pi (α := α) μ
have refine : ∀ (s : (i : ι) → Set (α i)),
  (∀ (i : ι), MeasurableSet (s i)) →
    Eq (α := ℝ≥0∞)
      ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
              (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
              (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
            (a : Set ((i : ι) → α i)) → ℝ≥0∞)
          (Set.pi (α := α) univ s) :
        ℝ≥0∞)
      (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine (pi_eq fun s _ => ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
            (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
            (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
        (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
      ((⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a) ⁻¹'
        Set.pi (α := α) univ s) :
    ℝ≥0∞)
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f,
      Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _, f.prod_comp (fun i => μ i (s i))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
            (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
            (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
        (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
      ((⇑(Equiv.piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
        Set.pi (α := α) univ s) :
    ℝ≥0∞)
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f,
      Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _, f.prod_comp (fun i => μ i (s i))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
            (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
            (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
        (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
      (Set.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) univ fun (i : ι') ↦ s ((f : (a : ι') → ι) i)) :
    ℝ≥0∞)
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f,
      Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _, f.prod_comp (fun i => μ i (s i))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) univ fun (i : ι') ↦ s ((f : (a : ι') → ι) i)) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
            (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
            (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞)
  (∏ i : ι',
    ((μ ((f : (a : ι') → ι) i) : Measure (α ((f : (a : ι') → ι) i))) : (a : Set (α ((f : (a : ι') → ι) i))) → ℝ≥0∞)
      (s ((f : (a : ι') → ι) i)))
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
Tactic: rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f,
      Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _, f.prod_comp (fun i => μ i (s i))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) univ fun (i : ι') ↦ s ((f : (a : ι') → ι) i)) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞)
    (∏ i : ι',
      ((μ ((f : (a : ι') → ι) i) : Measure (α ((f : (a : ι') → ι) i))) : (a : Set (α ((f : (a : ι') → ι) i))) → ℝ≥0∞)
        (s ((f : (a : ι') → ι) i)))
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
            (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
            (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
Tactic: rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f,
      Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _, f.prod_comp (fun i => μ i (s i))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
⊢ Eq (α := Measure ((γ → α) × (γ → β)))
    (Measure.map (α := γ → α × β)
      (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
      (Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i)))
    (Measure.prod (Measure.pi (α := fun (i : γ) ↦ α) fun (i : γ) ↦ μ i)
      (Measure.pi (α := fun (a : γ) ↦ β) fun (i : γ) ↦ ν i))
have refine_1 : Eq (α := MeasurableSpace (((i : γ) → α) × ((i : γ) → β))) Prod.instMeasurableSpace
  (generateFrom
    (image2 (fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2)
      (Set.pi (α := fun (i : γ) ↦ α) univ ''
        Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
      (Set.pi (α := fun (i : γ) ↦ β) univ ''
        Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})))
Tactic: refine (FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
      ((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
      (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn))) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
refine_1 :
  Eq (α := MeasurableSpace (((i : γ) → α) × ((i : γ) → β))) Prod.instMeasurableSpace
    (generateFrom
      (image2 (fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2)
        (Set.pi (α := fun (i : γ) ↦ α) univ ''
          Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
        (Set.pi (α := fun (i : γ) ↦ β) univ ''
          Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})))
⊢ Eq (α := Measure ((γ → α) × (γ → β)))
    (Measure.map (α := γ → α × β)
      (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
      (Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i)))
    (Measure.prod (Measure.pi (α := fun (i : γ) ↦ α) fun (i : γ) ↦ μ i)
      (Measure.pi (α := fun (a : γ) ↦ β) fun (i : γ) ↦ ν i))
have refine_2 : ∀ (s : Set (((i : γ) → α) × ((i : γ) → β))),
  Membership.mem (γ := Set (Set (((i : γ) → α) × ((i : γ) → β))))
      (image2 (fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2)
        (Set.pi (α := fun (i : γ) ↦ α) univ ''
          Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
        (Set.pi (α := fun (i : γ) ↦ β) univ ''
          Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s}))
      s →
    Eq (α := ℝ≥0∞)
      (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
            (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((Measure.map (α := γ → α × β)
              (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
              (Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i)) :
            (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: refine (FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
      ((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
      (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn))) ?_).symm