no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (j : Fin (n + 1)) → AddGroup (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (↑(succAbove i) j)
⊢ insertNth i x p - insertNth i y p = Pi.single i (x - y)
simp_rw [← insertNth_sub, ← insertNth_zero_right, Pi.sub_def, sub_self, Pi.zero_def]