case a.h
n : ℕ
α : TypeVec (n + 1)
i : Fin2 n
x✝ : drop α i
⊢ dropFun prod.diag i x✝ = prod.diag i x✝
n : ℕ
α : TypeVec (n + 1)
⊢ dropFun prod.diag = prod.diag
ext i : 2
no goals
case a.h
n : ℕ
α : TypeVec (n + 1)
i : Fin2 n
x✝ : drop α i
⊢ dropFun prod.diag i x✝ = prod.diag i x✝
induction i <;> simp [dropFun, *] <;> rfl