-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma congr_cylinder_of_subset (hP : IsProjectiveMeasureFamily P)
    {S : Set (∀ i : I, α i)} {T : Set (∀ i : J, α i)} (hT : MeasurableSet T)
    (h_eq : cylinder I S = cylinder J T) (hJI : J ⊆ I) :
    P I S = P J T

Proof state:
case inl.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
I : Finset ι
i : ι
hi_empty : IsEmpty (α i)
this : univ = ∅
⊢ (P {i}) univ = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
⊢ (P I) S = (P J) T

Tactic:
cases isEmpty_or_nonempty (∀ i, α i) with
| inl h =>
  suffices ∀ I, P I univ = 0 by
    simp only [Measure.measure_univ_eq_zero] at this
    simp [this]
  intro I
  simp only [isEmpty_pi] at h
  obtain ⟨i, hi_empty⟩ := h
  rw [measure_univ_eq hP I {i}]
  have : (univ : Set ((j : {x // x ∈ ({i} : Finset ι)}) → α j)) = ∅ := by simp [hi_empty]
  simp [this]
| inr h =>
  have : S = Finset.restrict₂ hJI ⁻¹' T :=
    eq_of_cylinder_eq_of_subset h_eq hJI
  rw [hP I J hJI, Measure.map_apply _ hT, this]
  exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Result:
no goals

Proof state:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
h : IsEmpty ((i : ι) → α i)
I : Finset ι
⊢ (P I) univ = 0

Tactic:
simp only [isEmpty_pi] at h

Result:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
I : Finset ι
h : ∃ a, IsEmpty (α a)
⊢ (P I) univ = 0

Proof state:
case inl.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
I : Finset ι
i : ι
hi_empty : IsEmpty (α i)
⊢ (P {i}) univ = 0

Tactic:
have : (univ : Set ((j : {x // x ∈ ({i} : Finset ι)}) → α j)) = ∅ := by simp [hi_empty]

Result:
case inl.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
I : Finset ι
i : ι
hi_empty : IsEmpty (α i)
this : univ = ∅
⊢ (P {i}) univ = 0

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this : ∀ (I : Finset ι), (P I) univ = 0
⊢ (P I) S = (P J) T

Tactic:
simp only [Measure.measure_univ_eq_zero] at this

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this : ∀ (I : Finset ι), P I = 0
⊢ (P I) S = (P J) T

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this : ∀ (I : Finset ι), P I = 0
⊢ (P I) S = (P J) T

Tactic:
simp [this]

Result:
no goals

Proof state:
case inl.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
I : Finset ι
i : ι
hi_empty : IsEmpty (α i)
⊢ (P I) univ = 0

Tactic:
rw [measure_univ_eq hP I {i}]

Result:
case inl.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
I : Finset ι
i : ι
hi_empty : IsEmpty (α i)
⊢ (P {i}) univ = 0

Proof state:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
⊢ ∀ (I : Finset ι), (P I) univ = 0

Tactic:
intro I

Result:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I✝ J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I✝ }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I✝ S = cylinder J T
hJI : J ⊆ I✝
h : IsEmpty ((i : ι) → α i)
I : Finset ι
⊢ (P I) univ = 0

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ hJI ⁻¹' T
⊢ Measurable (Finset.restrict₂ hJI)

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Result:
no goals

Proof state:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ hJI ⁻¹' T
⊢ (P I) S = (P J) T

Tactic:
rw [hP I J hJI, Measure.map_apply _ hT, this]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : Nonempty ((i : ι) → α i)
this : S = Finset.restrict₂ hJI ⁻¹' T
⊢ Measurable (Finset.restrict₂ hJI)