-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem piPremeasure_pi' {s : ∀ i, Set (α i)} : piPremeasure m (pi univ s) = ∏ i, m i (s i)

Proof state:
case inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : IsEmpty ι
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
simp [piPremeasure]

Result:
no goals

Proof state:
case inr.inl.intro
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
this : ∃ i, (m i) (s i) = 0
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
simpa [h, Finset.card_univ, zero_pow Fintype.card_ne_zero, @eq_comm _ (0 : ℝ≥0∞),
  Finset.prod_eq_zero_iff, piPremeasure]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : IsEmpty ι
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

case inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Proof state:
case inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
rcases (pi univ s).eq_empty_or_nonempty with h | h

Result:
case inr.inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

case inr.inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : (univ.pi s).Nonempty
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Proof state:
case inr.inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : (univ.pi s).Nonempty
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
simp [h, piPremeasure]

Result:
no goals

Proof state:
case inr.inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩

Result:
case inr.inl.intro
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
⊢ (m i) (s i) = 0

Tactic:
simp [hi]

Result:
no goals

Proof state:
case inr.inl.intro
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩

Result:
case inr.inl.intro
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
this : ∃ i, (m i) (s i) = 0
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)