awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
⊢ S = Finset.restrict₂ (π := α) hJI ⁻¹' T

Tactic:
have : S = Finset.restrict₂ hJI ⁻¹' T :=
      eq_of_cylinder_eq_of_subset h_eq hJI
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ (π := α) hJI ⁻¹' T
rw : Measurable (α := (i : ↥I) → α (↑i : ι)) (Finset.restrict₂ (π := α) hJI)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)

Tactic:
rw [hP I J hJI, Measure.map_apply _ hT, this]

Premises used: MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ (π := α) hJI ⁻¹' T
⊢ Measurable (α := (i : ↥I) → α (↑i : ι)) (Finset.restrict₂ (π := α) hJI)

Tactic:
measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, measurable_pi_apply, Subtype.mk, Finset.restrict₂._proof_1, Subtype.val
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ (π := α) hJI ⁻¹' T
⊢ Measurable (α := (i : ↥I) → α (↑i : ι)) (Finset.restrict₂ (π := α) hJI)

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, measurable_pi_apply
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
⊢ IsEmpty ((i : ι) → α i) ∨ Nonempty ((i : ι) → α i)

Tactic:
cases isEmpty_or_nonempty (∀ i, α i) with
  | inl h =>
    suffices ∀ I, P I univ = 0 by
      simp only [Measure.measure_univ_eq_zero] at this
      simp [this]
    simpa using eq_zero_of_isEmpty hP
  | inr h =>
    have : S = Finset.restrict₂ hJI ⁻¹' T :=
      eq_of_cylinder_eq_of_subset h_eq hJI
    rw [hP I J hJI, Measure.map_apply _ hT, this]
    exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, MeasureTheory.Measure.map_apply, measurable_pi_apply, isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
suffices :
  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)

Tactic:
suffices P (I ∪ J) U = P I S ∧ P (I ∪ J) U = P J T from this.1.symm.trans this.2
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
left :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) U : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
right :
  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 ∪ 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:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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 (α := α) I S = cylinder (α := α) I S ∩ cylinder (α := α) J T
rw₁ : cylinder (α := α) J T = cylinder (α := α) J T ∩ cylinder (α := α) J T
rw₂ rw₃ : cylinder (α := α) J T = cylinder (α := α) J T
⊢ cylinder (α := α) I S = cylinder (α := α) (I ∪ J) U

Tactic:
rw [← inter_cylinder, h_eq, inter_self]

Premises used: MeasureTheory.inter_cylinder, Set.inter_self
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
⊢ cylinder (α := α) I S = cylinder (α := α) (I ∪ J) U

Tactic:
have h_eq_union : cylinder I S = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
h_eq_union : cylinder (α := α) I S = cylinder (α := α) (I ∪ J) U
⊢ 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:
hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left

Premises used: MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset, Finset.subset_union_left, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
h_eq_union : cylinder (α := α) I S = cylinder (α := α) (I ∪ J) U
⊢ 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:
exact hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left

Premises used: MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset, Finset.subset_union_left, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
rw₂ rw₃ : cylinder (α := α) J T = cylinder (α := α) J T
⊢ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) U

Tactic:
rw [← inter_cylinder, h_eq, inter_self]

Premises used: MeasureTheory.inter_cylinder, Set.inter_self
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
⊢ 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]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
h_eq_union : cylinder (α := α) J T = cylinder (α := α) (I ∪ J) U
⊢ 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:
hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right

Premises used: MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset, Eq.symm, Finset.subset_union_right
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
h_eq_union : cylinder (α := α) J T = cylinder (α := α) (I ∪ J) U
⊢ 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:
exact hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right

Premises used: MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset, Eq.symm, Finset.subset_union_right
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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)
right right₁ :
  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 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)

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
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
rw : Measurable (α := (i : ι) → α i) (I.restrict (π := α))
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I s) : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) s : ENNReal)

Tactic:
rw [cylinder, ← Measure.map_apply _ hs, h I]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
⊢ Measurable (α := (i : ι) → α i) (I.restrict (π := α))

Tactic:
measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, measurable_pi_apply, Subtype.val
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
⊢ Measurable (α := (i : ι) → α i) (I.restrict (π := α))

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, measurable_pi_apply
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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)
rw₁ rw₂ :
  Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) 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)

Tactic:
rw [← cylinder_univ I, hμ.measure_cylinder _ MeasurableSet.univ]

Premises used: MeasureTheory.cylinder_univ, MeasureTheory.IsProjectiveLimit.measure_cylinder, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
measure_univ_lt_top : LT.lt (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (⊤ : ENNReal)
⊢ IsFiniteMeasure μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
measure_univ_lt_top :
  LT.lt (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (⊤ : ENNReal)
⊢ LT.lt (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (⊤ : ENNReal)

Tactic:
rw [hμ.measure_univ_eq (∅ : Finset ι)]

Premises used: MeasureTheory.IsProjectiveLimit.measure_univ_eq, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (⊤ : ENNReal)

Tactic:
measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (⊤ : ENNReal)

Tactic:
exact measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
measure_univ : Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ IsProbabilityMeasure μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
measure_univ : Eq (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
rw [hμ.measure_univ_eq (∅ : Finset ι)]

Premises used: MeasureTheory.IsProjectiveLimit.measure_univ_eq, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
exact measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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)
rw₁ rw₂ :
  Eq (α := ENNReal) ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P ∅ : (a : Set ((j : ↥∅) → α (↑j : ι))) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) univ : ENNReal)

Tactic:
rw [hμ.measure_univ_eq (∅ : Finset ι), hν.measure_univ_eq (∅ : Finset ι)]

Premises used: MeasureTheory.IsProjectiveLimit.measure_univ_eq, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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
⊢ IsFiniteMeasure μ

Tactic:
haveI : IsFiniteMeasure μ := hμ.isFiniteMeasure
-- Module: Mathlib.MeasureTheory.Constructions.Projective
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 μ
⊢ μ = ν

Tactic:
ext_of_generate_finite (measurableCylinders α) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (fun s hs ↦ ?_) (hμ.measure_univ_unique hν)

Premises used: MeasureTheory.ext_of_generate_finite, MeasureTheory.measurableCylinders, MeasureTheory.IsProjectiveLimit.measure_univ_unique, MeasureTheory.isPiSystem_measurableCylinders, MeasureTheory.generateFrom_measurableCylinders, Eq.symm