-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma eq_zero_of_isEmpty [h : IsEmpty (Π i, α i)]
    (hP : IsProjectiveMeasureFamily P) (I : Finset ι) :
    P I = 0

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
⊢ P I = 0

Tactic:
rw [hP (insert i I) I (I.subset_insert i)]

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
⊢ Measure.map (Finset.restrict₂ ⋯) (P (insert i I)) = 0

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
⊢ IsEmpty ((j : { x // x ∈ insert i I }) → α ↑j)

Tactic:
simp [hi]

Result:
no goals

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
this : IsEmpty ((j : { x // x ∈ insert i I }) → α ↑j)
⊢ Measure.map (Finset.restrict₂ ⋯) (P (insert i I)) = 0

Tactic:
rw [(P (insert i I)).eq_zero_of_isEmpty]

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
this : IsEmpty ((j : { x // x ∈ insert i I }) → α ↑j)
⊢ Measure.map (Finset.restrict₂ ⋯) 0 = 0

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
⊢ P I = 0

Tactic:
obtain ⟨i, hi⟩ := isEmpty_pi.mp h

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
⊢ P I = 0

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
⊢ Measure.map (Finset.restrict₂ ⋯) (P (insert i I)) = 0

Tactic:
have : IsEmpty (Π j : ↑(insert i I), α j) := by simp [hi]

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
this : IsEmpty ((j : { x // x ∈ insert i I }) → α ↑j)
⊢ Measure.map (Finset.restrict₂ ⋯) (P (insert i I)) = 0

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
this : IsEmpty ((j : { x // x ∈ insert i I }) → α ↑j)
⊢ Measure.map (Finset.restrict₂ ⋯) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
⊢ P I = 0

Tactic:
classical
obtain ⟨i, hi⟩ := isEmpty_pi.mp h
rw [hP (insert i I) I (I.subset_insert i)]
have : IsEmpty (Π j : ↑(insert i I), α j) := by simp [hi]
rw [(P (insert i I)).eq_zero_of_isEmpty]
simp

Result:
no goals