-- Mathlib/Algebra/Lie/BaseChange.lean
theorem bracket_leibniz_lie (x y : A ⊗[R] L) (z : A ⊗[R] M) :
    ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆

Proof state:
case refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((LieAlgebra.ExtendScalars.bracket' R A L M) x) z) =
        ((LieAlgebra.ExtendScalars.bracket' R A L M) (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x))
            z +
          ((LieAlgebra.ExtendScalars.bracket' R A L M) x)
            (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
      ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((LieAlgebra.ExtendScalars.bracket' R A L M) y) z) =
          ((LieAlgebra.ExtendScalars.bracket' R A L M) (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y))
              z +
            ((LieAlgebra.ExtendScalars.bracket' R A L M) y)
              (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
        ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
            (((LieAlgebra.ExtendScalars.bracket' R A L M) (x + y)) z) =
          ((LieAlgebra.ExtendScalars.bracket' R A L M)
                (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y)))
              z +
            ((LieAlgebra.ExtendScalars.bracket' R A L M) (x + y))
              (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Tactic:
intro u₁ u₂ h₁ h₂

Result:
case refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
u₁ u₂ : A ⊗[R] L
h₁ :
  ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((LieAlgebra.ExtendScalars.bracket' R A L M) u₁) z) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M) (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) u₁)) z +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) u₁) (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)
h₂ :
  ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((LieAlgebra.ExtendScalars.bracket' R A L M) u₂) z) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M) (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) u₂)) z +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) u₂) (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
      (((LieAlgebra.ExtendScalars.bracket' R A L M) (u₁ + u₂)) z) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M)
          (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (u₁ + u₂)))
        z +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) (u₁ + u₂))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Proof state:
case refine_2.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
u₁ u₂ : A ⊗[R] M
h₁ :
  ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
      (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) u₁) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M)
          (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        u₁ +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) u₁)
h₂ :
  ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
      (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) u₂) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M)
          (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        u₂ +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) u₂)
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
      (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (u₁ + u₂)) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M)
          (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        (u₁ + u₂) +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (u₁ + u₂))

Tactic:
rw [map_add, map_add, map_add, map_add, map_add, h₁, h₂, add_add_add_comm]

Result:
no goals

Proof state:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₂ * (a₁ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆

Tactic:
rw [mul_left_comm a₂ a₁ a₃, mul_assoc, leibniz_lie, TensorProduct.tmul_add]

Result:
no goals

Proof state:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x : A) (y : M),
    ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ((LieAlgebra.ExtendScalars.bracket' R A L M)
            (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
          (x ⊗ₜ[R] y) +
        ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂))
          (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))

Tactic:
intro a₃ l₃

Result:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
      (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (a₃ ⊗ₜ[R] l₃)) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M)
          (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        (a₃ ⊗ₜ[R] l₃) +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (a₃ ⊗ₜ[R] l₃))