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
M : Type u_4
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 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
r : A
x_1 : A ⊗[R] L
y : A ⊗[R] M
hx_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x_1
hy :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    y
h : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1, y⁆
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅r • x_1, y⁆

Tactic:
simp [add_mem, Submodule.smul_mem, *]

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- 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 : 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 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
r : A
x_1 : A ⊗[R] L
y : A ⊗[R] M
hx_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x_1
hy :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    y
h : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1, y⁆
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1, r • y⁆

Tactic:
simp [add_mem, Submodule.smul_mem, *]

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Add M
inst_4 : IsLieTower L₁ L₂ M
x : L₁
y : L₂
m : M
⊢ ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆

Tactic:
IsLieTower.leibniz_lie x y m

Premises used: IsLieTower.leibniz_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
⊢ ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆

Tactic:
have h1 := leibniz_lie x y m
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
⊢ ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆

Tactic:
have h2 := leibniz_lie y x m
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)

Tactic:
congr($h1.symm - $h2)

Premises used: congrArg, HSub.hSub, id, congr, Eq.symm
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
h : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
h₁ : -⁅⁅y, x⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Tactic:
convert! congr($h1.symm - $h2) using 1

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

Tactic:
simp only [add_sub_cancel_right, sub_add_cancel_right]

Premises used: add_sub_cancel_right, sub_add_cancel_right
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst : Bracket L₁ L₂
inst_1 : Bracket L₁ M
inst_2 : Bracket L₂ M
inst_3 : Bracket L₂ L₁
inst_4 : AddCommGroup M
inst_5 : IsLieTower L₁ L₂ M
inst_6 : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ -⁅⁅y, x⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)

Tactic:
simp only [add_sub_cancel_right, sub_add_cancel_right]

Premises used: add_sub_cancel_right, sub_add_cancel_right
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type u_1
inst : LieRing L
toModule : Module ℚ L
h₁ : ∀ (t : ℚ) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆
toModule_1 : Module ℚ L
h₂ : ∀ (t : ℚ) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆
heq : Eq.{u_1 + 1} (α := Module ℚ L) LieAlgebra.toModule LieAlgebra.toModule
⊢ { toModule := toModule, lie_smul := h₁ : LieAlgebra ℚ L } = { toModule := toModule_1, lie_smul := h₂ }

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type u_1
inst : LieRing L
⊢ Subsingleton.{max (u_1 + 1) 1} (LieAlgebra ℚ L)

Tactic:
LieAlgebra.toModule_injective L |>.subsingleton

Premises used: Function.Injective.subsingleton, LieAlgebra.toModule_injective
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x y : L
m : M
⊢ ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆

Tactic:
LieRingModule.add_lie x y m

Premises used: LieRingModule.add_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m n : M
⊢ ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆

Tactic:
LieRingModule.lie_add x m n

Premises used: LieRingModule.lie_add
-- 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
t : R
x : L
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
LieModule.smul_lie t x m

Premises used: LieModule.smul_lie
-- 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
t : R
x : L
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
LieModule.lie_smul t x m

Premises used: LieModule.lie_smul
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
⊢ Eq.{w + 1} (α := M) ⁅x, 0⁆ 0

Tactic:
(AddMonoidHom.mk' _ (lie_add x)).map_zero

Premises used: AddMonoidHom.map_zero, AddMonoidHom.mk'
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
m : M
⊢ Bracket.bracket.{v, w} (L := L) 0 m = 0

Tactic:
(AddMonoidHom.mk' (fun x : L => ⁅x, m⁆) fun x y => add_lie x y m).map_zero

Premises used: AddMonoidHom.map_zero, Bracket.bracket, AddMonoidHom.mk', add_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
inst : LieRing L
x : L
⊢ ⁅x, x⁆ = 0

Tactic:
LieRing.lie_self x

Premises used: LieRing.lie_self
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
inst : LieRing L
x y : L
rw : ⁅x + y, x + y⁆ = 0
⊢ ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0

Tactic:
rw [← lie_add]

Premises used: lie_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
inst : LieRing L
x y : L
⊢ ⁅x + y, x + y⁆ = 0

Tactic:
apply lie_self

Premises used: lie_self
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
inst : LieRing L
x y : L
⊢ ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0

Tactic:
have h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0 := by rw [← lie_add]; apply lie_self
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
inst : LieRing L
x y : L
h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0
⊢ -⁅y, x⁆ = ⁅x, y⁆

Tactic:
simpa [neg_eq_iff_add_eq_zero] using h

Premises used: neg_eq_iff_add_eq_zero
-- 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 m : L
rw : -⁅m, t • x⁆ = t • ⁅x, m⁆
rw₁ : -⁅m, t • x⁆ = t • -⁅m, x⁆
rw₂ : -(t • ⁅m, x⁆) = t • -⁅m, x⁆
rw₃ rw₄ : -(t • ⁅m, x⁆) = -(t • ⁅m, x⁆)
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]

Premises used: smul_neg, LieAlgebra.lie_smul, lie_skew
-- 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 y z : L
m n : M
⊢ ∀ (t : R) (x m : L), ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
apply LieAlgebra.lie_smul

Premises used: LieAlgebra.lie_smul
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
rw : ⁅-x + x, m⁆ = 0
⊢ ⁅-x, m⁆ = -⁅x, m⁆

Tactic:
rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]

Premises used: sub_eq_zero, sub_neg_eq_add, add_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
⊢ ⁅-x + x, m⁆ = 0

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
x : L
m : M
rw : ⁅x, -m + m⁆ = 0
⊢ ⁅x, -m⁆ = -⁅x, m⁆

Tactic:
rw [← sub_eq_zero, sub_neg_eq_add, ← lie_add]

Premises used: sub_eq_zero, sub_neg_eq_add, lie_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m + m⁆ = 0

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
x y : L
m : M
⊢ ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m n : M
⊢ ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
n : ℕ
⊢ ⁅n • x, m⁆ = n • ⁅x, m⁆

Tactic:
AddMonoidHom.map_nsmul
    { toFun := fun x : L => ⁅x, m⁆, map_zero' := zero_lie m, map_add' := fun _ _ => add_lie _ _ _ }
    _ _

Premises used: Bracket.bracket, AddMonoidHom.map_nsmul, AddMonoidHom.mk, ZeroHom.mk, zero_lie, add_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
n : ℕ
⊢ ⁅x, n • m⁆ = n • ⁅x, m⁆

Tactic:
AddMonoidHom.map_nsmul
    { toFun := fun m : M => ⁅x, m⁆, map_zero' := lie_zero x, map_add' := fun _ _ => lie_add _ _ _ }
    _ _

Premises used: Bracket.bracket, AddMonoidHom.map_nsmul, AddMonoidHom.mk, ZeroHom.mk, lie_zero, lie_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
a : ℤ
⊢ ⁅a • x, m⁆ = a • ⁅x, m⁆

Tactic:
AddMonoidHom.map_zsmul
    { toFun := fun x : L => ⁅x, m⁆, map_zero' := zero_lie m, map_add' := fun _ _ => add_lie _ _ _ }
    _ _

Premises used: AddMonoidHom.map_zsmul, Bracket.bracket, AddMonoidHom.mk, ZeroHom.mk, zero_lie, add_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x : L
m : M
a : ℤ
⊢ ⁅x, a • m⁆ = a • ⁅x, m⁆

Tactic:
AddMonoidHom.map_zsmul
    { toFun := fun m : M => ⁅x, m⁆, map_zero' := lie_zero x, map_add' := fun _ _ => lie_add _ _ _ }
    _ _

Premises used: AddMonoidHom.map_zsmul, Bracket.bracket, AddMonoidHom.mk, ZeroHom.mk, lie_zero, lie_add
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
x y : L
m : M
rw : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
rw₁ rw₂ : ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆
⊢ ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

Tactic:
rw [leibniz_lie, add_sub_cancel_right]

Premises used: leibniz_lie, add_sub_cancel_right
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
inst : LieRing L
x y z : L
rw : -(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0
⊢ ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0

Tactic:
rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie]

Premises used: lie_neg, Bracket.bracket, neg_neg, lie_skew, lie_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
L : Type v
inst : LieRing L
x y z : L
⊢ -(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0

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 y z : L
m n : M
h :
  ∀ (n : M),
    Eq (α := M)
      (({ toFun := fun (m : M) ↦ Bracket.bracket.{v, w} (L := L) 0 m, map_zero' := ⋯, map_add' := ⋯ } : (a : M) → M) n :
        M)
      ((0 : (a : M) → M) n : M)
⊢ Eq.{w + 1} (α := M →+ M) { toFun := fun (m : M) ↦ Bracket.bracket.{v, w} (L := L) 0 m, map_zero' := ⋯, map_add' := ⋯ }
    0

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 y z : L
m n_1 n : M
⊢ Eq (α := M)
    (({ toFun := fun (m : M) ↦ Bracket.bracket.{v, w} (L := L) 0 m, map_zero' := ⋯, map_add' := ⋯ } : (a : M) → M) n :
      M)
    ((0 : (a : M) → M) n : M)

Tactic:
zero_lie n

Premises used: zero_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 y z : L
m n_1 n : M
⊢ Eq (α := M)
    (({ toFun := fun (m : M) ↦ Bracket.bracket.{v, w} (L := L) 0 m, map_zero' := ⋯, map_add' := ⋯ } : (a : M) → M) n :
      M)
    ((0 : (a : M) → M) n : M)

Tactic:
exact zero_lie n

Premises used: zero_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 y_1 z_1 : L
m n : M
y z : L
h :
  ∀ (n : M),
    Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } : (a : M) → M) n : M)
      ((HAdd.hAdd (α := M →+ M) { toFun := fun (m : M) ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M }
              { toFun := fun (m : M) ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M } :
            (a : M) → M)
          n :
        M)
⊢ { toFun := fun (m : M) ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } =
    HAdd.hAdd (α := M →+ M) { toFun := fun (m : M) ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M }
      { toFun := fun (m : M) ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ 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 : R
x y_1 z_1 : L
m n_1 : M
y z : L
n : M
⊢ Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } : (a : M) → M) n : M)
    ((HAdd.hAdd (α := M →+ M) { toFun := fun (m : M) ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M }
            { toFun := fun (m : M) ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M } :
          (a : M) → M)
        n :
      M)

Tactic:
add_lie y z n

Premises used: 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 y_1 z_1 : L
m n_1 : M
y z : L
n : M
⊢ Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } : (a : M) → M) n : M)
    ((HAdd.hAdd (α := M →+ M) { toFun := fun (m : M) ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M }
            { toFun := fun (m : M) ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ : M →+ M } :
          (a : M) → M)
        n :
      M)

Tactic:
exact add_lie y z n

Premises used: 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 z : L
m_1 n_1 : M
x : L
f : M →ₗ[R] N
m n : M
simp :
  HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) (⁅x, (f : (a : M) → N) n⁆ : N) -
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, m⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N)
⊢ HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) (m + n)⁆ : N) ((f : (a : M) → N) ⁅x, m + n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N)

Tactic:
simp only [lie_add, map_add]

Premises used: map_add, 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_1 n_1 : M
x : L
f : M →ₗ[R] N
m n : M
⊢ HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) (⁅x, (f : (a : M) → N) n⁆ : N) -
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, m⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N) +
      HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (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_1 : R
x_1 y z : L
m_1 n : M
x : L
f : M →ₗ[R] N
t : R
m : M
⊢ HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) (t • m)⁆ : N) ((f : (a : M) → N) ⁅x, t • m⁆ : N) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R)
      (HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N))

Tactic:
simp only [smul_sub, map_smul, lie_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, lie_smul, smul_sub, map_smul