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 : ι))
μ ν : Measure ((i : ι) → α i)
inst_1 : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit (α := α) μ P
hν : IsProjectiveLimit (α := α) ν P
this : IsFiniteMeasure μ
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ν)

Premises used: MeasureTheory.ext_of_generate_finite, MeasureTheory.measurableCylinders, MeasureTheory.IsProjectiveLimit.measure_univ_unique, MeasureTheory.isPiSystem_measurableCylinders, MeasureTheory.generateFrom_measurableCylinders, 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 : ι))
μ ν : 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 α
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)
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) s : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) s : ENNReal)

Tactic:
obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders _).mp hs

Premises used: Iff.mp, MeasureTheory.mem_measurableCylinders, rfl
-- 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 μ
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)
rw₁ rw₂ :
  Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)
    ((ν : (a : Set ((i : ι) → α i)) → ENNReal) (cylinder (α := α) I S) : ENNReal)

Tactic:
rw [hμ.measure_cylinder _ hS, hν.measure_cylinder _ hS]

Premises used: MeasureTheory.IsProjectiveLimit.measure_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
⊢ IsSetRing (measurableCylinders α)

Tactic:
isSetAlgebra_measurableCylinders.isSetRing

Premises used: MeasureTheory.IsSetAlgebra.isSetRing, MeasureTheory.isSetAlgebra_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
⊢ IsSetSemiring (measurableCylinders α)

Tactic:
isSetRing_measurableCylinders.isSetSemiring

Premises used: MeasureTheory.isSetRing_measurableCylinders, MeasureTheory.IsSetRing.isSetSemiring
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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
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∞)
⊢ projectiveFamilyFun (α := α) P s = (P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S

Tactic:
rw [projectiveFamilyFun, dif_pos hs]

Premises used: dif_pos, MeasureTheory.projectiveFamilyFun
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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
⊢ 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:
hP.congr_cylinder (measurableCylinders.measurableSet hs) hS
    ((measurableCylinders.eq_cylinder hs).symm.trans hs_eq)

Premises used: MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder, MeasureTheory.measurableCylinders.eq_cylinder, Eq.symm, MeasureTheory.measurableCylinders.measurableSet, Eq.trans
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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
⊢ 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:
exact hP.congr_cylinder (measurableCylinders.measurableSet hs) hS
    ((measurableCylinders.eq_cylinder hs).symm.trans hs_eq)

Premises used: MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder, MeasureTheory.measurableCylinders.eq_cylinder, Eq.symm, MeasureTheory.measurableCylinders.measurableSet, Eq.trans
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ projectiveFamilyFun (α := α) P ∅ = 0

Tactic:
rw [projectiveFamilyFun_congr hP (empty_mem_measurableCylinders α) (cylinder_empty ∅).symm
    MeasurableSet.empty, measure_empty]

Premises used: MeasureTheory.cylinder_empty, MeasureTheory.empty_mem_measurableCylinders, MeasurableSet.empty, MeasureTheory.measure_empty, MeasureTheory.projectiveFamilyFun_congr, EmptyCollection.emptyCollection, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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
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
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t

Tactic:
obtain ⟨I, S, hS, hs_eq⟩ := (mem_measurableCylinders _).1 hs

Premises used: Iff.mp, MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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
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
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t

Tactic:
obtain ⟨J, T, hT, ht_eq⟩ := (mem_measurableCylinders _).1 ht

Premises used: Iff.mp, MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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
⊢ MeasurableSet S'

Tactic:
have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
⊢ MeasurableSet T'

Tactic:
have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
rw : cylinder (α := α) I S = cylinder (α := α) (I ∪ J) S'
⊢ s = cylinder (α := α) (I ∪ J) S'

Tactic:
rw [hs_eq]
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
⊢ cylinder (α := α) I S = cylinder (α := α) (I ∪ J) S'

Tactic:
cylinder_eq_cylinder_union I S J

Premises used: MeasureTheory.cylinder_eq_cylinder_union
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
⊢ cylinder (α := α) I S = cylinder (α := α) (I ∪ J) S'

Tactic:
exact cylinder_eq_cylinder_union I S J

Premises used: MeasureTheory.cylinder_eq_cylinder_union
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
⊢ s = cylinder (α := α) (I ∪ J) S'

Tactic:
have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
rw : cylinder (α := α) J T = cylinder (α := α) (I ∪ J) T'
⊢ t = cylinder (α := α) (I ∪ J) T'

Tactic:
rw [ht_eq]
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
⊢ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) T'

Tactic:
cylinder_eq_cylinder_union J T I

Premises used: Set.Mem, MeasureTheory.cylinder_eq_cylinder_union, setOf, Finset.restrict, MeasureTheory.cylinder, Multiset.Mem, Set.preimage, Finset.restrict₂, Multiset.ndunion
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
⊢ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) T'

Tactic:
exact cylinder_eq_cylinder_union J T I

Premises used: MeasureTheory.cylinder_eq_cylinder_union
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
⊢ t = cylinder (α := α) (I ∪ J) T'

Tactic:
have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
rw : cylinder (α := α) I S ∪ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) (S' ∪ T')
⊢ s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T')

Tactic:
rw [hs_eq, ht_eq]
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
⊢ cylinder (α := α) I S ∪ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) (S' ∪ T')

Tactic:
union_cylinder _ _ _ _

Premises used: MeasureTheory.union_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
⊢ cylinder (α := α) I S ∪ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) (S' ∪ T')

Tactic:
exact union_cylinder _ _ _ _

Premises used: MeasureTheory.union_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
⊢ s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T')

Tactic:
have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by
    rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T')
rw :
  (P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) (S' ∪ T') =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) S' : ℝ≥0∞)
      ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) T' : ℝ≥0∞)
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t

Tactic:
rw [projectiveFamilyFun_congr hP hs h_eq1 hS', projectiveFamilyFun_congr hP ht h_eq2 hT',
    projectiveFamilyFun_congr hP (union_mem_measurableCylinders hs ht) h_eq3 (hS'.union hT')]

Premises used: MeasureTheory.union_mem_measurableCylinders, MeasurableSet.union, MeasureTheory.projectiveFamilyFun_congr