ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i : ι
xi : β i
⊢ i = i ∧ HEq xi 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i : ι
xi : β i
⊢ single i xi = 0 ↔ xi = 0
rw [← single_zero i, single_eq_single_iff]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i : ι
xi : β i
⊢ i = i ∧ HEq xi 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0
simp