awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y_1 z : L
m n : M
x y : L
f : M →ₗ[R] N
h :
  ∀ (n : M),
    Eq.{w₁ + 1} (α := N)
      (({
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x + y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x + y, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : M) → N)
          n :
        N)
      ((HAdd.hAdd (α := M →ₗ[R] N)
              {
                toFun := fun (m : M) ↦
                  HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
              {
                toFun := fun (m : M) ↦
                  HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
            (a : M) → N)
          n :
        N)
⊢ {
      toFun := fun (m : M) ↦
        HSub.hSub (α := N) (β := N) (⁅x + y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x + y, m⁆ : N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] N)
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y_1 z : L
m n_1 : M
x y : L
f : M →ₗ[R] N
n : M
h :
  HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) (⁅y, (f : (a : M) → N) n⁆ : N) -
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, n⁆ : N) ((f : (a : M) → N) ⁅y, n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅y, n⁆ : N)
⊢ Eq.{w₁ + 1} (α := N)
    (({
            toFun := fun (m : M) ↦
              HSub.hSub (α := N) (β := N) (⁅x + y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x + y, m⁆ : N),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → N)
        n :
      N)
    ((HAdd.hAdd (α := M →ₗ[R] N)
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
          (a : M) → N)
        n :
      N)

Tactic:
simp only [add_lie, coe_mk, AddHom.coe_mk, add_apply, map_add]

Premises used: LinearMap.coe_mk, LinearMap.add_apply, map_add, AddHom.coe_mk, add_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y_1 z : L
m n_1 : M
x y : L
f : M →ₗ[R] N
n : M
⊢ HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) (⁅y, (f : (a : M) → N) n⁆ : N) -
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, n⁆ : N) ((f : (a : M) → N) ⁅y, n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅y, n⁆ : N)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m n : M
x : L
f g : M →ₗ[R] N
h :
  ∀ (n : M),
    Eq.{w₁ + 1} (α := N)
      (({
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (f + g : (a : M) → N) m⁆ : N) ((f + g : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : M) → N)
          n :
        N)
      ((HAdd.hAdd (α := M →ₗ[R] N)
              {
                toFun := fun (m : M) ↦
                  HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
              {
                toFun := fun (m : M) ↦
                  HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) m⁆ : N) ((g : (a : M) → N) ⁅x, m⁆ : N),
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
            (a : M) → N)
          n :
        N)
⊢ {
      toFun := fun (m : M) ↦
        HSub.hSub (α := N) (β := N) (⁅x, (f + g : (a : M) → N) m⁆ : N) ((f + g : (a : M) → N) ⁅x, m⁆ : N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] N)
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) m⁆ : N) ((g : (a : M) → N) ⁅x, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m n_1 : M
x : L
f g : M →ₗ[R] N
n : M
h :
  HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) (⁅x, (g : (a : M) → N) n⁆ : N) -
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, n⁆ : N) ((g : (a : M) → N) ⁅x, n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) n⁆ : N) ((g : (a : M) → N) ⁅x, n⁆ : N)
⊢ Eq.{w₁ + 1} (α := N)
    (({
            toFun := fun (m : M) ↦
              HSub.hSub (α := N) (β := N) (⁅x, (f + g : (a : M) → N) m⁆ : N) ((f + g : (a : M) → N) ⁅x, m⁆ : N),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → N)
        n :
      N)
    ((HAdd.hAdd (α := M →ₗ[R] N)
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) m⁆ : N) ((g : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
          (a : M) → N)
        n :
      N)

Tactic:
simp only [coe_mk, AddHom.coe_mk, lie_add, add_apply]

Premises used: LinearMap.coe_mk, LinearMap.add_apply, AddHom.coe_mk, lie_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m n_1 : M
x : L
f g : M →ₗ[R] N
n : M
⊢ HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) (⁅x, (g : (a : M) → N) n⁆ : N) -
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, n⁆ : N) ((g : (a : M) → N) ⁅x, n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) n⁆ : N) ((g : (a : M) → N) ⁅x, n⁆ : N)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y_1 z : L
m n_1 : M
x y : L
f : M →ₗ[R] N
n : M
⊢ HSub.hSub (α := N) (β := N) (⁅x, ⁅y, (f : (a : M) → N) n⁆⁆ : N) (⁅x, (f : (a : M) → N) ⁅y, n⁆⁆ : N) -
      HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) ⁅x, n⁆⁆ : N) ((f : (a : M) → N) ⁅y, ⁅x, n⁆⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, ⁅y, (f : (a : M) → N) n⁆⁆ : N) (⁅y, ⁅x, (f : (a : M) → N) n⁆⁆ : N) -
        HSub.hSub (α := N) (β := N) ((f : (a : M) → N) ⁅x, ⁅y, n⁆⁆ : N) ((f : (a : M) → N) ⁅y, ⁅x, n⁆⁆ : N) +
      (HSub.hSub (α := N) (β := N) (⁅y, ⁅x, (f : (a : M) → N) n⁆⁆ : N) (⁅y, (f : (a : M) → N) ⁅x, n⁆⁆ : N) -
        HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) ⁅y, n⁆⁆ : N) ((f : (a : M) → N) ⁅x, ⁅y, n⁆⁆ : N))

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
f : M →ₗ[R] N
x : L
m : M
⊢ (⁅x, f⁆ : (a : M) → N) m = HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m n : M
t : R
x : L
f : M →ₗ[R] N
h : ∀ (n : M), Eq.{w₁ + 1} (α := N) ((⁅t • x, f⁆ : (a : M) → N) n : N) ((t • ⁅x, f⁆ : (a : M) → N) n : N)
⊢ ⁅t • x, f⁆ = t • ⁅x, f⁆

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m n_1 : M
t : R
x : L
f : M →ₗ[R] N
n : M
⊢ Eq.{w₁ + 1} (α := N) ((⁅t • x, f⁆ : (a : M) → N) n : N) ((t • ⁅x, f⁆ : (a : M) → N) n : N)

Tactic:
simp only [smul_sub, smul_lie, smul_apply, LieHom.lie_apply, map_smul]

Premises used: LinearMap.smul_apply, LieHom.lie_apply, smul_lie, smul_sub, map_smul
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m n : M
t : R
x : L
f : M →ₗ[R] N
h : ∀ (n : M), Eq.{w₁ + 1} (α := N) ((⁅x, t • f⁆ : (a : M) → N) n : N) ((t • ⁅x, f⁆ : (a : M) → N) n : N)
⊢ ⁅x, t • f⁆ = t • ⁅x, f⁆

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m n_1 : M
t : R
x : L
f : M →ₗ[R] N
n : M
⊢ Eq.{w₁ + 1} (α := N) ((⁅x, t • f⁆ : (a : M) → N) n : N) ((t • ⁅x, f⁆ : (a : M) → N) n : N)

Tactic:
simp only [smul_sub, smul_apply, LieHom.lie_apply, lie_smul]

Premises used: LinearMap.smul_apply, lie_smul, LieHom.lie_apply, smul_sub
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m n : M
x : L
f : M →ₗ[R] R
⊢ ∀ (x_2 y : M),
    -(f : (a : M) → R) ⁅x, x_2 + y⁆ =
      HAdd.hAdd (α := R) (β := R) (-(f : (a : M) → R) ⁅x, x_2⁆ : R) (-(f : (a : M) → R) ⁅x, y⁆ : R)

Tactic:
simp [-neg_add_rev, neg_add]

Premises used: neg_add_rev, neg_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m n : M
x : L
f : M →ₗ[R] R
⊢ ∀ (m : R) (x_2 : M),
    -(f : (a : M) → R) ⁅x, m • x_2⁆ =
      HSMul.hSMul (α := R) (β := R) ((RingHom.id R : (a : R) → R) m : R) (-(f : (a : M) → R) ⁅x, x_2⁆ : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y_1 z : L
m_1 n : M
x y : L
m : M →ₗ[R] R
h :
  ∀ (n : M),
    Eq.{u + 1} (α := R)
      (({ toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x + y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R) n :
        R)
      ((HAdd.hAdd (α := M →ₗ[R] R)
              { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
              { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
            (a : M) → R)
          n :
        R)
⊢ { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x + y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] R)
      { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
      { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y_1 z : L
m_1 n_1 : M
x y : L
m : M →ₗ[R] R
n : M
⊢ Eq.{u + 1} (α := R)
    (({ toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x + y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R) n : R)
    ((HAdd.hAdd (α := M →ₗ[R] R)
            { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
            { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
          (a : M) → R)
        n :
      R)

Tactic:
simp [-neg_add_rev, neg_add]

Premises used: neg_add_rev, neg_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m_1 n_1 : M
x : L
m n : M →ₗ[R] R
h :
  ∀ (p : M),
    Eq.{u + 1} (α := R)
      (({ toFun := fun (m_2 : M) ↦ -(m + n : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R) p :
        R)
      ((HAdd.hAdd (α := M →ₗ[R] R)
              { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
              { toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
            (a : M) → R)
          p :
        R)
⊢ { toFun := fun (m_2 : M) ↦ -(m + n : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] R)
      { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
      { toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }

Tactic:
ext p
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m_1 n_1 : M
x : L
m n : M →ₗ[R] R
p : M
⊢ Eq.{u + 1} (α := R)
    (({ toFun := fun (m_2 : M) ↦ -(m + n : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R) p : R)
    ((HAdd.hAdd (α := M →ₗ[R] R)
            { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
            { toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
          (a : M) → R)
        p :
      R)

Tactic:
simp [-neg_add_rev, neg_add]

Premises used: neg_add_rev, neg_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m_1 n_1 : M
x m : L
n : M →ₗ[R] R
h :
  ∀ (p : M),
    Eq.{u + 1} (α := R)
      (({
              toFun := fun (m_2 : M) ↦
                -({ toFun := fun (m_3 : M) ↦ -(n : (a : M) → R) ⁅m, m_3⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R)
                    ⁅x, m_2⁆,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : M) → R)
          p :
        R)
      ((HAdd.hAdd (α := M →ₗ[R] R)
              { toFun := fun (m_2 : M) ↦ -(n : (a : M) → R) ⁅⁅x, m⁆, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
              {
                toFun := fun (m_2 : M) ↦
                  -({ toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
                        (a : M) → R)
                      ⁅m, m_2⁆,
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
            (a : M) → R)
          p :
        R)
⊢ {
      toFun := fun (m_2 : M) ↦
        -({ toFun := fun (m_3 : M) ↦ -(n : (a : M) → R) ⁅m, m_3⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R)
            ⁅x, m_2⁆,
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] R)
      { toFun := fun (m_2 : M) ↦ -(n : (a : M) → R) ⁅⁅x, m⁆, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
      {
        toFun := fun (m_2 : M) ↦
          -({ toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
                (a : M) → R)
              ⁅m, m_2⁆,
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }

Tactic:
ext p
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t : R
x_1 y z : L
m_1 n_1 : M
x m : L
n : M →ₗ[R] R
p : M
⊢ Eq.{u + 1} (α := R)
    (({
            toFun := fun (m_2 : M) ↦
              -({ toFun := fun (m_3 : M) ↦ -(n : (a : M) → R) ⁅m, m_3⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R)
                  ⁅x, m_2⁆,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → R)
        p :
      R)
    ((HAdd.hAdd (α := M →ₗ[R] R)
            { toFun := fun (m_2 : M) ↦ -(n : (a : M) → R) ⁅⁅x, m⁆, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
            {
              toFun := fun (m_2 : M) ↦
                -({ toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
                      (a : M) → R)
                    ⁅m, m_2⁆,
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
          (a : M) → R)
        p :
      R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
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
x : L
m : M
f : M →ₗ[R] R
⊢ Eq.{u + 1} (α := R) ((⁅x, f⁆ : (a : M) → R) m : R) (-(f : (a : M) → R) ⁅x, m⁆ : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x : L
m : M →ₗ[R] R
h : ∀ (n : M), Eq.{u + 1} (α := R) ((⁅t • x, m⁆ : (a : M) → R) n : R) ((t • ⁅x, m⁆ : (a : M) → R) n : R)
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m_1 n_1 : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ Eq.{u + 1} (α := R) ((⁅t • x, m⁆ : (a : M) → R) n : R) ((t • ⁅x, m⁆ : (a : M) → R) n : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x : L
m : M →ₗ[R] R
h : ∀ (n : M), Eq.{u + 1} (α := R) ((⁅x, t • m⁆ : (a : M) → R) n : R) ((t • ⁅x, m⁆ : (a : M) → R) n : R)
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
ext n
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
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
t_1 : R
x_1 y z : L
m_1 n_1 : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ Eq.{u + 1} (α := R) ((⁅x, t • m⁆ : (a : M) → R) n : R) ((t • ⁅x, m⁆ : (a : M) → R) n : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
ι : Type u_1
s : Finset ι
f : ι → L
m : M
⊢ Bracket.bracket.{v, w} (L := L) (∑ i ∈ s, f i) m = ∑ i ∈ s, ⁅f i, m⁆

Tactic:
map_sum ((LieRingModule.toEnd L M).flip m) f s

Premises used: map_sum, AddMonoidHom.flip, LieRingModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
ι : Type u_1
s : Finset ι
f : ι → M
a : L
⊢ Eq.{w + 1} (α := M) ⁅a, ∑ i ∈ s, f i⁆ (∑ i ∈ s, ⁅a, f i⁆)

Tactic:
map_sum (LieRingModule.toEnd L M a) f s

Premises used: map_sum, LieRingModule.toEnd, DFunLike.coe