case intro
α β : Type u
ι : Type u_1
f : ι → Type u
⊢ (prod fun i => #f i) = 0 ↔ ∃ i, (fun i => #f i) i = 0
α β : Type u
ι : Type u_1
f : ι → Cardinal
⊢ prod f = 0 ↔ ∃ i, f i = 0
lift f to ι → Type u using fun _ => trivial
no goals
case intro
α β : Type u
ι : Type u_1
f : ι → Type u
⊢ (prod fun i => #f i) = 0 ↔ ∃ i, (fun i => #f i) i = 0
simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]