case inl
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : IsEmpty ι
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)

case inr
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
cases isEmpty_or_nonempty ι
case inr.inl
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)

case inr.inr
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.Nonempty (Set.pi univ s)
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
case inr
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
cases' (pi univ s).eq_empty_or_nonempty with h h
no goals
case inl
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : IsEmpty ι
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
simp [piPremeasure]
case inr.inl.intro
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
case inr.inl
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
case inr.inl.intro
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
this : ∃ i, ↑(m i) (s i) = 0
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
case inr.inl.intro
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
no goals
case inr.inl.intro
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
this : ∃ i, ↑(m i) (s i) = 0
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
simpa [h, Finset.card_univ, zero_pow (Fintype.card_pos_iff.mpr ‹_›), @eq_comm _ (0 : ℝ≥0∞),
  Finset.prod_eq_zero_iff, piPremeasure]
no goals
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
⊢ ↑(m i) (s i) = 0
simp [hi]
no goals
case inr.inr
ι : Type u_2
ι' : Type ?u.1509037
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.Nonempty (Set.pi univ s)
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
simp [h, piPremeasure]