case h.mk
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_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
a' : α
b' : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂)) (a', b') =
    ↑(Finsupp.single (a, b) (r₁ * r₂)) (a', b')
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_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
⊢ ↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂)
ext ⟨a', b'⟩
no goals
case h.mk
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_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
a' : α
b' : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂)) (a', b') =
    ↑(Finsupp.single (a, b) (r₁ * r₂)) (a', b')
aesop (add norm [Finsupp.single_apply])