-- 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:
ι : 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'
⊢ s ∪ t = cylinder (I ∪ J) (S' ∪ T')

Tactic:
rw [hs_eq, ht_eq]

Result:
ι : 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')

Proof state:
case intro.intro.intro.intro.intro.intro.inl
ι : 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'
h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T')
h : IsEmpty ((i : ι) → α i)
⊢ (P (I ∪ J)) (S' ∪ T') = (P (I ∪ J)) S' + (P (I ∪ J)) T'

Tactic:
simp [hP.eq_zero_of_isEmpty]

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
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Tactic:
let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T

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
⊢ 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
⊢ 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

Result:
no goals

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'
⊢ cylinder I S = cylinder (I ∪ J) S'

Tactic:
exact cylinder_eq_cylinder_union I S J

Result:
no goals