n : ℕ
α : TypeVec (n + 1)
α' : TypeVec (n + 1)
f f' : drop α ⟹ drop α'
g g' : last α → last α'
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'
n : ℕ
α : TypeVec (n + 1)
α' : TypeVec (n + 1)
f f' : drop α ⟹ drop α'
g g' : last α → last α'
H : splitFun f g = splitFun f' g'
⊢ f = f' ∧ g = g'
rw [← dropFun_splitFun f g, H, ← lastFun_splitFun f g, H]
no goals
n : ℕ
α : TypeVec (n + 1)
α' : TypeVec (n + 1)
f f' : drop α ⟹ drop α'
g g' : last α → last α'
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'
simp