-- 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 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)
⊢ (P I) S = (P J) T

Tactic:
have : S = Finset.restrict₂ hJI ⁻¹' T :=
  eq_of_cylinder_eq_of_subset h_eq hJI

Result:
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

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)
⊢ (P I) S = (P J) T

Tactic:
suffices ∀ I, P I univ = 0 by
  simp only [Measure.measure_univ_eq_zero] at this
  simp [this]

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

Tactic:
obtain ⟨i, hi_empty⟩ := h

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:
ι : 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)
⊢ univ = ∅

Tactic:
simp [hi_empty]

Result:
no goals