awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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'
have rw : cylinder (α := α) I S = cylinder (α := α) (I ∪ J) S'
Tactic: rw [hs_eq]
-- 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'
hT' : MeasurableSet T'
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have h_eq1 : 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
-- 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
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'
have rw : cylinder (α := α) J T = cylinder (α := α) (I ∪ J) T'
Tactic: rw [ht_eq]
-- 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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have h_eq2 : 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
-- 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
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')
have rw : cylinder (α := α) I S ∪ cylinder (α := α) J T = cylinder (α := α) (I ∪ J) (S' ∪ T')
Tactic: rw [hs_eq, ht_eq]
-- 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'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have h_eq3 : 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 _ _ _ _
-- 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
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')
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have 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∞)
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')]
-- 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
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')
h : Nonempty ((i : ι) → α i)
⊢ (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∞)
have rw : Disjoint S' T'
Tactic: rw [measure_union _ hT']
-- 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
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')
h : Nonempty ((i : ι) → α i)
⊢ Disjoint S' T'
have rwa : ∀ (hst : Disjoint (cylinder (α := α) I S) t) (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),
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' S;
  let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' 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'))
    (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
Tactic: rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
Cleared hypotheses: hst, hS, hs_eq, J, T, hT, ht_eq, S', T', hS', hT', h_eq1, h_eq2, h_eq3, h
-- 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
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')
h : Nonempty ((i : ι) → α i)
rwa :
  ∀ (hst : Disjoint (cylinder (α := α) I S) t) (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),
    let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
    let 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'))
      (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
⊢ Disjoint S' T'
have rwa₁ : ∀ (hS : MeasurableSet S) (hs_eq : s = cylinder (α := α) I S) (J : Finset ι) (T : Set ((i : ↥J) → α (↑i : ι)))
  (hst : Disjoint (cylinder (α := α) I S) (cylinder (α := α) J T)) (hT : MeasurableSet T)
  (ht_eq : t = cylinder (α := α) J T),
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' S;
  let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' 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'))
    (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
Tactic: rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
Cleared hypotheses: hst, hS, hs_eq, J, T, hT, ht_eq, S', T', hS', hT', h_eq1, h_eq2, h_eq3, h
-- 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
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')
h : Nonempty ((i : ι) → α i)
rwa :
  ∀ (hst : Disjoint (cylinder (α := α) I S) t) (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),
    let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
    let 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'))
      (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
rwa₁ :
  ∀ (hS : MeasurableSet S) (hs_eq : s = cylinder (α := α) I S) (J : Finset ι) (T : Set ((i : ↥J) → α (↑i : ι)))
    (hst : Disjoint (cylinder (α := α) I S) (cylinder (α := α) J T)) (hT : MeasurableSet T)
    (ht_eq : t = cylinder (α := α) J T),
    let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
    let 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'))
      (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
⊢ Disjoint S' T'
have rwa₂ : ∀ (hS : MeasurableSet S) (hs_eq : s = cylinder (α := α) I S) (J : Finset ι) (T : Set ((i : ↥J) → α (↑i : ι)))
  (hst : Disjoint (α := Set ((i : ↥(I ∪ J)) → α (↑i : ι))) (restrict₂ (π := α) sorry ⁻¹' S) (restrict₂ (π := α) sorry ⁻¹' T))
  (hT : MeasurableSet T) (ht_eq : t = cylinder (α := α) J T),
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' S;
  let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' 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'))
    (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
Tactic: rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
Cleared hypotheses: hst, hS, hs_eq, J, T, hT, ht_eq, S', T', hS', hT', h_eq1, h_eq2, h_eq3, h
-- 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'
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')
⊢ (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∞)
have x : IsEmpty ((i : ι) → α i) ∨ Nonempty ((i : ι) → α i)
Tactic: cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
-- 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
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
let let₁ let₂ let₃ :
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have let₄ : let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' S;
∀ (hS' : MeasurableSet S'),
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
Tactic: classical
  let S' := restrict₂ (subset_union_left (s₂ := J)) ⁻¹' S
  let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T
  have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
  have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
  have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
  have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
  have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by
    rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
  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')]
  cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
-- 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
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
let let₁ let₂ let₃ :
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
let₄ :
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
  ∀ (hS' : MeasurableSet S'),
    projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have let₅ : let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' S;
let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' T;
∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T'),
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
Tactic: classical
  let S' := restrict₂ (subset_union_left (s₂ := J)) ⁻¹' S
  let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T
  have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
  have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
  have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
  have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
  have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by
    rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
  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')]
  cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
-- 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
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
let let₁ let₂ let₃ :
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
let₄ :
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
  ∀ (hS' : MeasurableSet S'),
    projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
let₅ :
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
  let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T;
  ∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T'),
    projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have let₆ : let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' S;
let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' T;
∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T') (h_eq1 : s = cylinder (α := α) (I ∪ J) S'),
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
Tactic: classical
  let S' := restrict₂ (subset_union_left (s₂ := J)) ⁻¹' S
  let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T
  have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
  have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
  have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
  have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
  have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by
    rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
  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')]
  cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst