[GOAL]
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
x : A ⊗[R] L
⊢ ⁅x, x⁆ = 0
[PROOFSTEP]
simp only [bracket_def]
[GOAL]
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
x : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) x = 0
[PROOFSTEP]
refine' x.induction_on _ _ _
[GOAL]
case refine'_1
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
x : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) 0 = 0
[PROOFSTEP]
simp only [LinearMap.map_zero, eq_self_iff_true, LinearMap.zero_apply]
[GOAL]
case refine'_2
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
x : A ⊗[R] L
⊢ ∀ (x : A) (y : L), ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) (x ⊗ₜ[R] y) = 0
[PROOFSTEP]
intro a l
[GOAL]
case refine'_2
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
x : A ⊗[R] L
a : A
l : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a ⊗ₜ[R] l)) (a ⊗ₜ[R] l) = 0
[PROOFSTEP]
simp only [bracket'_tmul, TensorProduct.tmul_zero, eq_self_iff_true, lie_self]
[GOAL]
case refine'_3
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
x : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) x = 0 →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) y = 0 →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) (x + y) = 0
[PROOFSTEP]
intro z₁ z₂ h₁ h₂
[GOAL]
case refine'_3
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (z₁ + z₂)) (z₁ + z₂) = 0
[PROOFSTEP]
suffices bracket' R A L z₁ z₂ + bracket' R A L z₂ z₁ = 0 by
  rw [LinearMap.map_add, LinearMap.map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂, zero_add, add_zero,
    add_comm, this]
[GOAL]
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
this : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₁ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (z₁ + z₂)) (z₁ + z₂) = 0
[PROOFSTEP]
rw [LinearMap.map_add, LinearMap.map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂, zero_add, add_zero,
  add_comm, this]
[GOAL]
case refine'_3
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₁ = 0
[PROOFSTEP]
refine' z₁.induction_on _ _ _
[GOAL]
case refine'_3.refine'_1
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) 0 = 0
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_3.refine'_2
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) z₂ +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (x ⊗ₜ[R] y) =
      0
[PROOFSTEP]
intro a₁ l₁
[GOAL]
case refine'_3.refine'_2
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
refine' z₂.induction_on _ _ _
[GOAL]
case refine'_3.refine'_2.refine'_1
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) 0 +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_3.refine'_2.refine'_2
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y) +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) (a₁ ⊗ₜ[R] l₁) =
      0
[PROOFSTEP]
intro a₂ l₂
[GOAL]
case refine'_3.refine'_2.refine'_2
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul, add_right_neg]
[GOAL]
case refine'_3.refine'_2.refine'_3
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) x +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) (a₁ ⊗ₜ[R] l₁) =
        0 →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (a₁ ⊗ₜ[R] l₁) =
          0 →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x + y) +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) (a₁ ⊗ₜ[R] l₁) =
          0
[PROOFSTEP]
intro y₁ y₂ hy₁ hy₂
[GOAL]
case refine'_3.refine'_2.refine'_3
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
y₁ y₂ : A ⊗[R] L
hy₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y₁ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₁) (a₁ ⊗ₜ[R] l₁) =
    0
hy₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₂) (a₁ ⊗ₜ[R] l₁) =
    0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (y₁ + y₂) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (y₁ + y₂)) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
simp only [hy₁, hy₂, add_add_add_comm, add_zero, LinearMap.add_apply, LinearMap.map_add]
[GOAL]
case refine'_3.refine'_3
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) x = 0 →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) y = 0 →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) z₂ +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (x + y) =
          0
[PROOFSTEP]
intro y₁ y₂ hy₁ hy₂
[GOAL]
case refine'_3.refine'_3
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
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
y₁ y₂ : A ⊗[R] L
hy₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₁) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) y₁ = 0
hy₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₂) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) y₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (y₁ + y₂)) z₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (y₁ + y₂) =
    0
[PROOFSTEP]
simp only [add_add_add_comm, hy₁, hy₂, add_zero, LinearMap.add_apply, LinearMap.map_add]
[GOAL]
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
x y z : A ⊗[R] L
⊢ ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
[PROOFSTEP]
simp only [bracket_def]
[GOAL]
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
x y z : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z)
[PROOFSTEP]
refine' x.induction_on _ _ _
[GOAL]
case refine'_1
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
x y z : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) z)
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_2
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
x y z : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y_1)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y_1)) y)) z +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y_1)) z)
[PROOFSTEP]
intro a₁ l₁
[GOAL]
case refine'_2
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
refine' y.induction_on _ _ _
[GOAL]
case refine'_2.refine'_1
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) 0)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_2.refine'_2
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) z) =
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y)))
          z +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y))
          (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
intro a₂ l₂
[GOAL]
case refine'_2.refine'_2
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
refine' z.induction_on _ _ _
[GOAL]
case refine'_2.refine'_2.refine'_1
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) 0) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        0 +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) 0)
[PROOFSTEP]
rw [LinearMap.map_zero, LinearMap.map_zero, LinearMap.map_zero, LinearMap.map_zero, add_zero]
[GOAL]
case refine'_2.refine'_2.refine'_2
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
          (x ⊗ₜ[R] y) +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
          (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))
[PROOFSTEP]
intro a₃ l₃
[GOAL]
case refine'_2.refine'_2.refine'_2
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (a₃ ⊗ₜ[R] l₃)) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        (a₃ ⊗ₜ[R] l₃) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₃ ⊗ₜ[R] l₃))
[PROOFSTEP]
simp only [bracket'_tmul]
[GOAL]
case refine'_2.refine'_2.refine'_2
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : L
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₂ * (a₁ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆
[PROOFSTEP]
rw [mul_left_comm a₂ a₁ a₃, mul_assoc, leibniz_lie, TensorProduct.tmul_add]
[GOAL]
case refine'_2.refine'_2.refine'_3
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
          (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) x) =
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
            x +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) x) →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) y) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                  (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
              y +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y) →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                  (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
              (x + y) +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x + y))
[PROOFSTEP]
intro u₁ u₂ h₁ h₂
[GOAL]
case refine'_2.refine'_2.refine'_3
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
u₁ u₂ : A ⊗[R] L
h₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) u₁) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        u₁ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₁)
h₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) u₂) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        u₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₂)
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (u₁ + u₂)) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        (u₁ + u₂) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (u₁ + u₂))
[PROOFSTEP]
rw [map_add, map_add, map_add, map_add, map_add, h₁, h₂, add_add_add_comm]
[GOAL]
case refine'_2.refine'_3
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z) =
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) x))
            z +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z) →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y))
              z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y)
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z) →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                  (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x + y)))
              z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y))
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
intro u₁ u₂ h₁ h₂
[GOAL]
case refine'_2.refine'_3
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
x y z : A ⊗[R] L
a₁ : A
l₁ : L
u₁ u₂ : A ⊗[R] L
h₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₁)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
h₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₂)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (u₁ + u₂)))
        z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
rw [map_add, LinearMap.add_apply, LinearMap.add_apply, map_add, map_add, map_add, LinearMap.add_apply, h₁, h₂,
  add_add_add_comm]
[GOAL]
case refine'_3
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
x y z : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) y)) z +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z) →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y_1) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y_1) y)) z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y_1) z) →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y_1)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y_1)) y)) z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y_1)) z)
[PROOFSTEP]
intro u₁ u₂ h₁ h₂
[GOAL]
case refine'_3
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
x y z u₁ u₂ : A ⊗[R] L
h₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) z)
h₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) z)
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) z)
[PROOFSTEP]
rw [map_add, LinearMap.add_apply, LinearMap.add_apply, LinearMap.add_apply, map_add, map_add, LinearMap.add_apply, h₁,
  h₂, add_add_add_comm]
[GOAL]
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
x y z : A ⊗[R] L
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
[PROOFSTEP]
simp only [bracket_def, LinearMap.add_apply, LinearMap.map_add]
[GOAL]
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
x y z : A ⊗[R] L
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
[PROOFSTEP]
simp only [bracket_def, LinearMap.map_add]
