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
hJI : J ⊆ I
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have have : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
Tactic: classical
  have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)
-- 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
hJI : J ⊆ I
have : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have have₁ : ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
  Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: classical
  have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)
-- 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
hJI : J ⊆ I
have : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₁ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₂ : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₃ have₄ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have have₅ : ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
  Eq (α := ENNReal)
    ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((i : ↥J) → α (↑i : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: classical
  have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)
-- 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
hJI : J ⊆ I
have : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₁ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₂ : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₃ have₄ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₅ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal)
      ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((i : ↥J) → α (↑i : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have have₆ : (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)) →
  MeasurableSpace ((i : ↥J) → α (↑i : ι))
Tactic: classical
  have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)
-- 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
hJI : J ⊆ I
have : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₁ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₂ : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₃ have₄ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₅ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal)
      ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((i : ↥J) → α (↑i : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₆ :
  (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)) →
    MeasurableSpace ((i : ↥J) → α (↑i : ι))
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have have₇ : ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
  Measurable (α := (j : ↥I) → α (↑j : ι)) (Finset.restrict₂ (π := α) hJI)
Tactic: classical
  have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)
-- 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 : ι))
hP : IsProjectiveMeasureFamily (α := α) P
I J : Finset ι
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw : Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
  ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
    ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]
-- 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 : ι))
hP : IsProjectiveMeasureFamily (α := α) P
I J : Finset ι
rw :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₁ : Finset ι
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw₂ : Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
  ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
    ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]
-- 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 : ι))
hP : IsProjectiveMeasureFamily (α := α) P
I J : Finset ι
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw : Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
  ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: classical
  rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
    ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]
-- 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 : ι))
hP : IsProjectiveMeasureFamily (α := α) P
I J : Finset ι
rw :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₁ : Finset ι
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw₂ : Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
  ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
Tactic: classical
  rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
    ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]
-- 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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this :
  ∀ (I : Finset ι), Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have this₁ : ∀ (I : Finset ι), P I = 0
Tactic: simp only [Measure.measure_univ_eq_zero] at this
Cleared hypotheses: this
-- 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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have inl : ∀ (I : Finset ι), Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal) (0 : ENNReal)
Tactic: suffices ∀ I, P I univ = 0 by
      simp only [Measure.measure_univ_eq_zero] at this
      simp [this]
-- 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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have this : S = Finset.restrict₂ (π := α) hJI ⁻¹' T
Tactic: have : S = Finset.restrict₂ hJI ⁻¹' T :=
      eq_of_cylinder_eq_of_subset h_eq hJI
-- 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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ (π := α) hJI ⁻¹' T
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have rw : Measurable (α := (i : ↥I) → α (↑i : ι)) (Finset.restrict₂ (π := α) hJI)
Tactic: rw [hP I J hJI, Measure.map_apply _ hT, this]
-- 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 : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have x : 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 _)
-- 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
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)
have 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)
Tactic: suffices P (I ∪ J) U = P I S ∧ P (I ∪ J) U = P J T from this.1.symm.trans this.2
-- 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
⊢ 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)
have 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)
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 : ι))
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)
⊢ 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)
have 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)
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 : ι))
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
have rw : cylinder (α := α) I S = cylinder (α := α) I S ∩ cylinder (α := α) J T
Tactic: 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
U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T
rw : cylinder (α := α) I S = cylinder (α := α) I S ∩ cylinder (α := α) J T
⊢ cylinder (α := α) I S = cylinder (α := α) (I ∪ J) U
have rw₁ : cylinder (α := α) J T = cylinder (α := α) J T ∩ cylinder (α := α) J T
Tactic: 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
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
⊢ cylinder (α := α) I S = 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 I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
have h_eq_union : 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]
-- 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
⊢ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) U
have rw : cylinder (α := α) J T = cylinder (α := α) I S ∩ cylinder (α := α) J T
Tactic: 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
U : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T
rw : cylinder (α := α) J T = cylinder (α := α) I S ∩ cylinder (α := α) J T
⊢ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) U
have rw₁ : cylinder (α := α) J T = cylinder (α := α) J T ∩ cylinder (α := α) J T
Tactic: rw [← inter_cylinder, h_eq, inter_self]