no goals
R : Type u
inst✝⁴ : CommSemiring R
A : Type v₁
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type v₂
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A ⊗[R] B
⊢ ↑(↑mul x) (1 ⊗ₜ[R] 1) = x
refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp (config := { contextual := true })