-- Mathlib/Algebra/Lie/BaseChange.lean
theorem bracket_lie_self (x : A ⊗[R] L) : ⁅x, x⁆ = 0

Proof state:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
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 L) (a ⊗ₜ[R] l)) (a ⊗ₜ[R] l) = 0

Tactic:
simp only [bracket'_tmul, TensorProduct.tmul_zero, eq_self_iff_true, lie_self]

Result:
no goals

Proof state:
case refine_3.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) z₂ +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) (a₁ ⊗ₜ[R] l₁) =
    0

Tactic:
refine z₂.induction_on ?_ ?_ ?_

Result:
case refine_3.refine_2.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) 0 +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) 0) (a₁ ⊗ₜ[R] l₁) =
    0

case refine_3.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y) +
        ((LieAlgebra.ExtendScalars.bracket' R A L L) (x ⊗ₜ[R] y)) (a₁ ⊗ₜ[R] l₁) =
      0

case refine_3.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x +
          ((LieAlgebra.ExtendScalars.bracket' R A L L) x) (a₁ ⊗ₜ[R] l₁) =
        0 →
      ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y +
            ((LieAlgebra.ExtendScalars.bracket' R A L L) y) (a₁ ⊗ₜ[R] l₁) =
          0 →
        ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y) +
            ((LieAlgebra.ExtendScalars.bracket' R A L L) (x + y)) (a₁ ⊗ₜ[R] l₁) =
          0

Proof state:
case refine_3.refine_2.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) 0 +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) 0) (a₁ ⊗ₜ[R] l₁) =
    0

Tactic:
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (z₁ + z₂)) (z₁ + z₂) = 0

Tactic:
suffices bracket' R A L L z₁ z₂ + bracket' R A L 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]

Result:
case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) z₁) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₁ = 0

Proof state:
case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) z₁) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₁ = 0

Tactic:
refine z₁.induction_on ?_ ?_ ?_

Result:
case refine_3.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) 0) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) 0 = 0

case refine_3.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ∀ (x : A) (y : L),
    ((LieAlgebra.ExtendScalars.bracket' R A L L) (x ⊗ₜ[R] y)) z₂ +
        ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) (x ⊗ₜ[R] y) =
      0

case refine_3.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ∀ (x y : A ⊗[R] L),
    ((LieAlgebra.ExtendScalars.bracket' R A L L) x) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) x = 0 →
      ((LieAlgebra.ExtendScalars.bracket' R A L L) y) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) y = 0 →
        ((LieAlgebra.ExtendScalars.bracket' R A L L) (x + y)) z₂ +
            ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) (x + y) =
          0

Proof state:
case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
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 L) 0) 0 = 0

Tactic:
simp only [LinearMap.map_zero, eq_self_iff_true, LinearMap.zero_apply]

Result:
no goals

Proof state:
case refine_3.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) 0) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) 0 = 0

Tactic:
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]

Result:
no goals

Proof state:
case refine_3.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
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 L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂) +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₂ ⊗ₜ[R] l₂)) (a₁ ⊗ₜ[R] l₁) =
    0

Tactic:
simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul,
  add_neg_cancel]

Result:
no goals