-- Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
lemma projectiveFamilyFun_union (hP : IsProjectiveMeasureFamily P)
    (hs : s ∈ measurableCylinders α) (ht : t ∈ measurableCylinders α) (hst : Disjoint s t) :
    projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Tactic:
have hT' : MeasurableSet T' := measurable_restrict₂ _ hT

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ 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 _ _ _ _

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ 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

Tactic:
have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ 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

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

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

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ 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

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Tactic:
have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ 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 : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : { x // x ∈ 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