no goals
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s t : A
x y : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (s ⊗ₜ[R] x)) (t ⊗ₜ[R] y) = (s * t) ⊗ₜ[R] ⁅x, y⁆
simp [bracket']