awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₁ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₁ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
h₂ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₂ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (a₂ ⊗ₜ[R] l₂) :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] 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]

Premises used: add_neg_cancel, _private.0.LieAlgebra.ExtendScalars.bracket'_tmul, lie_skew, mul_comm, TensorProduct.tmul_neg
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₁ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₁ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
h₂ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₂ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
a₁ : A
l₁ : L
y₁ y₂ : A ⊗[R] L
hy₁ :
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          y₁ :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y₁ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (a₁ ⊗ₜ[R] l₁) :
        A ⊗[R] L) =
    0
hy₂ :
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          y₂ :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (a₁ ⊗ₜ[R] l₁) :
        A ⊗[R] L) =
    0
⊢ HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (y₁ + y₂) :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (y₁ + y₂) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (a₁ ⊗ₜ[R] l₁) :
        A ⊗[R] L) =
    0

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

Premises used: LinearMap.add_apply, map_add, add_add_add_comm, add_zero
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₁ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₁ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
h₂ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₂ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
y₁ y₂ : A ⊗[R] L
hy₁ :
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y₁ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          z₂ :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          y₁ :
        A ⊗[R] L) =
    0
hy₂ :
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          z₂ :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          y₂ :
        A ⊗[R] L) =
    0
⊢ HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (y₁ + y₂) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          z₂ :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (y₁ + y₂) :
        A ⊗[R] L) =
    0

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

Premises used: LinearMap.add_apply, map_add, add_add_add_comm, add_zero
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) x : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        z) =
    HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  y) :
              A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          z :
        A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) x : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) :
        A ⊗[R] M)

Tactic:
x.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) 0 : (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        z) =
    HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                (((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) 0 : (a : A ⊗[R] L) → A ⊗[R] L) y) :
              A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          z :
        A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) 0 : (a : A ⊗[R] M) → A ⊗[R] M) z) :
        A ⊗[R] M)

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

Premises used: LinearMap.zero_apply, map_zero, add_zero
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        z) =
    HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                      A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  y) :
              A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          z :
        A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) :
        A ⊗[R] M)

Tactic:
y.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) 0 : (a : A ⊗[R] M) → A ⊗[R] M) z) =
    HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
      (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
              ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                    A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                  (a : A ⊗[R] L) → A ⊗[R] L)
                0) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          z :
        A ⊗[R] M)
      (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) 0 : (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) :
        A ⊗[R] M)

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

Premises used: LinearMap.zero_apply, map_zero, add_zero
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : 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 : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        z) =
    HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                      A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  (a₂ ⊗ₜ[R] l₂)) :
              A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          z :
        A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) :
        A ⊗[R] M)

Tactic:
z.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : 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 : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        0) =
    HAdd.hAdd (α := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
              ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                    A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                  (a : A ⊗[R] L) → A ⊗[R] L)
                (a₂ ⊗ₜ[R] l₂)) :
            A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        0)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          0))

Tactic:
simp only [map_zero, add_zero]

Premises used: map_zero, add_zero
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
refine_2 :
  (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ =
    HAdd.hAdd (α := A ⊗[R] M) ((a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆) ((a₂ * (a₁ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆)
⊢ (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        (a₃ ⊗ₜ[R] l₃)) =
    HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                      A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  (a₂ ⊗ₜ[R] l₂)) :
              A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          (a₃ ⊗ₜ[R] l₃) :
        A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            (a₃ ⊗ₜ[R] l₃)) :
        A ⊗[R] M)

Tactic:
simp only [bracket'_tmul]

Premises used: _private.0.LieAlgebra.ExtendScalars.bracket'_tmul
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
refine_2 :
  (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ =
    HAdd.hAdd (α := A ⊗[R] M) ((a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆)
refine_2₁ :
  (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ =
    HAdd.hAdd (α := A ⊗[R] M) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆)
refine_2₂ :
  (a₁ * (a₂ * a₃)) ⊗ₜ[R] (⁅⁅l₁, l₂⁆, l₃⁆ + ⁅l₂, ⁅l₁, l₃⁆⁆) =
    HAdd.hAdd (α := A ⊗[R] M) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆)
refine_2₃ refine_2₄ :
  HAdd.hAdd (α := A ⊗[R] M) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆) =
    HAdd.hAdd (α := A ⊗[R] M) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆) ((a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆)
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ =
    HAdd.hAdd (α := A ⊗[R] M) ((a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆) ((a₂ * (a₁ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆)

Tactic:
rw [mul_left_comm a₂ a₁ a₃, mul_assoc, leibniz_lie, TensorProduct.tmul_add]

Premises used: leibniz_lie, mul_assoc, mul_left_comm, TensorProduct.tmul_add
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y z : A ⊗[R] L
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

Tactic:
simp only [bracket_def, LinearMap.add_apply, map_add]

Premises used: LinearMap.add_apply, map_add, _private.0.LieAlgebra.ExtendScalars.bracket_def
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y z : A ⊗[R] L
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

Tactic:
simp only [bracket_def, map_add]

Premises used: map_add, _private.0.LieAlgebra.ExtendScalars.bracket_def
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
⊢ ∀ (t : R) (x y : A ⊗[R] L), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
simp [bracket_def]

Premises used: _private.0.LieAlgebra.ExtendScalars.bracket_def
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

Tactic:
simp only [bracket_def, LinearMap.add_apply, map_add]

Premises used: LinearMap.add_apply, map_add, _private.0.LieAlgebra.ExtendScalars.bracket_def
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x : A ⊗[R] L
y z : A ⊗[R] M
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

Tactic:
simp only [bracket_def, map_add]

Premises used: map_add, _private.0.LieAlgebra.ExtendScalars.bracket_def
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
t : A
x : A ⊗[R] L
m : A ⊗[R] M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
simp only [bracket_def, map_smul, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, _private.0.LieAlgebra.ExtendScalars.bracket_def, map_smul
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R_1 : Type u_1
A_1 : Type u_2
L_1 : Type u_3
M : Type u_4
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
inst_3 : LieRing L_1
inst_4 : LieAlgebra R_1 L_1
inst_5 : AddCommGroup M
inst_6 : Module R_1 M
inst_7 : LieRingModule L_1 M
inst_8 : LieModule R_1 L_1 M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst_9 : CommRing R
inst_10 : CommRing A
inst_11 : Algebra R A
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : LieRing L
inst_15 : LieAlgebra R L
inst_16 : LieRing L'
inst_17 : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ Eq (α := B ⊗[R] L')
    ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
        (((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) 0 : (a : A ⊗[R] L) → A ⊗[R] L) y) :
      B ⊗[R] L')
    (((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
            ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') 0) :
          (a : B ⊗[R] L') → B ⊗[R] L')
        ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
      B ⊗[R] L')

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R_1 : Type u_1
A_1 : Type u_2
L_1 : Type u_3
M : Type u_4
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
inst_3 : LieRing L_1
inst_4 : LieAlgebra R_1 L_1
inst_5 : AddCommGroup M
inst_6 : Module R_1 M
inst_7 : LieRingModule L_1 M
inst_8 : LieModule R_1 L_1 M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst_9 : CommRing R
inst_10 : CommRing A
inst_11 : Algebra R A
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : LieRing L
inst_15 : LieAlgebra R L
inst_16 : LieRing L'
inst_17 : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
x_1 : A
refine_1 :
  ∀ (y_1 : L),
    Eq (α := B ⊗[R] L')
      ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
          ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            y) :
        B ⊗[R] L')
      ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x_1 ⊗ₜ[R] y_1)) :
              B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
            (a : B ⊗[R] L') → B ⊗[R] L')
          ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
        B ⊗[R] L')
⊢ ∀ (y_1 : L),
    Eq (α := B ⊗[R] L')
      ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
          ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            y) :
        B ⊗[R] L')
      ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x_1 ⊗ₜ[R] y_1)) :
              B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
            (a : B ⊗[R] L') → B ⊗[R] L')
          ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
        B ⊗[R] L')

Tactic:
_