Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2.refine_1
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
⊢ ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) 0) =
    ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) 0 +
      ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) 0)

pp: 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),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x ⊗ₜ[R] y) +
        ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))

pp: 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
⊢ ∀ (x y : A ⊗[R] M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) x) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) x +
          ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) x) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) y) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) y +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) y) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x + y) +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x + y))

Tactic:
· simp only [map_zero, add_zero]

Goal state after:
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),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x ⊗ₜ[R] y) +
        ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))

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
⊢ ∀ (x y : A ⊗[R] M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) x) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) x +
          ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) x) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) y) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) y +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) y) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x + y) +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x + y))