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 y z : A ⊗[R] B
a₁✝ a₂✝ a₃✝ : A
b₁✝ b₂✝ b₃✝ : B
⊢ ↑(↑mul (↑(↑mul (a₁✝ ⊗ₜ[R] b₁✝)) (a₂✝ ⊗ₜ[R] b₂✝))) (a₃✝ ⊗ₜ[R] b₃✝) =
    ↑(↑mul (a₁✝ ⊗ₜ[R] b₁✝)) (↑(↑mul (a₂✝ ⊗ₜ[R] b₂✝)) (a₃✝ ⊗ₜ[R] b₃✝))
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 y z : A ⊗[R] B
⊢ ∀ (a₁ a₂ a₃ : A) (b₁ b₂ b₃ : B),
    ↑(↑mul (↑(↑mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂))) (a₃ ⊗ₜ[R] b₃) =
      ↑(↑mul (a₁ ⊗ₜ[R] b₁)) (↑(↑mul (a₂ ⊗ₜ[R] b₂)) (a₃ ⊗ₜ[R] b₃))
intros
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 y z : A ⊗[R] B
a₁✝ a₂✝ a₃✝ : A
b₁✝ b₂✝ b₃✝ : B
⊢ ↑(↑mul (↑(↑mul (a₁✝ ⊗ₜ[R] b₁✝)) (a₂✝ ⊗ₜ[R] b₂✝))) (a₃✝ ⊗ₜ[R] b₃✝) =
    ↑(↑mul (a₁✝ ⊗ₜ[R] b₁✝)) (↑(↑mul (a₂✝ ⊗ₜ[R] b₂✝)) (a₃✝ ⊗ₜ[R] b₃✝))
simp only [mul_apply, mul_assoc]