no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (j : Fin (n + 1)) → Zero (α j)
i : Fin (n + 1)
x : α i
⊢ Pi.single i x i = x ∧ 0 = fun j => Pi.single i x (↑(succAbove i) j)
simp [succAbove_ne, Pi.zero_def]