awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T
rw : cylinder (α := α) J T = cylinder (α := α) I S ∩ cylinder (α := α) J T
rw₁ : cylinder (α := α) J T = cylinder (α := α) J T ∩ cylinder (α := α) J T
⊢ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) U
have rw₂ : cylinder (α := α) J T = cylinder (α := α) J T
Tactic: rw [← inter_cylinder, h_eq, inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T
⊢ Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have h_eq_union : cylinder (α := α) J T = cylinder (α := α) (I ∪ J) U
Tactic: have h_eq_union : cylinder J T = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
let let₁ let₂ :
  Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have let₃ : let U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) sorry ⁻¹' S ∩ Finset.restrict₂ (π := α) sorry ⁻¹' T;
Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal) ∧
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
Tactic: classical
  let U := Finset.restrict₂ Finset.subset_union_left ⁻¹' S ∩
      Finset.restrict₂ Finset.subset_union_right ⁻¹' T
  suffices P (I ∪ J) U = P I S ∧ P (I ∪ J) U = P J T from this.1.symm.trans this.2
  constructor
  · have h_eq_union : cylinder I S = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left
  · have h_eq_union : cylinder J T = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
let let₁ let₂ :
  Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
let₃ :
  let U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T;
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
      ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal) ∧
    Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have left : let U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) sorry ⁻¹' S ∩ Finset.restrict₂ (π := α) sorry ⁻¹' T;
Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
  ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
Tactic: classical
  let U := Finset.restrict₂ Finset.subset_union_left ⁻¹' S ∩
      Finset.restrict₂ Finset.subset_union_right ⁻¹' T
  suffices P (I ∪ J) U = P I S ∧ P (I ∪ J) U = P J T from this.1.symm.trans this.2
  constructor
  · have h_eq_union : cylinder I S = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left
  · have h_eq_union : cylinder J T = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
let let₁ let₂ :
  Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
let₃ :
  let U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T;
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
      ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal) ∧
    Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
left :
  let U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T;
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have right : let U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) sorry ⁻¹' S ∩ Finset.restrict₂ (π := α) sorry ⁻¹' T;
Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
  ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
Tactic: classical
  let U := Finset.restrict₂ Finset.subset_union_left ⁻¹' S ∩
      Finset.restrict₂ Finset.subset_union_right ⁻¹' T
  suffices P (I ∪ J) U = P I S ∧ P (I ∪ J) U = P J T from this.1.symm.trans this.2
  constructor
  · have h_eq_union : cylinder I S = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left
  · have h_eq_union : cylinder J T = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit (α := α) μ P
I : Finset ι
s : Set ((i : ↥I) → α (↑i : ι))
hs : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I s) : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) s : ENNReal)
have rw : Measurable (α := (i : ι) → α i) (I.restrict (π := α))
Tactic: rw [cylinder, ← Measure.map_apply _ hs, h I]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit (α := α) μ P
I : Finset ι
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw : Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I univ) : ENNReal)
  ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: rw [← cylinder_univ I, hμ.measure_cylinder _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit (α := α) μ P
I : Finset ι
rw :
  Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I univ) : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw₁ : Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
  ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: rw [← cylinder_univ I, hμ.measure_cylinder _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
⊢ IsFiniteMeasure μ
have measure_univ_lt_top : LT.lt (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (⊤ : ENNReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
⊢ LT.lt (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (⊤ : ENNReal)
have measure_univ_lt_top : LT.lt (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (⊤ : ENNReal)
Tactic: rw [hμ.measure_univ_eq (∅ : Finset ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
⊢ IsProbabilityMeasure μ
have measure_univ : Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (1 : ENNReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (1 : ENNReal)
have measure_univ : Eq (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (1 : ENNReal)
Tactic: rw [hμ.measure_univ_eq (∅ : Finset ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ ν : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
have rw : Eq (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal)
  ((ν : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
Tactic: rw [hμ.measure_univ_eq (∅ : Finset ι), hν.measure_univ_eq (∅ : Finset ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ ν : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
rw :
  Eq (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
have rw₁ : Eq (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal)
  ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: rw [hμ.measure_univ_eq (∅ : Finset ι), hν.measure_univ_eq (∅ : Finset ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ ν : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
⊢ μ = ν
have this : IsFiniteMeasure μ
Tactic: haveI : IsFiniteMeasure μ := hμ.isFiniteMeasure
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ ν : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
this : IsFiniteMeasure μ
⊢ μ = ν
have refine : ∀ (s : Set ((i : ι) → α i)) (hs : s ∈ measurableCylinders α),
  Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) s : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) s : ENNReal)
Tactic: refine ext_of_generate_finite (measurableCylinders α) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (fun s hs ↦ ?_) (hμ.measure_univ_unique hν)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ ν : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
this : IsFiniteMeasure μ
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) s : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) s : ENNReal)
have obtain : ∀ (I : Finset ι) (S : Set ((i : ↥I) → α (↑i : ι))) (hS : MeasurableSet S)
  (hs : cylinder (α := α) I S ∈ measurableCylinders α),
  Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
Tactic: obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders _).mp hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ ν : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := α) I S ∈ measurableCylinders α
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
have rw : Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
  ((ν : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
Tactic: rw [hμ.measure_cylinder _ hS, hν.measure_cylinder _ hS]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
μ ν : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := α) I S ∈ measurableCylinders α
rw :
  Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
have rw₁ : Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
  ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
Tactic: rw [hμ.measure_cylinder _ hS, hν.measure_cylinder _ hS]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s : Set ((i : ι) → α i)
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
hs_eq : s = cylinder (α := α) I S
hS : MeasurableSet S
⊢ projectiveFamilyFun (α := α) P s = (P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S
have rw : Eq (α := ℝ≥0∞)
  ((P (measurableCylinders.finset (α := α) (t := s) hs) :
        (a : Set ((j : ↥(measurableCylinders.finset hs)) → α (↑j : ι))) → ℝ≥0∞)
      (measurableCylinders.set (α := α) (t := s) hs) :
    ℝ≥0∞)
  ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)
Tactic: rw [projectiveFamilyFun, dif_pos hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
hP : IsProjectiveMeasureFamily (α := α) P
⊢ projectiveFamilyFun (α := α) P ∅ = 0
have rw : Eq (α := ℝ≥0∞) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ℝ≥0∞) ∅) 0
Tactic: rw [projectiveFamilyFun_congr hP (empty_mem_measurableCylinders α) (cylinder_empty ∅).symm
    MeasurableSet.empty, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
hP : IsProjectiveMeasureFamily (α := α) P
rw : Eq (α := ℝ≥0∞) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ℝ≥0∞) ∅) 0
⊢ projectiveFamilyFun (α := α) P ∅ = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [projectiveFamilyFun_congr hP (empty_mem_measurableCylinders α) (cylinder_empty ∅).symm
    MeasurableSet.empty, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have obtain : ∀ (I : Finset ι) (S : Set ((i : ↥I) → α (↑i : ι))) (hS : MeasurableSet S) (hs_eq : s = cylinder (α := α) I S),
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
Tactic: obtain ⟨I, S, hS, hs_eq⟩ := (mem_measurableCylinders _).1 hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have obtain : ∀ (J : Finset ι) (T : Set ((i : ↥J) → α (↑i : ι))) (hT : MeasurableSet T) (ht_eq : t = cylinder (α := α) J T),
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
Tactic: obtain ⟨J, T, hT, ht_eq⟩ := (mem_measurableCylinders _).1 ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have hS' : MeasurableSet S'
Tactic: have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T
hS' : MeasurableSet S'
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have hT' : MeasurableSet T'
Tactic: have hT' : MeasurableSet T' := measurable_restrict₂ _ hT