awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
conv_rhs : map N.incl N' ≤ map N.incl ⊤
⊢ map N.incl N' ≤ N

Tactic:
conv_rhs => rw [← N.map_incl_top]

Premises used: LieSubmodule.map_incl_top
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' ≤ map N.incl ⊤

Tactic:
LieSubmodule.map_mono le_top

Premises used: le_top, LieSubmodule.map_mono
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' ≤ map N.incl ⊤

Tactic:
exact LieSubmodule.map_mono le_top

Premises used: le_top, LieSubmodule.map_mono
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
M : Type u_1
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
x : ↥⊤
⊢ (ofTop R L M : (a : ↥⊤) → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
M : Type u_1
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
M' : Type u_2
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
rw : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := M') (⇑e.toLieModuleHom : (a : M) → M')
⊢ e.range = ⊤

Tactic:
rw [LieModuleHom.range_eq_top]

Premises used: LieModuleHom.range_eq_top
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
M : Type u_1
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
M' : Type u_2
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := M') (⇑e.toLieModuleHom : (a : M) → M')

Tactic:
e.surjective

Premises used: LieModuleEquiv.surjective
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
M : Type u_1
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
M' : Type u_2
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := M') (⇑e.toLieModuleHom : (a : M) → M')

Tactic:
exact e.surjective

Premises used: LieModuleEquiv.surjective
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : ↥⊤
⊢ (topEquiv : (a : ↥⊤) → L) x = (↑x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
simp :
  HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N) +
      HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N) =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N) +
      HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
⊢ (hasBracketAux (x + y) : (a : M ⊗[R] N) → M ⊗[R] N) t =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)

Tactic:
simp only [hasBracketAux, LinearMap.lTensor_add, LinearMap.rTensor_add, map_add,
      LinearMap.add_apply]

Premises used: LinearMap.add_apply, map_add, TensorProduct.LieModule.hasBracketAux, LinearMap.rTensor_add, LinearMap.lTensor_add
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N) +
      HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N) =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) x) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N) +
      HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)
        ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) y) :
              (a : M ⊗[R] N) → M ⊗[R] N)
            t :
          M ⊗[R] N)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
this :
  hasBracketAux x ∘ₗ hasBracketAux y =
    HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x)
rw :
  (HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x) :
        (a : M ⊗[R] N) → M ⊗[R] N)
      t =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux ⁅x, y⁆ : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t) : M ⊗[R] N)
⊢ (hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) t) =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux ⁅x, y⁆ : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t) : M ⊗[R] N)

Tactic:
rw [← LinearMap.comp_apply, this]

Premises used: LinearMap.comp_apply
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
this :
  hasBracketAux x ∘ₗ hasBracketAux y =
    HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x)
⊢ (HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x) :
        (a : M ⊗[R] N) → M ⊗[R] N)
      t =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux ⁅x, y⁆ : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t) : M ⊗[R] N)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
suffices :
  hasBracketAux x ∘ₗ hasBracketAux y =
    HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x)
⊢ (hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) t) =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux ⁅x, y⁆ : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t) : M ⊗[R] N)

Tactic:
suffices (hasBracketAux x).comp (hasBracketAux y) =
        hasBracketAux ⁅x, y⁆ + (hasBracketAux y).comp (hasBracketAux x) by
      rw [← LinearMap.comp_apply, this]; rfl
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
a :
  ∀ (m : M) (n : N),
    Eq (α := M ⊗[R] N)
      (((((AlgebraTensorModule.curry (hasBracketAux x ∘ₗ hasBracketAux y) : M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                  (a : M) → N →ₗ[R] M ⊗[R] N)
                m :
              N →ₗ[R] M ⊗[R] N) :
            (a : N) → M ⊗[R] N)
          n :
        M ⊗[R] N)
      (((((AlgebraTensorModule.curry
                      (HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆)
                        (hasBracketAux y ∘ₗ hasBracketAux x)) :
                    M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                  (a : M) → N →ₗ[R] M ⊗[R] N)
                m :
              N →ₗ[R] M ⊗[R] N) :
            (a : N) → M ⊗[R] N)
          n :
        M ⊗[R] N)
⊢ hasBracketAux x ∘ₗ hasBracketAux y =
    HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆) (hasBracketAux y ∘ₗ hasBracketAux x)

Tactic:
ext m n
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
m : M
n : N
a :
  HAdd.hAdd (α := M ⊗[R] N) (⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n) (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆) +
      HAdd.hAdd (α := M ⊗[R] N) (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆) (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) =
    HSub.hSub (α := M ⊗[R] N) (⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n) (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n) +
        HSub.hSub (α := M ⊗[R] N) (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) (m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆) +
      (HAdd.hAdd (α := M ⊗[R] N) (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n) (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆) +
        HAdd.hAdd (α := M ⊗[R] N) (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆) (m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆))
⊢ Eq (α := M ⊗[R] N)
    (((((AlgebraTensorModule.curry (hasBracketAux x ∘ₗ hasBracketAux y) : M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : M) → N →ₗ[R] M ⊗[R] N)
              m :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)
    (((((AlgebraTensorModule.curry
                    (HAdd.hAdd (α := Module.End R (M ⊗[R] N)) (hasBracketAux ⁅x, y⁆)
                      (hasBracketAux y ∘ₗ hasBracketAux x)) :
                  M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : M) → N →ₗ[R] M ⊗[R] N)
              m :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)

Tactic:
simp only [hasBracketAux, AlgebraTensorModule.curry_apply, curry_apply, sub_tmul, tmul_sub,
      LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.coe_comp,
      LinearMap.rTensor_tmul, LieHom.map_lie, toEnd_apply_apply, LinearMap.add_apply,
      map_add, LieHom.lie_apply, Module.End.lie_apply, LinearMap.lTensor_tmul]

Premises used: LinearMap.rTensor_tmul, LinearMap.add_apply, TensorProduct.tmul_sub, LinearMap.coe_restrictScalars, LieHom.map_lie, map_add, LieHom.lie_apply, Module.End.lie_apply, TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.sub_tmul, LieModule.toEnd_apply_apply, LinearMap.coe_comp, TensorProduct.curry_apply, Function.comp_apply, TensorProduct.LieModule.hasBracketAux, LinearMap.lTensor_tmul
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
m : M
n : N
⊢ HAdd.hAdd (α := M ⊗[R] N) (⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n) (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆) +
      HAdd.hAdd (α := M ⊗[R] N) (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆) (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) =
    HSub.hSub (α := M ⊗[R] N) (⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n) (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n) +
        HSub.hSub (α := M ⊗[R] N) (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) (m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆) +
      (HAdd.hAdd (α := M ⊗[R] N) (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n) (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆) +
        HAdd.hAdd (α := M ⊗[R] N) (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆) (m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆))

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
c : R
x : L
t : M ⊗[R] N
⊢ (hasBracketAux (c • x) : (a : M ⊗[R] N) → M ⊗[R] N) t =
    HSMul.hSMul (β := M ⊗[R] N) c ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)

Tactic:
simp only [hasBracketAux, smul_add, LinearMap.rTensor_smul, LinearMap.smul_apply,
      LinearMap.lTensor_smul, map_smul, LinearMap.add_apply]

Premises used: LinearMap.lTensor_smul, LinearMap.smul_apply, LinearMap.add_apply, TensorProduct.LieModule.hasBracketAux, LinearMap.rTensor_smul, smul_add, map_smul
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x : L
m : M
n : N
⊢ (hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) (m ⊗ₜ[R] n) =
    HAdd.hAdd (α := M ⊗[R] N) (⁅x, m⁆ ⊗ₜ[R] n) (m ⊗ₜ[R] ⁅x, n⁆)

Tactic:
simp only [hasBracketAux, LinearMap.rTensor_tmul, toEnd_apply_apply,
      LinearMap.add_apply, LinearMap.lTensor_tmul]

Premises used: LinearMap.rTensor_tmul, LinearMap.add_apply, LieModule.toEnd_apply_apply, TensorProduct.LieModule.hasBracketAux, LinearMap.lTensor_tmul
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x : L
f : M →ₗ[R] N →ₗ[R] P
a :
  ∀ (m : M) (n : N),
    Eq.{w₂ + 1} (α := P)
      (((((AlgebraTensorModule.curry
                      (AddHom.toFun
                        (LinearMap.toAddHom
                          (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                        ⁅x, f⁆) :
                    M →ₗ[R] N →ₗ[R] P) :
                  (a : M) → N →ₗ[R] P)
                m :
              N →ₗ[R] P) :
            (a : N) → P)
          n :
        P)
      (((((AlgebraTensorModule.curry
                      ⁅x,
                        AddHom.toFun
                          (LinearMap.toAddHom
                            (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                          f⁆ :
                    M →ₗ[R] N →ₗ[R] P) :
                  (a : M) → N →ₗ[R] P)
                m :
              N →ₗ[R] P) :
            (a : N) → P)
          n :
        P)
⊢ AddHom.toFun (LinearMap.toAddHom (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
      ⁅x, f⁆ =
    ⁅x,
      AddHom.toFun
        (LinearMap.toAddHom (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P)) f⁆

Tactic:
ext m n
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
a :
  HSub.hSub (β := P)
      (HSub.hSub (α := P) (β := P) (⁅x, (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n⁆ : P)
        ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) ⁅x, n⁆ : P))
      ((((f : (a : M) → N →ₗ[R] P) ⁅x, m⁆ : N →ₗ[R] P) : (a : N) → P) n : P) =
    HSub.hSub (α := P) (⁅x, (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n⁆ : P)
      (HAdd.hAdd (α := P) (β := P) ((((f : (a : M) → N →ₗ[R] P) ⁅x, m⁆ : N →ₗ[R] P) : (a : N) → P) n : P)
        ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) ⁅x, n⁆ : P))
⊢ Eq.{w₂ + 1} (α := P)
    (((((AlgebraTensorModule.curry
                    (AddHom.toFun
                      (LinearMap.toAddHom
                        (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                      ⁅x, f⁆) :
                  M →ₗ[R] N →ₗ[R] P) :
                (a : M) → N →ₗ[R] P)
              m :
            N →ₗ[R] P) :
          (a : N) → P)
        n :
      P)
    (((((AlgebraTensorModule.curry
                    ⁅x,
                      AddHom.toFun
                        (LinearMap.toAddHom
                          (↑(lift.equiv (RingHom.id R) M N P) : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P))
                        f⁆ :
                  M →ₗ[R] N →ₗ[R] P) :
                (a : M) → N →ₗ[R] P)
              m :
            N →ₗ[R] P) :
          (a : N) → P)
        n :
      P)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
        AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
        lift.equiv_apply, LieHom.lie_apply, LinearMap.sub_apply, lie_tmul_right, map_add]

Premises used: LinearMap.coe_restrictScalars, AddHom.toFun_eq_coe, map_add, LieHom.lie_apply, TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.LieModule.lie_tmul_right, TensorProduct.curry_apply, LinearMap.coe_toAddHom, LinearMap.sub_apply, LinearEquiv.coe_coe, TensorProduct.lift.equiv_apply