Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case 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
⊢ ((bracket' R A L M) 0) (((bracket' R A L M) y) z) =
    ((bracket' R A L M) (((bracket' R A L L) 0) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) 0) z)

pp: case 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
⊢ ∀ (x : A) (y_1 : L),
    ((bracket' R A L M) (x ⊗ₜ[R] y_1)) (((bracket' R A L M) y) z) =
      ((bracket' R A L M) (((bracket' R A L L) (x ⊗ₜ[R] y_1)) y)) z +
        ((bracket' R A L M) y) (((bracket' R A L M) (x ⊗ₜ[R] y_1)) z)

pp: case 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
⊢ ∀ (x y_1 : A ⊗[R] L),
    ((bracket' R A L M) x) (((bracket' R A L M) y) z) =
        ((bracket' R A L M) (((bracket' R A L L) x) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) x) z) →
      ((bracket' R A L M) y_1) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) y_1) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) y_1) z) →
        ((bracket' R A L M) (x + y_1)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (x + y_1)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (x + y_1)) z)

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

Goal state after:
case 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
⊢ ∀ (x : A) (y_1 : L),
    ((bracket' R A L M) (x ⊗ₜ[R] y_1)) (((bracket' R A L M) y) z) =
      ((bracket' R A L M) (((bracket' R A L L) (x ⊗ₜ[R] y_1)) y)) z +
        ((bracket' R A L M) y) (((bracket' R A L M) (x ⊗ₜ[R] y_1)) z)

case 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
⊢ ∀ (x y_1 : A ⊗[R] L),
    ((bracket' R A L M) x) (((bracket' R A L M) y) z) =
        ((bracket' R A L M) (((bracket' R A L L) x) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) x) z) →
      ((bracket' R A L M) y_1) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) y_1) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) y_1) z) →
        ((bracket' R A L M) (x + y_1)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (x + y_1)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (x + y_1)) z)