-- Mathlib/Algebra/Lie/BaseChange.lean
theorem bracket_lie_self (x : A ⊗[R] L) : ⁅x, x⁆ = 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 : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ((LieAlgebra.ExtendScalars.bracket' R A L L) x) x = 0 →
      ((LieAlgebra.ExtendScalars.bracket' R A L L) y) y = 0 →
        ((LieAlgebra.ExtendScalars.bracket' R A L L) (x + y)) (x + y) = 0

Tactic:
intro z₁ z₂ h₁ h₂

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₂)) (z₁ + z₂) = 0

Proof state:
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
⊢ ⁅x, x⁆ = 0

Tactic:
simp only [bracket_def]

Result:
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) x) x = 0

Proof state:
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

Tactic:
intro y₁ y₂ hy₁ hy₂

Result:
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
y₁ y₂ : A ⊗[R] L
hy₁ : ((LieAlgebra.ExtendScalars.bracket' R A L L) y₁) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) y₁ = 0
hy₂ : ((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) (y₁ + y₂)) z₂ +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) (y₁ + y₂) =
    0

Proof state:
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

Tactic:
intro y₁ y₂ hy₁ hy₂

Result:
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
y₁ y₂ : A ⊗[R] L
hy₁ :
  ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y₁ +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) y₁) (a₁ ⊗ₜ[R] l₁) =
    0
hy₂ :
  ((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₁)) (y₁ + y₂) +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) (y₁ + y₂)) (a₁ ⊗ₜ[R] l₁) =
    0

Proof state:
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
this : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₁) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₁ = 0
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (z₁ + z₂)) (z₁ + z₂) = 0

Tactic:
rw [LinearMap.map_add, LinearMap.map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
  zero_add, add_zero, add_comm, this]

Result:
no goals

Proof state:
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
y₁ y₂ : A ⊗[R] L
hy₁ : ((LieAlgebra.ExtendScalars.bracket' R A L L) y₁) z₂ + ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) y₁ = 0
hy₂ : ((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) (y₁ + y₂)) z₂ +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) (y₁ + y₂) =
    0

Tactic:
simp only [add_add_add_comm, hy₁, hy₂, add_zero, LinearMap.add_apply, LinearMap.map_add]

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
⊢ ∀ (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

Tactic:
intro a₂ l₂

Result:
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

Proof state:
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
y₁ y₂ : A ⊗[R] L
hy₁ :
  ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y₁ +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) y₁) (a₁ ⊗ₜ[R] l₁) =
    0
hy₂ :
  ((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₁)) (y₁ + y₂) +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) (y₁ + y₂)) (a₁ ⊗ₜ[R] l₁) =
    0

Tactic:
simp only [hy₁, hy₂, add_add_add_comm, add_zero, LinearMap.add_apply, LinearMap.map_add]

Result:
no goals