case h
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : last (α ⊗ α')
⊢ lastFun (f ⊗' f') i = Prod.map (lastFun f) (lastFun f') i
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ lastFun (f ⊗' f') = Prod.map (lastFun f) (lastFun f')
ext i : 1
case h.mk
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : last α
snd✝ : last α'
⊢ lastFun (f ⊗' f') (fst✝, snd✝) = Prod.map (lastFun f) (lastFun f') (fst✝, snd✝)
case h
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : last (α ⊗ α')
⊢ lastFun (f ⊗' f') i = Prod.map (lastFun f) (lastFun f') i
induction i
case h.mk
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : last α
snd✝ : last α'
⊢ (f ⊗' f') Fin2.fz (fst✝, snd✝) = Prod.map (f Fin2.fz) (f' Fin2.fz) (fst✝, snd✝)
case h.mk
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : last α
snd✝ : last α'
⊢ lastFun (f ⊗' f') (fst✝, snd✝) = Prod.map (lastFun f) (lastFun f') (fst✝, snd✝)
simp [lastFun, *]
no goals
case h.mk
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : last α
snd✝ : last α'
⊢ (f ⊗' f') Fin2.fz (fst✝, snd✝) = Prod.map (f Fin2.fz) (f' Fin2.fz) (fst✝, snd✝)
rfl