no goals
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_2
inst✝ : CommRing S
α : Type u_1
β : Type u_3
f : α →₀ S
g : β →₀ S
a : α
b : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (f ⊗ₜ[S] g)) (a, b) = ↑f a * ↑g b
simp [finsuppTensorFinsupp']