-- 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
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
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') (h_eq1 : s = cylinder (α := α) (I ∪ J) 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') (h_eq1 : s = cylinder (α := α) (I ∪ J) S')
    (h_eq2 : t = cylinder (α := α) (I ∪ J) T'),
    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') (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
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') (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∞)
⊢ 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

Premises used: isEmpty_or_nonempty, MeasureTheory.disjoint_cylinder_iff